Merge pull request #3414 from mtzguido/refactor2

A bit more refactor

src/syntax/FStar.Syntax.Print.fst

@@ -1016,6 +1016,11 @@ instance showable_pat    = { show = pat_to_string; }
 instance showable_const  = { show = const_to_string; }
 instance showable_letbinding  = { show = lb_to_string; }
 instance showable_modul       = { show = modul_to_string; }
+instance showable_ctx_uvar_meta = {
+  show = (function
+          | Ctx_uvar_meta_attr attr -> "Ctx_uvar_meta_attr " ^ show attr
+          | Ctx_uvar_meta_tac r -> "Ctx_uvar_meta_tac " ^ show r);
+}
 
 instance pretty_term     = { pp   = term_to_doc; }
 instance pretty_univ     = { pp   = univ_to_doc; }

src/syntax/FStar.Syntax.Print.fsti

@@ -107,6 +107,7 @@ instance val showable_pat       : showable pat
 instance val showable_const     : showable sconst
 instance val showable_letbinding : showable letbinding
 instance val showable_modul      : showable modul
+instance val showable_ctx_uvar_meta : showable ctx_uvar_meta_t
 
 instance val pretty_term        : pretty term
 instance val pretty_univ        : pretty universe

src/typechecker/FStar.TypeChecker.DeferredImplicits.fst

@@ -182,9 +182,9 @@ let find_user_tac_for_uvar env (u:ctx_uvar) : option sigelt =
     | _ -> None
 
 let should_defer_uvar_to_user_tac env (u:ctx_uvar) =
-  if not env.enable_defer_to_tac then false
-  else Option.isSome (find_user_tac_for_uvar env u)
-
+  if not env.enable_defer_to_tac
+  then false
+  else Some? (find_user_tac_for_uvar env u)
 
 let solve_goals_with_tac env g (deferred_goals:implicits) (tac:sigelt) =
   Profiling.profile (fun () ->

src/typechecker/FStar.TypeChecker.Env.fst

@@ -2021,6 +2021,21 @@ let new_implicit_var_aux reason r env k should_check meta =
 
 (***************************************************)
 
+let uvar_meta_for_binder (b:binder) : option ctx_uvar_meta_t =
+  let { binder_bv=x; binder_qual=qual; binder_attrs=attrs } = b in
+  match qual, attrs with
+  | Some (Meta tau), _ ->
+    Some (Ctx_uvar_meta_tac tau)
+  | _, attr::_ ->
+    (* NB: it does not have to be marked Implicit to get a
+    Ctx_uvar_meta_attr. In practice most of them are (or
+    the typechecker will not decide to instantiate) but the
+    layered effects checking code will sometimes call this
+    function on regular explicit binders. *)
+    Some (Ctx_uvar_meta_attr attr)
+  | _, _ ->
+    None
+
 //
 // Perhaps this should not return a guard,
 //   but only a list of implicits, so that callers don't have to
@@ -2030,19 +2045,15 @@ let uvars_for_binders env (bs:S.binders) substs reason r =
   bs |> List.fold_left (fun (substs, uvars, g) b ->
     let sort = SS.subst substs b.binder_bv.sort in
 
-    let ctx_uvar_meta_t =
-      match b.binder_qual, b.binder_attrs with
-      | Some (Meta t), [] ->
-        Some (Ctx_uvar_meta_tac t)
-      | _, t::_ -> Some (Ctx_uvar_meta_attr t)
-      | _ -> None in
+    let ctx_uvar_meta = uvar_meta_for_binder b in
 
     let t, l_ctx_uvars, g_t = new_implicit_var_aux
       (reason b) r env sort
       (if Options.compat_pre_typed_indexed_effects ()
        then Allow_untyped "indexed effect uvar in compat mode"
        else Strict)
-      ctx_uvar_meta_t in
+      ctx_uvar_meta
+    in
 
     if !dbg_LayeredEffectsEqns
     then List.iter (fun (ctx_uvar, _) ->

src/typechecker/FStar.TypeChecker.Env.fsti

@@ -512,6 +512,8 @@ val new_implicit_var_aux : string ->
                            option ctx_uvar_meta_t ->
                            (term & list (ctx_uvar & Range.range) & guard_t)
 
+val uvar_meta_for_binder (b:binder) : option ctx_uvar_meta_t
+
 (* layered effect utils *)
 
 (*

src/typechecker/FStar.TypeChecker.Util.fst

@@ -1043,11 +1043,8 @@ let ad_hoc_indexed_bind_substs env
          match (SS.compress t).n with
          | Tm_uvar (u, _ ) ->
            BU.print2 "Generated uvar %s with attribute %s\n"
-             (Print.term_to_string t)
-             (match u.ctx_uvar_meta with
-              | Some (Ctx_uvar_meta_attr a) -> Print.term_to_string a
-              | _ -> "<no attr>")
-         | _ -> failwith ("Impossible, expected a uvar, got : " ^ Print.term_to_string t));
+             (show t) (show u.ctx_uvar_meta)
+         | _ -> failwith ("Impossible, expected a uvar, got : " ^ show t));
 
   let subst = List.map2
     (fun b t -> NT (b.binder_bv, t))
@@ -2849,16 +2846,8 @@ let instantiate_one_binder (env:env_t) (r:Range.range) (b:binder) : term & typ &
   if Debug.high () then
     BU.print1 "instantiate_one_binder: Instantiating implicit binder %s\n" (show b);
   let (++) = Env.conj_guard in
-  let { binder_bv=x; binder_qual=qual; binder_attrs=attrs } = b in
-  let ctx_uvar_meta =
-      match qual, attrs with
-      | Some (Meta tau), _ ->
-        Some (Ctx_uvar_meta_tac tau)
-      | Some (Implicit _), attr::_ ->
-        Some (Ctx_uvar_meta_attr attr)
-      | _, _ ->
-        None
-  in
+  let { binder_bv=x } = b in
+  let ctx_uvar_meta = uvar_meta_for_binder b in (* meta/attrs computed here *)
   let t = x.sort in
   let varg, _, implicits =
     let msg =