anchor.diff:              else giveup env "head-symbol is free" orig probs
      
     
  -and solve_t (top:bool) (env:Env.env) (rel:rel) (t1:typ) (t2:typ) (probs:worklist) : solution = 
  -    if Util.physical_equality t1 t2 then solve env probs else
  -    let t1 = compress env probs.subst t1 in
  -    let t2 = compress env probs.subst t2 in 
  -    if Util.physical_equality t1 t2 then solve env probs else
  -    let _ = if debug env (Options.Other "Rel") then Util.fprint2 "Attempting (top level? %s):\n%s\n" (if top then "true" else "false") (prob_to_string env (TProb(top, rel, t1, t2))) in
  -//    printfn "Tag t1 = %s, t2 = %s" (Print.tag_of_typ t1) (Print.tag_of_typ t2);
  -    if Util.physical_equality t1 t2 then solve env probs else
  -    let r = Env.get_range env in
  -    let solve_and_close env binders subprobs probs p = 
  -        let sol = match p with 
  -            | TProb(top, rel, t1, t2) -> solve_t top env rel t1 t2 empty_worklist 
  -            | CProb(top, rel, c1, c2) -> solve_c top env rel c1 c2 empty_worklist
  -            | _ -> failwith "impos" in
  -        begin match sol with 
  -            | Success (subst, guard_f) -> 
  -                let probs = extend_subst' subst probs |> guard env false (close_guard binders guard_f) in
  -                solve env (attempt subprobs probs)
  -
  -            | Failed reasons -> 
  -                giveup env (reasons |> List.map (fun (_, _, r) -> r) |> String.concat ", ")  p probs
  -        end in 
  -
  -    match t1.n, t2.n with
  -      | Typ_ascribed(t, _), _
  -      | Typ_meta(Meta_pattern(t, _)), _ 
  -      | Typ_meta(Meta_labeled(t, _, _)), _
  -      | Typ_meta(Meta_refresh_label(t, _, _)), _
  -      | Typ_meta(Meta_named(t, _)), _ -> solve_t top env rel t t2 probs
  -
  -      | _, Typ_ascribed(t, _)
  -      | _, Typ_meta(Meta_pattern(t, _))
  -      | _, Typ_meta(Meta_labeled(t, _, _))
  -      | _, Typ_meta(Meta_refresh_label(t, _, _))
  -      | _, Typ_meta(Meta_named(t, _)) -> solve_t top env rel t1 t probs
  -
  -      | Typ_btvar a, Typ_btvar b -> 
  -        if Util.bvd_eq a.v b.v 
  -        then solve env probs
  -        else giveup env "unequal type variables" (TProb(top, rel, t1, t2)) probs (* TODO: They may be equal by refinement, though *)
  -
  -      | Typ_fun(bs1, c1), Typ_fun(bs2, c2) ->
  -        let curry_fun n bs c = 
  -         let bs, rest = Util.first_N n bs in
  -         (bs, mk_Total(mk_Typ_fun(rest, c) ktype c.pos)) in
  -            
  -        let (bs1, c1), (bs2, c2) = 
  -            let l1 = List.length bs1 in
  -            let l2 = List.length bs2 in
  -            if l1 = l2
  -            then (bs1, c1), (bs2, c2)
  -            else if l1 > l2
  -            then curry_fun l2 bs1 c1, (bs2, c2) 
  -            else (bs1, c1), curry_fun l1 bs2 c2 in
  -        solve_binders env bs1 bs2 rel (TProb(top, rel, t1, t2)) probs
  -        (fun subst subprobs -> 
  -            let c2 = Util.subst_comp subst c2 in
  -            let rel = if !Options.verify then EQ else rel in
  -            solve_and_close env bs1 subprobs probs (CProb(false, rel, c1, c2)))
  -
  -      | Typ_lam(bs1, t1'), Typ_lam(bs2, t2') -> 
  -        solve_binders env bs1 bs2 rel (TProb(top, rel, t1, t2)) probs
  -        (fun subst subprobs -> 
  -            let prob = TProb(false, rel, t1', Util.subst_typ subst t2') in
  -            if Env.debug env <| Options.Other "Rel"
  -            then (Util.fprint3 "Kind of lhs is %s body type %s is %s\n" (Normalize.kind_norm_to_string env t1.tk) (Normalize.typ_norm_to_string env t1') (Normalize.kind_norm_to_string env t1'.tk);
  -                  Util.fprint1 "Sub-problems from Typ_lam:\n%s\n" ((prob::subprobs) |> List.map (prob_to_string env) |> String.concat "\n"));
  -            solve_and_close env bs1 subprobs probs prob)
  -
  -      | Typ_refine(x1, phi1), Typ_refine(x2, phi2) -> 
  -        let base_prob = TProb(top, rel, x1.sort, x2.sort) in
  -        let subst = [Inr(x2.v, Util.bvar_to_exp x1)] in
  -        let phi2 = Util.subst_typ subst phi2 in
  -        begin match rel with 
  -            | EQ -> 
  -              solve_and_close env [v_binder x1] [base_prob] probs (TProb(false, EQ, phi1, phi2))
  -               
  -            | SUB -> 
  -              let g = NonTrivial <| mk_Typ_lam([v_binder x1], Util.mk_imp phi1 phi2) (mk_Kind_arrow([v_binder x1], ktype) r) r in
  -              let probs = guard env top g probs in
  -              solve env (attempt [base_prob] probs)
  -        end
  -
  -      (* flex-flex *)
  -      | Typ_uvar _, Typ_uvar _
  -      | Typ_app({n=Typ_uvar _}, _), Typ_uvar _ 
  -      | Typ_uvar _, Typ_app({n=Typ_uvar _}, _)
  -      | Typ_app({n=Typ_uvar _}, _), Typ_app({n=Typ_uvar _}, _) -> 
  -        solve_t_flex_flex top env (TProb(top, rel, t1, t2)) (destruct_flex_t t1) (destruct_flex_t t2) probs
  -   
  -      (* flex-rigid *)
  -      | Typ_uvar _, _
  -      | Typ_app({n=Typ_uvar _}, _), _ -> 
  -        solve_t_flex_rigid top env (TProb(top, rel, t1, t2)) (destruct_flex_t t1) t2 probs
  -
  -      (* rigid-flex ... reorient *)
  -      | _, Typ_uvar _ 
  -      | _, Typ_app({n=Typ_uvar _}, _) ->
  -        solve_t top env EQ t2 t1 probs 
  -
  -      | Typ_refine(x, phi1), _ ->
  -        if rel=EQ
  -        then giveup env "refinement subtyping is not applicable" (TProb(top, rel, t1, t2)) probs //but t2 may be able to take delta steps
  -        else solve_t top env rel x.sort t2 probs
  -
  -      | _, Typ_refine(x, phi2) -> 
  -        if rel=EQ
  -        then giveup env "refinement subtyping is not applicable" (TProb(top, rel, t1, t2)) probs //but t1 may be able to take delta steps
  -        else let g = NonTrivial <| mk_Typ_lam([v_binder (bvd_to_bvar_s x.v t1)], phi2) (mk_Kind_arrow([null_v_binder t1], ktype) r) r in
  -             solve_t top env rel t1 x.sort (guard env top g probs)   
  -      
  -      | Typ_btvar _, _
  -      | Typ_const _, _
  -      | Typ_app _, _
  -      | _, Typ_btvar _
  -      | _, Typ_const _ 
  -      | _, Typ_app _ -> 
  -         let m, o = head_matches_delta env t1 t2 in
  -         begin match m, o  with 
  -            | (MisMatch, _) -> 
  -                giveup env "head mismatch (t-1)" (TProb(top, rel, t1, t2)) probs        //heads definitely do not match
  -
  -            | (_, Some (t1, t2)) ->
  -               //              printfn "Head match with delta %s, %s" (Print.typ_to_string head) (Print.typ_to_string head');
  -               probs |> solve_t top env rel t1 t2
  -
  -            | (_, None) -> //head matches head'
  -                if debug env <| Options.Other "Rel" then Util.fprint2 "Head matches: %s and %s\n" (Print.typ_to_string t1) (Print.typ_to_string t2);
  -                let head, args = Util.head_and_args t1 in
  -                let head', args' = Util.head_and_args t2 in
  -                if List.length args = List.length args'
  -                then let subprobs = List.map2 (fun a a' -> match fst a, fst a' with 
  -                    | Inl t, Inl t' -> TProb(false, EQ, t, t')
  -                    | Inr v, Inr v' -> EProb(false, EQ, v, v')
  -                    | _ -> failwith "Impossible" (*terms are well-kinded*)) args args' in
  -                    let subprobs = match m with 
  -                        | FullMatch -> subprobs
  -                        | _ -> TProb(false, EQ, head, head')::subprobs in
  -                    solve env (attempt subprobs probs)
  -                else giveup env (Util.format4 "unequal number of arguments: %s[%s] and %s[%s]" 
  -                            (Print.typ_to_string head)
  -                            (Print.args_to_string args)
  -                            (Print.typ_to_string head')
  -                            (Print.args_to_string args')) 
  -                            (TProb(top, rel, t1, t2)) probs
  -          end
  -
  -      | _ -> giveup env (Util.format2 "head mismatch (t-2): %s and %s" (Print.tag_of_typ t1) (Print.tag_of_typ t2)) (TProb(top, rel, t1, t2)) probs
  -
  -and solve_c (top:bool) (env:Env.env) (rel:rel) (c1:comp) (c2:comp) (probs:worklist) : solution =
  -    if Util.physical_equality c1 c2 then solve env probs
  -    else let _ = if debug env <| Options.Other "Rel" then Util.fprint2 "solve_c %s and %s\n" (Print.comp_typ_to_string c1) (Print.comp_typ_to_string c2) in
  -         let r = Env.get_range env in
  -         let c1_0, c2_0 = c1, c2 in
  -         match c1.n, c2.n with
  -               | Total t1, Total t2 -> //rigid-rigid 1
  -                 solve_t false env rel t1 t2 probs
  -               
  -               | Total _,  Comp _ -> solve_c top env rel (mk_Comp <| comp_to_comp_typ c1) c2 probs
  -               | Comp _, Total _ -> solve_c top env rel c1 (mk_Comp <| comp_to_comp_typ c2) probs
  -               
  -               | Comp _, Comp _ ->
  -                 if (Util.is_ml_comp c1 && Util.is_ml_comp c2) 
  -                    || (Util.is_total_comp c1 && (Util.is_total_comp c2 || Util.is_ml_comp c2))
  -                 then solve_t false env rel (Util.comp_result c1) (Util.comp_result c2) probs 
  -                 else
  -                     let c1_comp = Util.comp_to_comp_typ c1 in
  -                     let c2_comp = Util.comp_to_comp_typ c2 in
  -                     if rel=EQ && lid_equals c1_comp.effect_name c2_comp.effect_name
  -                     then let sub_probs = List.map2 (fun arg1 arg2 -> match fst arg1, fst arg2 with 
  -                            | Inl t1, Inl t2 -> TProb(false, EQ, t1, t2)
  -                            | Inr e1, Inr e2 -> EProb(false, EQ, e1, e2)
  -                            | _ -> failwith "impossible") c1_comp.effect_args c2_comp.effect_args in
  -                          solve env (attempt sub_probs probs)
  -                     else
  -                         let c1 = Normalize.weak_norm_comp env c1 in
  -                         let c2 = Normalize.weak_norm_comp env c2 in
  -                         if debug env <| Options.Other "Rel" then Util.fprint2 "solve_c for %s and %s\n" (c1.effect_name.str) (c2.effect_name.str);
  -                         begin match Tc.Env.monad_leq env c1.effect_name c2.effect_name with
  -                           | None -> giveup env "incompatible monad ordering" (CProb(top, rel, c1_0, c2_0)) probs
  -                           | Some edge ->
  -                             let is_null_wp_2 = c2.flags |> Util.for_some (function TOTAL | MLEFFECT | SOMETRIVIAL -> true | _ -> false) in
  -                             let wpc1, wpc2 = match c1.effect_args, c2.effect_args with 
  -                               | (Inl wp1, _)::_, (Inl wp2, _)::_ -> wp1, wp2 
  -                               | _ -> failwith (Util.format2 "Got effects %s and %s, expected normalized effects" (Print.sli c1.effect_name) (Print.sli c2.effect_name)) in
  -                             let res_t_prob = TProb(false, rel, c1.result_typ, c2.result_typ) in
  -                             if Util.physical_equality wpc1 wpc2 
  -                             then solve env (attempt [res_t_prob] probs)
  -                             else let c2_decl : monad_decl = Tc.Env.get_monad_decl env c2.effect_name in
  -                                  let g = 
  -                                    if is_null_wp_2 
  -                                    then let _ = if debug env <| Options.Other "Rel" then Util.print_string "Using trivial wp ... \n" in
  -                                         NonTrivial <| mk_Typ_app(c2_decl.trivial, [targ c1.result_typ; targ <| edge.mlift c1.result_typ wpc1]) ktype r 
  -                                    else let wp2_imp_wp1 = mk_Typ_app(c2_decl.wp_binop, 
  -                                                                      [targ c2.result_typ; 
  -                                                                       targ wpc2; 
  -                                                                       targ <| Util.ftv Const.imp_lid (Const.kbin ktype ktype ktype); 
  -                                                                       targ <| edge.mlift c1.result_typ wpc1]) wpc2.tk r in
  -                                         NonTrivial <| mk_Typ_app(c2_decl.wp_as_type, [targ c2.result_typ; targ wp2_imp_wp1]) ktype r  in
  -                                  let probs = guard env top g probs in 
  -                                  solve env (attempt [res_t_prob] probs)
  -                         end
  -
  -                                
  -and solve_e (top:bool) (env:Env.env) (rel:rel) (e1:exp) (e2:exp) (probs:worklist) : solution = 
  -    let e1 = compress_e env probs.subst e1 in 
  -    let e2 = compress_e env probs.subst e2 in
  -    let _ = if debug env <| Options.Other "Rel" then Util.fprint1 "Attempting:\n%s\n" (prob_to_string env (EProb(top, rel, e1, e2))) in
  -  
  -    let solve_flex_rigid (u1, t1) r1 args1 e2 = 
  -        let maybe_vars1 = pat_vars env [] args1 in
  -        let sub_problems xs args =
  -            let gi_xi, gi_pi = args |> List.map (function 
  -            | Inl t, imp -> 
  -                let gi_xi, gi = new_tvar t.pos xs t.tk in
  -                let gi_pi = mk_Typ_app(gi, args1) t.tk t.pos in
  -                (Inl gi_xi, imp), TProb(false, EQ, gi_pi, t)
  -            | Inr v, imp ->
  -                let gi_xi, gi = new_evar v.pos xs v.tk in 
  -                let gi_pi = mk_Exp_app(gi, args1) v.tk v.pos in
  -                (Inr gi_xi, imp), EProb(false, EQ, gi_pi, v)) |> List.unzip in
  -          gi_xi, gi_pi in
  -         
  -        let project_e head2 args2 = 
  -            //u p1..pn =?= y a1 .. am
  -            //if pi = y  
  -            //u = \x1..xn. xi (G1 (x1..xn), ..., Gm (x1..xn))
  -            //Gi(p1..pn) =?= ai 
  -            let giveup reason = giveup env (Util.format1 "flex-rigid: refusing to project expressions (%s)" reason) (EProb(top, rel, e1, e2)) probs in
  -            match (Util.compress_exp head2).n with 
  -                | Exp_bvar y -> 
  -                    let all_xs, tres = match Util.function_formals t1 with
  -                        | None -> [], t1
  -                        | Some (xs, c) -> xs, Util.comp_result c in
  -                    if List.length all_xs <> List.length args1
  -                    then giveup (Util.format2 "unequal arity:\n\texpetced binders %s\n\tgot args {%s}" (Print.binders_to_string ", " all_xs) (Print.args_to_string args2))
  -                    else let rec aux xs args = match xs, args with 
  -                            | [], [] -> giveup "variable to project not found"
  -                            | [], _
  -                            | _, [] -> failwith "impossible"
  -                            | (Inl _, _)::xs, (Inl _, _)::args -> aux xs args
  -                            | (Inr xi, _)::xs, (Inr arg, _)::args -> 
  -                                begin match (Util.compress_exp arg).n with 
  -                                       | Exp_bvar z -> 
  -                                          if Util.bvar_eq y z (* found the variable to project *)
  -                                          then let gi_xi, gi_pi = sub_problems all_xs args2 in
  -                                               let sol = mk_Exp_abs(all_xs, mk_Exp_app'(Util.bvar_to_exp xi, gi_xi) tres e1.pos) t1 e1.pos in
  -                                               if Tc.Env.debug env <| Options.Other "Rel"
  -                                               then Util.fprint3 "Projected: %s -> %s\nSubprobs=\n%s\n" (Print.uvar_e_to_string (u1,t1)) (Print.exp_to_string sol) (gi_pi |> List.map (prob_to_string env) |> String.concat "\n");
  -                                               solve env (attempt gi_pi (extend_subst (UE((u1, t1), sol)) probs))
  -                                          else aux xs args
  -                                       | _ -> aux xs args
  -                                end
  -                            | x::xs, arg::args -> giveup (Util.format2 "type incorrect term---impossible: expected %s; got %s\n" (Print.binder_to_string x) (Print.arg_to_string arg)) in
  -                          aux (List.rev all_xs) (List.rev args1)
  -                | _ -> giveup "rhs head term is not a variable" in
  -
  -        let imitate_e () = 
  -            //u1 p1..pn =?= h a1..am
  -            //if h not occurs in u1 and h not free
  -            //u1 = \x1..xn. h (G1(x1...xn), ..., Gm(x1..xn))
  -            //and Gi(p1..pn) =?= ai
  -            if Tc.Env.debug env <| Options.Other "Rel"
  -            then Util.fprint2 "Imitating expressions: %s =?= %s\n" (Print.exp_to_string e1) (Print.exp_to_string e2);
  -            let head2, args2 = Util.head_and_args_e e2 in
  -            let fvhead = Util.freevars_exp head2 in
  -            let occurs_ok, _ = occurs_check_e env (u1, t1) head2 in
  -            if Util.fvs_included fvhead Syntax.no_fvs && occurs_ok
  -            then let xs, tres = match Util.function_formals t1 with
  -                        | None -> [], t1
  -                        | Some (xs, c) -> xs, Util.comp_result c in
  -                 let gi_xi, gi_pi = sub_problems xs args2 in
  -                 let sol = mk_Exp_abs(xs, mk_Exp_app(head2, gi_xi) tres e1.pos) t1 e1.pos in
  -                 if Tc.Env.debug env <| Options.Other "Rel"
  -                 then Util.fprint3 "Imitated: %s -> %s\nSubprobs=\n%s\n" (Print.uvar_e_to_string (u1,t1)) (Print.exp_to_string sol) (gi_pi |> List.map (prob_to_string env) |> String.concat "\n");
  -                 solve env (attempt gi_pi (extend_subst (UE((u1, t1), sol)) probs))
  -            else if occurs_ok 
  -            then project_e head2 args2
  -            else giveup env "flex-rigid: occurs check failed" (EProb(top, rel, e1, e2)) probs in
  -      
  -
  -        begin match maybe_vars1 with 
  -        | None -> imitate_e ()
  -        | Some xs -> 
  -            let fvs1 = freevars_of_binders xs in 
  -            let fvs2 = Util.freevars_exp e2 in 
  -            let occurs_ok, _ = occurs_check_e env (u1, t1) e2 in
  -            if Util.set_is_subset_of fvs2.ftvs fvs1.ftvs 
  -                && Util.set_is_subset_of fvs2.fxvs fvs1.fxvs 
  -                && occurs_ok
  -            then // U1 xs =?= e2
  -                // U1 = \xs. e2
  -                let sol = mk_Exp_abs(xs, e2) t1 r1 in
  -                solve env (extend_subst (UE((u1,t1), sol)) probs)
  -            else imitate_e ()
  -        end in
  -
  -    let solve_flex_flex (u1, t1) r1 args1 (u2, t2) r2 args2 = //flex-flex: solve only patterns
  -      let maybe_vars1 = pat_vars env [] args1 in
  -      let maybe_vars2 = pat_vars env [] args2 in
  -      begin match maybe_vars1, maybe_vars2 with 
  -        | None, _
  -        | _, None -> solve env (defer "flex/flex not a pattern" (EProb(top, rel, e1, e2)) probs) //refuse to solve non-patterns
  -        | Some xs, Some ys -> 
  -          if (Unionfind.equivalent u1 u2 && binders_eq xs ys)
  -          then solve env probs
  -          else 
  -              //U1 xs =?= U2 ys
  -              //zs = xs intersect ys, U fresh
  -              //U1 = \x1 x2. U zs
  -              //U2 = \y1 y2 y3. U zs 
  -              let zs = intersect_vars xs ys in 
  -              let u, _ = new_evar (Env.get_range env) zs e2.tk in
  -              let sub1 = mk_Exp_abs(xs, u) t1 r1 in
  -              let sub2 = mk_Exp_abs(ys, u) t2 r2 in
  -              solve env (extend_subst (UE((u1,t1), sub1)) probs |> extend_subst (UE((u2,t2), sub2))) 
  -      end in
  -
  -    match e1.n, e2.n with 
  -    | Exp_bvar x1, Exp_bvar x1' -> 
  -      if Util.bvd_eq x1.v x1'.v
  -      then solve env probs
  -      else solve env (guard env top (NonTrivial <| Util.mk_eq e1 e2) probs)
  -
  -    | Exp_fvar (fv1, _), Exp_fvar (fv1', _) -> 
  -      if lid_equals fv1.v fv1'.v
  -      then solve env probs
  -      else giveup env "free-variables unequal" (EProb(top, rel, e1, e2)) probs //distinct top-level free vars are never provably equal
  -
  -    | Exp_constant s1, Exp_constant s1' -> 
  -      let const_eq s1 s2 = match s1, s2 with 
  -          | Const_bytearray(b1, _), Const_bytearray(b2, _) -> b1=b2
  -          | Const_string(b1, _), Const_string(b2, _) -> b1=b2
  -          | _ -> s1=s2 in
  -      if const_eq s1 s1'
  -      then solve env probs
  -      else giveup env "constants unequal" (EProb(top, rel, e1, e2)) probs
  -
  -    | Exp_ascribed(e1, _), _ -> 
  -      solve_e top env rel e1 e2 probs
  -
  -    | _, Exp_ascribed(e2, _) -> 
  -      solve_e top env rel e1 e2 probs
  -
  -    | Exp_uvar(u1, t1), Exp_uvar(u2, t2) -> 
  -      solve_flex_flex (u1, t1) e1.pos [] (u2, t2) e2.pos []
  -    | Exp_app({n=Exp_uvar(u1,t1); pos=r1}, args1), Exp_uvar(u2, t2) -> 
  -      solve_flex_flex (u1, t1) r1 args1 (u2, t2) e2.pos []
  -    | Exp_uvar(u1, t1), Exp_app({n=Exp_uvar(u2, t2); pos=r2}, args2) -> 
  -      solve_flex_flex (u1, t1) e1.pos [] (u2, t2) e2.pos args2
  -    | Exp_app({n=Exp_uvar(u1,t1); pos=r1}, args1), Exp_app({n=Exp_uvar(u2, t2); pos=r2}, args2) -> 
  -      solve_flex_flex (u1, t1) r1 args1 (u2, t2) r2 args2
  -
  -    | Exp_uvar(u1, t1), _ ->
  -      solve_flex_rigid (u1, t1) e1.pos [] e2
  -    | Exp_app({n=Exp_uvar(u1,t1); pos=r1}, args1), _ -> //flex-rigid
  -      solve_flex_rigid (u1, t1) r1 args1 e2 
  -
  -    | _, Exp_uvar _ 
  -    | _, Exp_app({n=Exp_uvar _}, _) -> //rigid-flex ... reorient
  -     solve_e top env EQ e2 e1 probs
  -
  -    | _ -> //TODO: check that they at least have the same head? 
  -     solve env (guard env top (NonTrivial <| Util.mk_eq e1 e2) probs)  
             
   let explain env d = 
       if debug env <| Options.Other "ExplainRel"
  
positive.code: //Refinement subtyping with higher-order unification 
  //with special treatment for higher-order patterns 
  //////////////////////////////////////////////////////////////////////////
  type rel = 
    | EQ 
    | SUB
  let rel_to_string = function
    | EQ -> "="
    | SUB -> "<:"
  
  type prob = 
    | KProb of bool * rel * knd * knd 
    | TProb of bool * rel * typ * typ
    | EProb of bool * rel * exp * exp 
    | CProb of bool * rel * comp * comp  //the bool in each case records whether or not it is a 'top-level' problem
  let prob_to_string env = function 
    | KProb(_, rel, k1, k2) -> Util.format3 "\t%s\n\t\t%s\n\t%s" (Print.kind_to_string k1) (rel_to_string rel) (Print.kind_to_string k2)
    | TProb(_, rel, t1, t2) -> 
      Util.format "\t%s : %s (%s) \n\t\t%s\n\t%s : %s (%s)" 
          [//(Normalize.typ_norm_to_string env t1);
           Print.typ_to_string t1;
           Print.kind_to_string t1.tk;
           (Print.tag_of_typ t1) ;
           (rel_to_string rel);
           (Normalize.typ_norm_to_string env t2) ;
           (Print.kind_to_string t2.tk);
           (Print.tag_of_typ t2)]
    | EProb(_, rel, k1, k2) -> Util.format3 "\t%s \n\t\t%s\n\t%s" (Normalize.exp_norm_to_string env k1) (rel_to_string rel) (Normalize.exp_norm_to_string env k2)
    | CProb(_, rel, k1, k2) -> 
      Util.format3 "\t%s \n\t\t%s\n\t%s" (Normalize.comp_typ_norm_to_string env k1) (rel_to_string rel) (Normalize.comp_typ_norm_to_string env k2)
  type uvar_inst =  //never a uvar in the co-domain of this map
    | UK of uvar_k * knd 
    | UT of (uvar_t * knd) * typ 
    | UE of (uvar_e * typ) * exp
    | UC of (uvar_t * knd) * typ
  let str_uvi env ui =
    (* 
       CH: F* fails to type check this without the annotation on u.
       NS: Yes, this is by design. F* does not generalize inner lets by default. 
    *)
    let str (u:Unionfind.uvar<'a>) = if !Options.hide_uvar_nums then "?" else Unionfind.uvar_id u |> string_of_int in
    match ui with
    | UK (u, _) -> str u |> Util.format1 "UK %s"
    | UT ((u,_), t) -> str u |> (fun x -> Util.format2 "UT %s %s" x (Normalize.typ_norm_to_string env t))
    | UE ((u,_), _) -> str u |> Util.format1 "UE %s"
    | UC ((u,_), _) -> str u |> Util.format1 "UC %s"
  
  let print_uvi env uvi = Util.fprint1 "%s\n" (str_uvi env uvi) 
      
  type reason = string
  type worklist = {
      attempting: list<prob>;
      deferred: list<(int * prob * reason)>;
      subst: list<uvar_inst>;
      top_t: option<typ>;      //the guard is either trivial; or a type of kind top_t => Type, where None => Type = Type and (Some t) => Type = t => Type
      guard: guard_t;
      ctr: int;
  }
  type solution = 
      | Success of list<uvar_inst> * guard_t
      | Failed of list<(int * prob * reason)>
  let empty_worklist = {
      attempting=[];
      deferred=[];
      subst=[];
      top_t=None;
      guard=Trivial;
      ctr=0;
  }
  let singleton prob tk = {empty_worklist with attempting=[prob]; top_t=tk}
  
  let reattempt (_, p, _) = p
  let giveup env reason prob probs = 
      if debug env <| Options.Other "Rel"
      then Util.fprint2 "Failed %s:\n%s\n" reason (prob_to_string env prob);
      Failed <| (probs.ctr, prob, reason)::probs.deferred
  let giveup_noex probs = Failed probs.deferred
  let extend_subst ui wl = 
      //Util.print_string "Extending subst ... "; print_uvi ui;
     {wl with subst=ui::wl.subst; ctr=wl.ctr + 1}
  let extend_subst' uis wl = 
     {wl with subst=uis@wl.subst; ctr=wl.ctr + 1}
  
  let defer reason prob wl = {wl with deferred=(wl.ctr, prob, reason)::wl.deferred}
  let attempt probs wl = {wl with attempting=probs@wl.attempting}
  
  let close_predicate f = match (Util.compress_kind f.tk).n with 
      | Kind_arrow(bs, {n=Kind_type}) -> close bs f
      | Kind_type -> f
      | _ ->  failwith "Unexpected kind"
  
  let close_guard_predicate = function
      | Trivial -> Trivial
      | NonTrivial f -> NonTrivial <| close_predicate f
  
  let guard (env:env) top g probs =
      let mk_pred top_t f = match top_t with 
          | None -> f
          | Some t -> 
              let b = [null_v_binder t] in
              mk_Typ_lam(b, f) (mk_Kind_arrow(b, ktype) f.pos) f.pos in
  
      let g = simplify_guard env g in
      match g with 
      | Trivial -> probs
      | NonTrivial f -> 
          let g = if not top 
                  then let qf = close_predicate f in 
                       match probs.top_t, probs.guard with 
                         | _, Trivial -> 
                           NonTrivial (mk_pred probs.top_t qf)
                         | Some _, NonTrivial {n=Typ_lam(bs, body); tk=tk; pos=p} -> 
                           NonTrivial (mk_Typ_lam(bs, Util.mk_conj body qf) tk p)
                         | None, NonTrivial g -> 
                           NonTrivial <| Util.mk_conj g qf
                         | _ -> failwith "Impossible"
                  else match probs.top_t, probs.guard with 
                         | _, Trivial -> NonTrivial f
                         | None, NonTrivial g -> 
                           NonTrivial <| Util.mk_conj g f
                         | Some _, NonTrivial ({n=Typ_lam(xs, g)}) -> 
                              begin match f.n with 
                              | Typ_lam(ys, fbody) ->
                                let xs, args = Util.args_of_binders xs in
                                NonTrivial <| mk_Typ_lam(xs, Util.mk_conj g (Util.subst_typ (Util.subst_of_list ys args) fbody)) g.tk g.pos
                              | _ -> 
                                NonTrivial <| mk_Typ_lam(xs, Util.mk_conj g f) g.tk g.pos
                              end
                        | Some _, _ -> failwith "Impossible" in
          {probs with guard=g}
  
  let commit env uvi = 
    let rec pre_kind_compat k1 k2 = 
     let k1, k2 = (compress_kind k1), (compress_kind k2) in
     match k1.n,k2.n with 
      | _, Kind_uvar uv 
      | Kind_uvar uv, _ -> true
      | Kind_type, Kind_type -> true
      | Kind_abbrev(_, k1), _ -> pre_kind_compat k1 k2
      | _, Kind_abbrev(_, k2) -> pre_kind_compat k1 k2
      | Kind_arrow(bs, k), Kind_arrow(bs', k') -> List.length bs = List.length bs' && pre_kind_compat k k'
      | _ -> Util.print_string (Util.format4 "(%s -- %s) Pre-kind-compat failed on %s and %s\n" (Range.string_of_range k1.pos) (Range.string_of_range k2.pos) (Print.kind_to_string k1) (Print.kind_to_string k2)); 
        false in
  
      uvi |> List.iter (fun uv -> 
          if debug env Extreme then (print_uvi env) uv;
          match uv with 
          | UK(u,k) -> Unionfind.change u (Fixed k)
          | UT((u,k),t) -> //ignore <| pre_kind_compat k t.tk; 
                           if debug env (Options.Other "Rel")
                           then Util.fprint2 "Commiting %s to %s\n" (Print.uvar_t_to_string (u,k)) (Normalize.typ_norm_to_string env t);
                           Unionfind.change u (Fixed t)
          | UE((u,_),e) -> Unionfind.change u (Fixed e)
          | UC((u,_),c) -> Unionfind.change u (Fixed c))
  let find_uvar_k uv s = Util.find_map s (function UK(u, t) -> if Unionfind.equivalent uv u then Some t else None | _ -> None)
  let find_uvar_t uv s = Util.find_map s (function UT((u,_), t) -> if Unionfind.equivalent uv u then Some t else None | _ -> None)
  let find_uvar_e uv s = Util.find_map s (function UE((u,_), t) -> if Unionfind.equivalent uv u then Some t else None | _ -> None)
  let find_uvar_c uv s = Util.find_map s (function UC((u,_), t) -> if Unionfind.equivalent uv u then Some t else None | _ -> None)
  
  let intersect_vars v1 v2 = 
      let fvs1 = freevars_of_binders v1 in
      let fvs2 = freevars_of_binders v2 in 
      binders_of_freevars ({ftvs=Util.set_intersect fvs1.ftvs fvs2.ftvs; fxvs=Util.set_intersect fvs1.fxvs fvs2.fxvs})
  type uvis = list<uvar_inst>
  let rec compress_k (env:env) s k = 
      let k = Util.compress_kind k in 
      match k.n with 
          | Kind_uvar(uv, actuals) -> 
              (match find_uvar_k uv s with
                  | None -> k
                  | Some k' -> 
                      match k'.n with 
                          | Kind_lam(formals, body) -> 
                                 let k = Util.subst_kind (Util.subst_of_list formals actuals) body in
                                 compress_k env s k
                          | _ -> if List.length actuals = 0 
                                 then compress_k env s k'
                                 else failwith "Wrong arity for kind unifier")
          | _ -> k
  
  let rec compress env s t =
      let t = Util.compress_typ t in
      match t.n with 
          | Typ_uvar (uv, _) ->
             (match find_uvar_t uv s with 
                  | None -> whnf env t
                  | Some t -> compress env s t)   
          | Typ_app({n=Typ_uvar(uv, k)}, args) -> 
              (match find_uvar_t uv s with 
                  | Some t' -> 
                    let t' = compress env s t' in 
                    let t'' = mk_Typ_app(t', args) t.tk t.pos in 
                    let t''' = whnf env t'' in
                    if debug env Extreme then Util.fprint3 "Resolving uvar %s to\n\t%s\n\tnorm to %s\n" (Print.typ_to_string t) (Print.typ_to_string t'') (Print.typ_to_string t''');
                    t'''
                  | _ -> whnf env t)
          | _ -> whnf env t
  
  let rec compress_e (env:env) s e = 
      let e = Util.compress_exp e in
      match e.n with 
          | Exp_uvar (uv, t) -> 
             begin match find_uvar_e uv s with 
              | None -> e
              | Some e' -> compress_e env s e'
             end
          | Exp_app({n=Exp_uvar(uv, t)}, args) -> 
             begin match find_uvar_e uv s with 
              | None -> e
              | Some e' -> 
                  let e' = compress_e env s e' in
                  mk_Exp_app(e', args) e.tk e.pos //TODO: whnf for expressions?
             end
          | _ -> e
  
  type match_result = 
    | MisMatch
    | HeadMatch
  
negative.code:     | _ -> HeadMatch
  
  let rec head_matches env t1 t2 : match_result = 
    match (Util.unmeta_typ t1).n, (Util.unmeta_typ t2).n with 
      | Typ_btvar x, Typ_btvar y -> if Util.bvar_eq x y then FullMatch else MisMatch
      | Typ_const f, Typ_const g -> if Util.fvar_eq f g then FullMatch else MisMatch
      
      | Typ_btvar _, Typ_const _
      | Typ_const _, Typ_btvar _ -> MisMatch
  
  