anchor.diff:  //Refinement subtyping with higher-order unification 
   //with special treatment for higher-order patterns 
   //////////////////////////////////////////////////////////////////////////
  +
   type rel = 
     | EQ 
     | SUB
  -let rel_to_string = function
  -  | EQ -> "="
  -  | SUB -> "<:"
  +  | SUBINV  (* sub-typing/sub-kinding, inverted *)
  +
  +type problem<'a,'b> = {               //Try to prove: lhs rel rhs ~> guard        
  +    lhs:'a;
  +    relation:rel;   
  +    rhs:'a;
  +    element:option<'b>;               //where, guard is a predicate on this term (which appears free in/is a subterm of the guard) 
  +    closing_context:binders;          //and must be closed by this context
  +    reason: list<string>;             //why we generated this problem, for error reporting
  +    loc: Range.range;                 //and the source location where this arose
  +}
   
   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
  +  | KProb of problem<knd,typ>
  +  | TProb of problem<typ,exp>
  +  | EProb of problem<exp,unit>
  +  | CProb of problem<comp,unit>
  +
  +type probs = list<prob>
  +
  +type guard_formula = 
  +  | Trivial
  +  | NonTrivial of formula
  +
  +type guard_t = {
  +  guard_f:  guard_formula;
  +  carry:    probs
  +}
  +
  +(* Instantiation of unification variables *)
  +type uvi =  
     | 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. 
  -  *)
  +
  +(* The set of problems currently being addressed *)
  +type worklist = {
  +    attempting: probs;
  +    deferred:   list<(int * prob)>;  //flex-flex cases, non patterns, and subtyping constraints involving a unification variable, 
  +    subst:      list<uvi>;           //the partial solution derived so far
  +    guard:      guard_formula;       //the logical condition gathered so far
  +    ctr:        int;                 //a counter incremented each time we extend subst, used to detect if we've made progress
  +}
  +
  +type solution = 
  +    | Success of list<uvi> * guard_t
  +    | Failed  of prob * string
  +
  +(* ------------------------------------------------*)
  +(* <Printing> (mainly for debugging) *)
  +(* ------------------------------------------------*)
  +let rel_to_string = function
  +  | EQ -> "="
  +  | SUB -> "<:"
  +  | SUBINV -> ":>"
  +
  +
  +let prob_to_string env = function 
  +  | KProb p -> Util.format3 "\t%s\n\t\t%s\n\t%s" (Print.kind_to_string p.lhs) (rel_to_string p.relation) (Print.kind_to_string p.rhs)
  +  | TProb p -> 
  +    Util.format "\t%s (%s) \n\t\t%s\n\t%s (%s)" 
  +        [(Normalize.typ_norm_to_string env p.lhs);
  +         (Print.tag_of_typ p.lhs) ;
  +         (rel_to_string p.relation);
  +         (Normalize.typ_norm_to_string env p.rhs);
  +         (Print.tag_of_typ p.rhs)]
  +  | EProb p -> Util.format3 "\t%s \n\t\t%s\n\t%s" (Normalize.exp_norm_to_string env p.lhs) (rel_to_string p.relation) (Normalize.exp_norm_to_string env p.rhs)
  +  | CProb p -> Util.format3 "\t%s \n\t\t%s\n\t%s" (Normalize.comp_typ_norm_to_string env p.lhs) (rel_to_string p.relation) (Normalize.comp_typ_norm_to_string env p.rhs)
  +
  +let guard_to_string (env:env) g = 
  +  let form = match g.guard_f with 
  +      | Trivial -> "trivial"
  +      | NonTrivial f ->
  +          if debug env <| Options.Other "Rel" 
  +          then Normalize.formula_norm_to_string env f
  +          else "non-trivial" in
  +  let carry = List.map (prob_to_string env) g.carry |> String.concat ", " in
  +  Util.format2 "{guard_f=%s;\ndeferred=%s;}\n" form carry
  +
  +let uvi_to_string env uvi = 
  +  (* 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)>
  +  match uvi 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"
  +(* ------------------------------------------------*)
  +(* </Printing> *)
  +(* ------------------------------------------------*)
  +
  +
  +(* ------------------------------------------------*)
  +(* <guard_formula ops> Operations on guard_formula *)
  +(* ------------------------------------------------*)
  +let trivial t = match t with 
  +  | Trivial -> ()
  +  | NonTrivial _ -> failwith "impossible"
  +
  +let conj_guard g1 g2 = match g1, g2 with 
  +  | Trivial, g
  +  | g, Trivial -> g
  +  | NonTrivial f1, NonTrivial f2 -> NonTrivial (Util.mk_conj f1 f2)
  +
  +let rec close_forall bs f = match bs with 
  +    | [] -> f
  +    | b::rest -> 
  +      let body = mk_Typ_lam([b], close rest f) (mk_Kind_arrow([b], ktype) f.pos) f.pos in
  +      match fst b with 
  +        | Inl a ->
  +          mk_Typ_app(Util.tforall_typ a.sort, [targ body]) ktype f.pos
  +        | Inr x -> 
  +          mk_Typ_app(Util.tforall, [(Inl x.sort, true); targ body]) ktype f.pos
  +
  +let close_guard binders g = match g with 
  +    | Trivial -> g
  +    | NonTrivial f -> close_forall binders f |> NonTrivial
  +
  +let mk_guard g ps = {guard_f=g; carry=List.map snd ps}
  +
  +(* ------------------------------------------------*)
  +(* </guard_formula ops>                            *)
  +(* ------------------------------------------------*)
  +
  +(* ------------------------------------------------*)
  +(* <prob ops> lifting from problem to prob         *)
  +(* ------------------------------------------------*)
  +let invert_rel = function 
  +    | EQ -> EQ
  +    | SUB -> SUBINV
  +    | SUBINV -> SUB
  +let invert p       = {p with lhs=p.rhs; rhs=p.lhs; relation=invert_rel p.relation}
  +let maybe_invert p = if p.relation = SUBINV then invert p else p
  +let p_rel = function 
  +   | KProb p -> p.relation
  +   | TProb p -> p.relation
  +   | EProb p -> p.relation
  +   | CProb p -> p.relation    
  +let p_reason = function 
  +   | KProb p -> p.reason
  +   | TProb p -> p.reason
  +   | EProb p -> p.reason
  +   | CProb p -> p.reason    
  +let p_loc = function 
  +   | KProb p -> p.loc
  +   | TProb p -> p.loc
  +   | EProb p -> p.loc
  +   | CProb p -> p.loc
  +let p_context = function
  +   | KProb p -> p.closing_context
  +   | TProb p -> p.closing_context
  +   | EProb p -> p.closing_context
  +   | CProb p -> p.closing_context
  +let mk_problem orig lhs rel rhs elt bs reason = {     
  +     lhs=lhs;
  +     relation=rel;
  +     rhs=rhs;
  +     element=elt;
  +     closing_context=bs@p_context orig;
  +     reason=reason::p_reason orig;
  +     loc=p_loc orig;
  +     }
  +(* ------------------------------------------------*)
  +(* </prob ops>                                     *)
  +(* ------------------------------------------------*)
  +
  +(* ------------------------------------------------*)
  +(* <worklist ops> Operations on worklists          *)
  +(* ------------------------------------------------*)
   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 = 
  +let singleton prob         = {empty_worklist with attempting=[prob]}
  +let extend_subst' uis wl   = {wl with subst=uis@wl.subst; ctr=wl.ctr + 1}
  +let extend_subst ui wl     = {wl with subst=ui::wl.subst; ctr=wl.ctr + 1}
  +let defer prob wl          = {wl with deferred=(wl.ctr, prob)::wl.deferred}
  +let attempt probs wl       = {wl with attempting=probs@wl.attempting}
  +let guard (env:env) g wl   = {wl with guard=conj_guard g wl.guard}   
  +let giveup env reason prob = 
       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")
  +    Failed(prob, reason)
  +(* ------------------------------------------------*)
  +(* </worklist ops>                                 *)
  +(* ------------------------------------------------*)
  +
  +(* ------------------------------------------------*)
  +(* <uvi ops> Instantiating unification variables   *)
  +(* ------------------------------------------------*)
  +let commit env uvis = 
  +    uvis |> List.iter (function
  +        | UK(u,k)     -> Unionfind.change u (Fixed k)
  +        | UT((u,k),t) -> 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_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 = 
  +(* ------------------------------------------------*)
  +(* </uvi ops>                                      *)
  +(* ------------------------------------------------*)
  +
  +
  +(* ------------------------------------------------*)
  +(* <normalization>                                *)
  +(* ------------------------------------------------*)
  +let norm_targ env t = Tc.Normalize.norm_typ [Beta] env t
  +let norm_arg env a = match fst a with 
  +    | Inl t -> Inl <| norm_targ env t, snd a
  +    | Inr v -> Inr <| Tc.Normalize.norm_exp [Beta] env v, snd a
  +let whnf env t = Tc.Normalize.whnf env t |> Util.compress_typ
  +let sn env t = Tc.Normalize.norm_typ [Beta;Eta] env t |> Util.compress_typ
  +let sn_binders env binders = 
  +    binders |> List.map (function 
  +        | Inl a, imp -> 
  +          Inl ({a with sort=Tc.Normalize.norm_kind [Beta] env a.sort}), imp
  +        | Inr x, imp -> 
  +          Inr ({x with sort=norm_targ env x.sort}), imp)
  +let whnf_k env k = Tc.Normalize.norm_kind [Beta;Eta;WHNF] env k |> Util.compress_kind
  +
  +let rec compress_k (env:env) wl k = 
       let k = Util.compress_kind k in 
       match k.n with 
           | Kind_uvar(uv, actuals) -> 
  -            (match find_uvar_k uv s with
  +            (match find_uvar_k uv wl.subst 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
  +                               compress_k env wl k
                           | _ -> if List.length actuals = 0 
  -                               then compress_k env s k'
  +                               then compress_k env wl k'
                                  else failwith "Wrong arity for kind unifier")
           | _ -> k
   
  -let rec compress env s t =
  -    let t = Util.compress_typ t in
  +let rec compress env wl t =
  +    let t = Util.unmeta_typ t in
       match t.n with 
           | Typ_uvar (uv, _) ->
  -           (match find_uvar_t uv s with 
  +           (match find_uvar_t uv wl.subst 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 -> compress env wl t)   
  +        | Typ_app({n=Typ_uvar(uv, _)}, args) -> 
  +            (match find_uvar_t uv wl.subst with 
                   | Some t' -> 
  -                  let t' = compress env s t' in 
  +                  let t' = compress env wl 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)
           | _ -> whnf env t
   
  -let rec compress_e (env:env) s e = 
  -    let e = Util.compress_exp e in
  +let rec compress_e (env:env) wl e = 
  +    let e = Util.unmeta_exp e in
       match e.n with 
           | Exp_uvar (uv, t) -> 
  -           begin match find_uvar_e uv s with 
  +           begin match find_uvar_e uv wl.subst with 
               | None -> e
  -            | Some e' -> compress_e env s e'
  +            | Some e' -> compress_e env wl e'
              end
  -        | Exp_app({n=Exp_uvar(uv, t)}, args) -> 
  -           begin match find_uvar_e uv s with 
  +        | Exp_app({n=Exp_uvar(uv, _)}, args) -> 
  +           begin match find_uvar_e uv wl.subst with 
               | None -> e
               | Some e' -> 
  -                let e' = compress_e env s e' in
  +                let e' = compress_e env wl e' in
                   mk_Exp_app(e', args) e.tk e.pos //TODO: whnf for expressions?
              end
           | _ -> e
   
  +(* ------------------------------------------------ *)
  +(* </normalization>                                 *)
  +(* ------------------------------------------------ *)
  +
  +(* ------------------------------------------------ *)
  +(* <variable ops> common ops on variables           *)
  +(* ------------------------------------------------ *)
  +let occurs_check env uk t = 
  +    let uvs = Util.uvars_in_typ t in 
  +    let occurs_ok = not (Util.set_mem uk uvs.uvars_t) in
  +    let msg = 
  +        if occurs_ok then None
  +        else Some (Util.format4 "occurs-check failed (%s occurs in {%s} uvars of %s normalized to %s)" 
  +                        (Print.uvar_t_to_string uk) 
  +                        (Util.set_elements uvs.uvars_t |> List.map Print.uvar_t_to_string |> String.concat ", ")
  +                        (Print.typ_to_string t)
  +                        (Normalize.typ_norm_to_string env t)) in
  +    occurs_ok, msg
  +
  +let occurs_check_e env ut e = 
  +    let uvs = Util.uvars_in_exp e in 
  +    let occurs_ok = not (Util.set_mem ut uvs.uvars_e) in
  +    let msg = 
  +        if occurs_ok then None
  +        else Some (Util.format3 "occurs-check failed (%s occurs in {%s} uvars of %s normalized to %s)" 
  +                        (Print.uvar_e_to_string ut) 
  +                        (Util.set_elements uvs.uvars_e |> List.map Print.uvar_e_to_string |> String.concat ", ")
  +                        (Normalize.exp_norm_to_string env e)) in
  +    occurs_ok, msg
  +
  +
  +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})
  +
  +let binders_eq v1 v2 = 
  +  List.length v1 = List.length v2 
  +  && List.forall2 (fun ax1 ax2 -> match fst ax1, fst ax2 with 
  +        | Inl a, Inl b -> Util.bvar_eq a b
  +        | Inr x, Inr y -> Util.bvar_eq x y
  +        | _ -> false) v1 v2
  +
  +let rec pat_vars env seen args : option<binders> = match args with 
  +    | [] -> Some (List.rev seen) 
  +    | hd::rest -> 
  +        (match fst <| norm_arg env hd with
  +            | Inl {n=Typ_btvar a} -> 
  +               if seen |> Util.for_some (function 
  +                        | Inl b, _ -> bvd_eq a.v b.v
  +                        | _ -> false)
  +               then None //not a pattern
  +               else pat_vars env ((Inl a, snd hd)::seen) rest
  +
  +            | Inr {n=Exp_bvar x} ->
  +                if seen |> Util.for_some (function 
  +                    | Inr y, _ -> bvd_eq x.v y.v
  +                    | _ -> false)
  +                then None //not a pattern
  +                else pat_vars env ((Inr x, snd hd)::seen) rest
  +
  +            | _ -> None) //not a pattern
  +
  +(* ------------------------------------------------ *)
  +(* </variable ops>                                  *)
  +(* ------------------------------------------------ *)
  +
  +
  +(* ------------------------------------------------ *)
  +(* <decomposition> of a type/kind with its binders  *)
  +(* ------------------------------------------------ *)
  +(*
  +    It simplifies the unification algorithm to view every F* term/type/kind
  +    as either a lambda, a variable, or the application of a constructor to some arguments.
  +    
  +    For the built-in term formers, i.e., Typ_fun, Typ_refine, and Kind_arrow, 
  +    we need a way to decompose them into their sub-terms so that they 
  +    appear in the form (C arg1 ... argn), for some constructor C.
  +     
  +    We call this operation 'decomposition'.
  +
  +    To illustrate, take:
  +
  +    val decompose_typ: env -> typ 
  +                    -> (list<ktec> -> typ) 
  +                        * (typ -> bool) 
  +                        * list<(binders * ktec)>
  +
  +    let recompose, matches, components = decompose_typ env t
  +        
  +        1. The components are the immediate sub-terms of t, 
  +           with their contexts provided as a binders
  +           
  +           For example: if t = x1:t1 -> ... -> xn:tn -> C
  +           the components are ([([], t1); ... ([(x1..xn-1)], tn); ([(x1..xn)], C)]
  +
  +        2. recompose is a function that rebuilds a t-like type from new subterms
  +           
  +           In our example, rebuild [s1;...;sn; C'] builds
  +                           x1:s1 -> ... -> xn:sn -> C'
  +           The shape of the argument to rebuild must match the shape of the components of t
  +
  +        3. matches is function which decides whether or not 
  +           a given type t' could be structurally similar to t (modulo reduction). It serves
  +           as a proxy for the constructor C itself
  +
  +           For example, any Typ_fun full matches t
  +                        any Uvar    head matches t
  +                        any Typ_lam head matches t
  +                        any (t1 t2) head matches t, if t1 matches t
  +              
  +           where t matches t' 
  +              if t head matches t'
  +              or t full matches t'
  +            
  + *)
   type match_result = 
     | MisMatch
     | HeadMatch
  
positive.code: open Microsoft.FStar.Tc.Normalize
  open Microsoft.FStar.Absyn.Syntax
  
  let norm_targ env t = Tc.Normalize.norm_typ [Beta] env t
  let whnf env t = Tc.Normalize.whnf env t |> Util.compress_typ
  let sn env t = Tc.Normalize.norm_typ [Beta;Eta] env t |> Util.compress_typ
  let sn_binders env binders = 
      binders |> List.map (function 
          | Inl a, imp -> 
            Inl ({a with sort=Tc.Normalize.norm_kind [Beta] env a.sort}), imp
          | Inr x, imp -> 
            Inr ({x with sort=norm_targ env x.sort}), imp)
  let whnf_k env k = Tc.Normalize.norm_kind [Beta;Eta;WHNF] env k |> Util.compress_kind
  let destruct_flex_t t = match t.n with
      | Typ_uvar(uv, k) -> (t, uv, k, [])
      | Typ_app({n=Typ_uvar(uv, k)}, args) -> (t, uv, k, args)
      | _ -> failwith "Not a flex-uvar"
  
  (**********************************************************************************************************************)
  (* Relations (equality and subsumption) between kinds, types, expressions and computations *)
  (**********************************************************************************************************************)
  type guard_t = 
    | Trivial
    | NonTrivial of formula
  
  let rec is_trivial f : bool = 
      let bin_op f l = match l with 
          | [(Inl t1, _); (Inl t2, _)] -> f t1 t2
          | _ -> failwith "Impossible" in
      let connectives = [(Const.and_lid, bin_op (fun t1 t2 -> is_trivial t1 && is_trivial t2));
                         (Const.or_lid,  bin_op (fun t1 t2 -> is_trivial t1 || is_trivial t2));
                         (Const.imp_lid, bin_op (fun t1 t2 -> is_trivial t2));
                         (Const.true_lid, (fun _ -> true));
                         (Const.false_lid, (fun _ -> false));
                         ] in
  
      let fallback phi = match phi.n with 
          | Typ_lam(_, phi) -> is_trivial phi
          | _ -> false in
  
      match Util.destruct_typ_as_formula f with 
          | None -> fallback f
          | Some (BaseConn(op, arms)) -> 
             (match connectives |> List.tryFind (fun (l, _) -> lid_equals op l) with 
               | None -> false
               | Some (_, f) -> f arms)
          | Some (QAll(_, _, body)) 
          | Some (QEx(_, _, body)) -> is_trivial body
    
  let simplify_guard (env:env) g =
    match g with 
      | Trivial -> g
      | NonTrivial f -> 
        //let f = Tc.Normalize.normalize env f in //NS: EXPENSIVE!
        if is_trivial f 
        then Trivial
        else NonTrivial f
  
  let guard_to_string (env:env) = function  
    | Trivial -> "trivial"
    | NonTrivial f ->
        if debug env Medium then
          Normalize.formula_norm_to_string env f
        else
          "non-trivial"
  
  let trivial t = match t with 
    | Trivial -> ()
    | NonTrivial _ -> failwith "impossible"
  
  let conj_guard g1 g2 = match g1, g2 with 
    | Trivial, g
    | g, Trivial -> g
    | NonTrivial f1, NonTrivial f2 -> NonTrivial (Util.mk_conj f1 f2)
  
  let rec close bs f = match bs with 
      | [] -> f
      | (Inl a, _)::rest -> 
        mk_Typ_app(Util.tforall_typ a.sort, [targ <| close rest f]) ktype f.pos
      | (Inr x, _)::rest -> 
        mk_Typ_app(Util.tforall, [targ <| close rest f]) ktype f.pos
  
  let close_guard binders g = match g with 
      | Trivial -> g
      | NonTrivial f -> close binders 
                      (mk_Typ_lam(binders, f) (mk_Kind_arrow(binders, f.tk) f.pos) f.pos) |> NonTrivial
          
  //////////////////////////////////////////////////////////////////////////
  //Making substitutions for alpha-renaming 
  //////////////////////////////////////////////////////////////////////////
  
negative.code:                  solve env ({probs with attempting=sub::probs.attempting})
          | _ -> giveup_noex probs
  
  
  
  and solve_t_flex_flex (top:bool) (env:Tc.Env.env) (orig:prob) 
                        (lhs:flex_t) (rhs:flex_t) (probs:worklist) : solution = 
  