anchor.diff:        let args, g' = tc_args en p in
         (args::pats, Env.conj_guard g g')) pats ([], Env.trivial_guard)
   
  -and tc_tot_or_gtot_term' (env:env) (e:term) (msg:string)
  +and tc_tot_or_gtot_term_maybe_solve_deferred (env:env) (e:term) (msg:string) (solve_deferred:bool)
   : term * lcomp * guard_t
   = let e, c, g = tc_maybe_toplevel_term env e in
     if TcComm.is_tot_or_gtot_lcomp c
     then e, c, g
  -  else let g = Rel.solve_deferred_constraints env g in
  +  else let g =
  +         if solve_deferred
  +         then Rel.solve_deferred_constraints env g
  +         else g in
          let c, g_c = TcComm.lcomp_comp c in
          let c = norm_c env c in
          let target_comp, allow_ghost =
  
positive.code:                                           (BU.string_of_int (List.length sub_pats))
                                            (BU.string_of_int (List.length simple_bvs)));
            let simple_pat_e, simple_bvs, g1, erasable =
                let simple_pat_e, simple_pat_t, simple_bvs, guard, erasable =
                    type_of_simple_pat env simple_pat_e
                in
                let g' = pat_typ_ok env simple_pat_t (expected_pat_typ env p0.p t) in
                let guard = Env.conj_guard guard g' in
                if Env.debug env <| Options.Other "Patterns"
                then BU.print3 "$$$$$$$$$$$$Checked simple pattern %s at type %s with bvs=%s\n"
  
negative.code: 
                  | Tm_uvar _ ->
                    let env = Env.set_expected_typ env t_f in
                    //
                    //AR: 03/03: When typechecking these uvar args,
                    //  we don't want to solve the deferred constraints here,
                    //  since solving them here may mean solving flex-flex equations
                    //  among them
                    //
                    //  Whereas if we wait for unification of these dot pattern uvars
                    //  with the type of the scrutinee (in pat_typ_ok), we have a good
                    //  chance of solving these uvars as flex-rigid equations
                    //
                    //  Therefore, ask tc_tot to not solve deferred, and return the
                    //  guard as is
                    //
                    let a, _, g = tc_tot_or_gtot_term_maybe_solve_deferred
                      env
                      a
                      ""
                      false in  //don't solve the deferred constraints in the guard
                    let subst = NT(f, a)::subst in
                    (a, imp_a), subst, bvs, g
  
  