anchor.diff:        let e = eapply (Operator (x + "[]")) [e1; e2] in
         let (t, ae) = infer_exp env u e expected_typ in
         match ae with
  -      | (AE_Apply (_, _, es), _) -> ret t (AE_Op (Subscript, es)) // TODO: save x or t1
  +      | (AE_Apply (_, _, es), _) -> ret t.norm_typ (AE_Op (Subscript, es)) // TODO: save x or t1
         | _ -> internalErr ("EOp Subscript")
       )
     | EOp (Update, [e1; e2; e3]) ->
  
positive.code: // t1 = t2
  let u_constrain_equal_loc (u:unifier) (loc:loc option) (t1:typ) (t2:typ):unit =
    if t1 = t2 then () else
    // printfn "constrain %A = %A at %A" t1 t2 (match loc with None -> "None" | Some loc -> string_of_loc loc);
    u.u_equalities <- (t1, t2, loc)::u.u_equalities
  
  
negative.code:       err ("circular type constraint" + err_id x + " " + string_of_typ t)
      else u_add_subst u x t
  
  let rec u_unify_one (u:unifier) (loc:loc option) (t1:typ) (t2:typ):unit =
    let r = u_unify_one u loc in
    if t1 = t2 then () else
    let env = u.u_env in
    let t1 = subst_typ u.u_substs t1 in
    let t2 = subst_typ u.u_substs t2 in
    if t1 = t2 then () else
    let typ_err () = err ("cannot coerce type '" + string_of_typ t1 + "' to type '" + string_of_typ t2 + "'") in
    match (t1, t2) with
    | (TVar (x, _), _) -> u_bind u x t2
    | (_, TVar (x, _)) -> u_bind u x t1
    | (TTuple ts1, TTuple ts2) when List.length ts1 = List.length ts2 ->
        List.iter2 (fun t1 t2 -> u_constrain_equal_loc u loc t1 t2) ts1 ts2
    | (TFun (ts1, t1), TFun (ts2, t2)) when List.length ts1 = List.length ts2 ->
        List.iter2 (fun t1 t2 -> u_constrain_equal_loc u loc t1 t2) ts1 ts2;
        u_constrain_equal_loc u loc t1 t2
    | (TApply (x1, ts1), TApply (x2, ts2)) when List.length ts1 = List.length ts2 ->
        if (x1 = x2) then
          List.iter2 (fun t1 t2 -> u_constrain_equal_loc u loc t1 t2) ts1 ts2
        else
          let t1 = normalize_type env t1 in
          let t2 = normalize_type env t2 in
          match (t1.norm_typ, t2.norm_typ) with
          | (TApply (x1, ts1), TApply (x2, ts2)) when x1 = x2 && List.length ts1 = List.length ts2 ->
            List.iter2 (fun t1 t2 -> u_constrain_equal_loc u loc t1 t2) ts1 ts2
          | _ -> typ_err() 
    | _ when typ_equal env t1 t2 -> () 
    | _ -> 
      let norm1 = normalize_type env t1 in
      let norm2 = normalize_type env t2 in
      if norm1.norm_typ = t1 && norm2.norm_typ = t2 then typ_err() else
      r norm1.norm_typ norm2.norm_typ
  
  let rec u_unify_equalities (u:unifier):unit =
    match u.u_equalities with
  