Tc: fix context push/pop in #check

Use the proper API to reset the id_info_table, or this will crash in IDE
mode. Also descend into the terms in VisitM.

Author: mtzguido

src/syntax/FStarC.Syntax.VisitM.fst

@@ -437,7 +437,10 @@ let rec on_sub_sigelt' #m {|d : lvm m |} (se : sigelt') : m sigelt' =
     // ^ review: residual flags should not have terms
     return <| Sig_effect_abbrev {lid; us; bs; comp; cflags}
 
-  (* No content *)
+  (* No content, except for Check. *)
+  | Sig_pragma (Check t) ->
+    let! t = f_term t in
+    return <| Sig_pragma (Check t)
   | Sig_pragma _ -> return se
 
   | Sig_polymonadic_bind {m_lid; n_lid; p_lid; tm; typ; kind} ->

src/typechecker/FStarC.TypeChecker.Tc.fst

@@ -920,6 +920,16 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env =
     [se], [], env0)
 
 
+let snapshot_context env msg = BU.atomically (fun () ->
+    TypeChecker.Env.snapshot env msg)
+
+let rollback_context solver msg depth : env = BU.atomically (fun () ->
+    let env = TypeChecker.Env.rollback solver msg depth in
+    env)
+
+let push_context env msg = snd (snapshot_context env msg)
+let pop_context env msg = rollback_context env.solver msg None
+
 (* [tc_decl env se] typechecks [se] in environment [env] and returns
  * the list of typechecked sig_elts, and a list of new sig_elts elaborated
  * during typechecking but not yet typechecked. This may also be called
@@ -1013,6 +1023,7 @@ let add_sigelt_to_env (env:Env.env) (se:sigelt) (from_cache:bool) : Env.env =
       env
 
     | Sig_pragma (Check t0) ->
+      let env = push_context env "#check" in
       let tx = UF.new_transaction () in
       let t, lc, g = tc_term { env with instantiate_imp = false } t0 in
       let c, g' = lcomp_comp lc in
@@ -1028,7 +1039,7 @@ let add_sigelt_to_env (env:Env.env) (se:sigelt) (from_cache:bool) : Env.env =
             empty
         ]
       );
-      UF.rollback tx;
+      let env = pop_context env "#check" in
       env
 
     | Sig_new_effect ne ->
@@ -1176,16 +1187,6 @@ let tc_decls env ses =
 let _ =
     tc_decls_knot := Some tc_decls
 
-let snapshot_context env msg = BU.atomically (fun () ->
-    TypeChecker.Env.snapshot env msg)
-
-let rollback_context solver msg depth : env = BU.atomically (fun () ->
-    let env = TypeChecker.Env.rollback solver msg depth in
-    env)
-
-let push_context env msg = snd (snapshot_context env msg)
-let pop_context env msg = rollback_context env.solver msg None
-
 let tc_partial_modul env modul =
   let verify = Options.should_verify (string_of_lid modul.name) in
   let action = if verify then "verifying" else "lax-checking" in