anchor.diff:  
       imps, b
   
  -type check_implicit_solution_t =
  -  | Implicit_visit_later
  -  | Implicit_checked of guard_t
  -
   (*
    * Check that an implicit solution t has expected uvar type k
    *   we know that G |- t : (G)Tot k', for some k'
    *
    * must_tot : if t must be a Tot (i.e. it must not be a GTot)
  - * later_if_univ_constraint : if typechecking the solution returns a deferred universe constraint, then
  - *                            return Implicit_visit_later
    *)
  -let check_implicit_solution_maybe_fastpath env t k (must_tot:bool) (later_if_univ_constraint:bool)
  -  : check_implicit_solution_t =
  -
  -  let check_implicit_solution_fastpath env t k must_tot : option<check_implicit_solution_t> =
  +let check_implicit_solution_maybe_fastpath env t k (must_tot:bool) : guard_t =
  +  let check_implicit_solution_fastpath env t k must_tot : option<guard_t> =
       (*
        * AR: when we create lambda terms as solutions to implicits (in u_abs),
        *       we set the type in the residual comp to be the type of the uvar
  
positive.code:     let env = Env.set_expected_typ ({env with use_bv_sorts=true}) k in
      BU.print1 "Fast path failed for %s\n" (Print.term_to_string t);
      let _, _, g = env.typeof_tot_or_gtot_term env t must_tot in
      Implicit_checked g
  
  let rec resolve_implicits' env is_tac g =
    let rec unresolved ctx_u =
      match (Unionfind.find ctx_u.ctx_uvar_head) with
      | Some r ->
          begin match ctx_u.ctx_uvar_meta with
          | None -> false
          (* If we have a meta annotation, we recurse to see if the uvar
           * is actually solved, instead of being resolved to yet another uvar.
           * In that case, while we are keeping track of that uvar, we must not
           * forget the meta annotation in case this second uvar is not solved.
           * See #1561. *)
          | Some _ ->
              begin match (SS.compress r).n with
              | Tm_uvar (ctx_u', _) -> unresolved ctx_u'
              | _ -> false
              end
          end
      | None -> true
    in
    let rec until_fixpoint (later_if_univ_constraint:bool)
                           (acc: Env.implicits * bool)
                           (implicits:Env.implicits) : Env.implicits =
      let out, changed = acc in
      let until_fixpoint = until_fixpoint later_if_univ_constraint in  //for recursive calls
      match implicits with
      | [] ->
        if not changed
        then let out, changed = try_solve_single_valued_implicits env is_tac out in
             if changed then until_fixpoint ([], false) out
             else out
        else until_fixpoint ([], false) out
      | hd::tl ->
            let { imp_reason = reason; imp_tm = tm; imp_uvar = ctx_u; imp_range = r } = hd in
            if ctx_u.ctx_uvar_should_check = Allow_unresolved
            then until_fixpoint (out, true) tl
            else if unresolved ctx_u
            then begin match ctx_u.ctx_uvar_meta with
                 | Some (Ctx_uvar_meta_tac (env_dyn, tau)) ->
                      let env : Env.env = FStar.Dyn.undyn env_dyn in
                      if Env.debug env (Options.Other "Tac") then
                          BU.print1 "Running tactic for meta-arg %s\n" (Print.ctx_uvar_to_string ctx_u);
  
                      let t =
                        Errors.with_ctx "Running tactic for meta-arg"
                          (fun () -> env.synth_hook env hd.imp_uvar.ctx_uvar_typ tau)
                      in
                      // let the unifier handle setting the variable
                      let extra =
                          match teq_nosmt env t tm with
                          | None -> failwith "resolve_implicits: unifying with an unresolved uvar failed?"
                          | Some g -> g.implicits
                      in
                      let ctx_u = { ctx_u with ctx_uvar_meta = None } in
                      let hd = { hd with imp_uvar = ctx_u } in
                      until_fixpoint (out, true) (extra @ tl)
                 | _ ->
                      until_fixpoint (hd::out, changed) tl
  
                 end
            else if ctx_u.ctx_uvar_should_check = Allow_untyped
            then until_fixpoint (out, true) tl
            else begin
              let env = {env with gamma=ctx_u.ctx_uvar_gamma} in
              let tm = norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.8" [Env.Beta] env tm in
              (*
               * AR: We do not retypecheck the solutions solved by a tactic
               *     However we still check that any uvars remaining in those solutions
               *       are Allow_unresolved
               *)
              let tm_ok_for_tac tm =
                tm
                |> Free.uvars
                |> BU.set_elements
                |> List.for_all (fun uv -> uv.ctx_uvar_should_check = Allow_unresolved) in
              if is_tac then if tm_ok_for_tac tm
                             then until_fixpoint (out, true) tl        //Move on to the next imp
                             else until_fixpoint (hd::out, changed) tl  //Move hd to out
              else begin
                //typecheck the solution
                if Env.debug env <| Options.Other "Rel"
                then BU.print5 "Checking uvar %s resolved to %s at type %s, introduce for %s at %s\n"
                                (Print.uvar_to_string ctx_u.ctx_uvar_head)
                                (Print.term_to_string tm)
                                (Print.term_to_string ctx_u.ctx_uvar_typ)
                                reason
                                (Range.string_of_range r);
  
                let g =
                  let must_tot = not (env.phase1 || env.lax || ctx_u.ctx_uvar_should_check = Allow_ghost) in
                  Errors.with_ctx (BU.format3 "While checking implicit %s set to %s of expected type %s"
                                                (Print.uvar_to_string ctx_u.ctx_uvar_head)
                                                (N.term_to_string env tm)
                                                (N.term_to_string env ctx_u.ctx_uvar_typ))
                                  (fun () -> check_implicit_solution_maybe_fastpath
                                            env tm ctx_u.ctx_uvar_typ must_tot later_if_univ_constraint) in
  
                match g with
                | Implicit_visit_later -> until_fixpoint (hd::out, changed) tl  //Move hd to out
                | Implicit_checked g ->
                  let g' =
                    (match discharge_guard' (Some (fun () ->
                             BU.format4 "%s (Introduced at %s for %s resolved at %s)"
                               (Print.term_to_string tm)
                               (Range.string_of_range r)
                               reason
                               (Range.string_of_range tm.pos))) env g true with
                     | Some g -> g
                     | None -> failwith "Impossible, with use_smt = true, discharge_guard' must return Some") in
                
                until_fixpoint (g'.implicits@out, true) tl
              end
          end
    in
  
    (*
  
negative.code:    *     we end up applying the umax heuristic too eagerly, which fails later on, and requires annotations
     *   With this 2-phase solving, we allow for more delay in these constraints
     *)
    let imps = g.implicits |> until_fixpoint ([], false) in  //first round, don't solve deferred universe constraints
    {g with implicits=imps}
  
  let resolve_implicits env g =
  