anchor.diff:  // |- a = ?u
   // |- ?u = c
   //
  -// without asking for ?u first, which will most likely be instantiated when
  -// solving any of these two goals. In any case, if ?u is not solved, we fail afterwards.
  +// without asking for |- ?u : Type first, which will most likely be instantiated when
  +// solving any of these two goals. In any case, if ?u is not solved, we will later fail.
   // TODO: this should probably be made into a user tactic
  -let rec __apply (uopt:bool) (tm:term) (typ:typ) : tac<unit> =
  -    bind (cur_goal ()) (fun goal ->
  -    mlog (fun () -> BU.print1 ">>> Calling __exact(%s)\n" (Print.term_to_string tm)) (fun () ->
  -    bind (trytac_exn (with_policy Force (t_exact false tm))) (function
  -    | Some r -> ret r // if tm is a solution, we're done
  -    | None ->
  -        // exact failed, try to instantiate more arguments
  -        mlog (fun () -> BU.print1 ">>> typ = %s\n" (Print.term_to_string typ)) (fun () ->
  -        match U.arrow_one typ with
  -        | None -> raise NoUnif
  -        | Some ((bv, aq), c) ->
  -            mlog (fun () ->
  -                BU.print1 "__apply: pushing binder %s\n" (Print.binder_to_string (bv, aq))) (fun _ ->
  -            if not (U.is_total_comp c) then fail "apply: not total codomain" else
  -            bind (new_uvar "apply" (goal_env goal) bv.sort) (fun (u, _goal_u) ->
  -            (* BU.print1 "__apply: witness is %s\n" (Print.term_to_string u); *)
  -            let tm' = mk_Tm_app tm [(u, aq)] None tm.pos in
  -            let typ' = SS.subst [S.NT (bv, u)] <| comp_to_typ c in
  -            bind (__apply uopt tm' typ') (fun _ ->
  -            let u = bnorm (goal_env goal) u in
  -            match (SS.compress (fst (U.head_and_args u))).n with
  -            | Tm_uvar (goal_u, _) ->
  -                bind get (fun ps ->
  -                if uopt && uvar_free goal_u.ctx_uvar_head ps
  -                then ret ()
  -                else begin
  -                    (* BU.print2 "__apply: adding goal %s : %s\n" (Print.term_to_string u) *)
  -                    (*                                            (Print.term_to_string bv.sort); *)
  -                    add_goals [bnorm_goal ({ goal with
  -                                             goal_ctx_uvar = goal_u;
  -                                             is_guard = false; })]
  -                end)
  -            | t -> begin
  -                (* BU.print1 "__apply: uvar was instantiated to %s\n" (Print.term_to_string u); *)
  -                ret ()
  -                end
  -            )))))))
  -
  -// The exception is thrown only when the tactic runs, not when it's defined,
  -// so we need to do this to catch it
  -let try_unif (t : tac<'a>) (t' : tac<'a>) : tac<'a> =
  -    mk_tac (fun ps ->
  -        try run t ps
  -        with NoUnif -> run t' ps)
  -
   let apply (uopt:bool) (tm:term) : tac<unit> = wrap_err "apply" <|
       mlog (fun () -> BU.print1 "apply: tm = %s\n" (Print.term_to_string tm)) (fun _ ->
       bind (cur_goal ()) (fun goal ->
  -    bind (__tc (goal_env goal) tm) (fun (tm, typ, guard) ->
  +    let e = goal_env goal in
  +    bind (__tc e tm) (fun (tm, typ, guard) ->
       // Focus helps keep the goal order
  -    let typ = bnorm (goal_env goal) typ in
  -    try_unif (focus (bind (__apply uopt tm typ) (fun _ -> proc_guard "apply guard" (goal_env goal) guard)))
  -             (fail3 "Cannot instantiate %s (of type %s) to match goal (%s)"
  -                            (tts (goal_env goal) tm)
  -                            (tts (goal_env goal) typ)
  -                            (tts (goal_env goal) (goal_type goal)))
  -    )))
  +    let typ = bnorm e typ in
  +    bind (try_match_by_application e typ (goal_type goal)) (fun uvs ->
  +    let w = List.fold_right (fun (uvt, q, _) w -> U.mk_app w [(uvt, q)]) uvs tm in
  +
  +    let uvset = List.fold_right (fun (_, _, uv) s -> BU.set_union s (SF.uvars uv.ctx_uvar_typ)) uvs (SF.new_uv_set ()) in
  +    let free_in_some_goal uv =
  +        BU.set_mem uv uvset
  +    in
  +    bind (solve' goal w) (fun () ->
  +    bind (mapM (fun (uvt, q, uv) ->
  +                 match UF.find uv.ctx_uvar_head with
  +                 (* Already (at least partially) solved, skip asking the user for it *)
  +                 | Some _ ->
  +                       ret ()
  +                 (* Not instantiated at all *)
  +                 | None ->
  +                    (* We might still not add it if uopt is on, as described above *)
  +                    if uopt && free_in_some_goal uv
  +                    then ret ()
  +                    else add_goals [bnorm_goal ({ goal with
  +                                                  goal_ctx_uvar = uv;
  +                                                  is_guard = false; })]
  +               ) uvs) (fun _ ->
  +    proc_guard "apply guard" e guard
  +    ))))))
   
   // returns pre and post
   let lemma_or_sq (c : comp) : option<(term * term)> =
  
positive.code:     | Inr r -> ret r
      | Inl _ -> fail e)))) // keep original error
  
  let uvar_free_in_goal (u:uvar) (g:goal) =
      if g.is_guard then false else
      let free_uvars = List.map (fun u -> u.ctx_uvar_head) (BU.set_elements (SF.uvars (goal_type g))) in
      List.existsML (UF.equiv u) free_uvars
  
  let uvar_free (u:uvar) (ps:proofstate) : bool =
      List.existsML (uvar_free_in_goal u) ps.goals
  
  let rec mapM (f : 'a -> tac<'b>) (l : list<'a>) : tac<list<'b>> =
      match l with
      | [] -> ret []
  
negative.code:         bind (mapM f xs) (fun ys ->
          ret (y::ys)))
  
  let rec  __try_match_by_application (acc : list<(term * aqual * ctx_uvar)>)
                                      (e : env) (ty1 : term) (ty2 : term)
                                          : tac<list<(term * aqual * ctx_uvar)>> =
      bind (do_unify e ty1 ty2) (function
      | true ->
          (* Done! *)
          ret acc
      | false -> begin
          (* Not a match, try instantiating the first type by application *)
          match U.arrow_one ty1 with
          | None ->
              fail2 "Could not instantiate, %s to %s" (Print.term_to_string ty1) (Print.term_to_string ty2)
          | Some (b, c) ->
              if not (U.is_total_comp c) then fail "Codomain is effectful" else
              bind (new_uvar "apply arg" e (fst b).sort) (fun (uvt, uv) ->
              let typ = comp_to_typ c in
              let typ' = SS.subst [S.NT (fst b, uvt)] typ in
              __try_match_by_application ((uvt, snd b, uv)::acc) e typ' ty2)
      end)
  
  (* Can t1 match t2 if it's applied to arguments? If so return uvars for them *)
  (* NB: Result is reversed, which helps so we use fold_right instead of fold_left *)
  let try_match_by_application (e : env) (ty1 : term) (ty2 : term) : tac<list<(term * aqual * ctx_uvar)>> =
      __try_match_by_application [] e ty1 ty2
  
  // uopt: Don't add goals for implicits that appear free in posterior goals.
  // This is very handy for users, allowing to turn
  