Ensure type decls are types

src/fstar/FStarC.CheckedFiles.fst

@@ -36,7 +36,7 @@ let dbg = Debug.get_toggle "CheckedFiles"
  * detect when loading the cache that the version number is same
  * It needs to be kept in sync with Prims.fst
  *)
-let cache_version_number = 72
+let cache_version_number = 73
 
 (*
  * Abbreviation for what we store in the checked files (stages as described below)

src/smtencoding/FStarC.SMTEncoding.Solver.fst

@@ -55,10 +55,6 @@ let dbg_SMTFail  = Debug.get_toggle "SMTFail"
 // The type definition is now in [FStarC.Compiler.Util], since it needs to be visible to
 // both the F# and OCaml implementations.
 
-type z3_replay_result = either (option UC.unsat_core), error_labels
-let z3_result_as_replay_result = function
-    | Inl l -> Inl l
-    | Inr (r, _) -> Inr r
 let recorded_hints : ref (option hints) = BU.mk_ref None
 let replaying_hints: ref (option hints) = BU.mk_ref None
 

src/syntax/FStarC.Syntax.Syntax.fst

@@ -353,7 +353,8 @@ let default_sigmeta = {
     sigmeta_spliced=false;
     sigmeta_admit=false;
     sigmeta_already_checked=false;
-    sigmeta_extension_data=[]
+    sigmeta_extension_data=[];
+    sigmeta_is_typ_abbrev=false;
 }
 let mk_sigelt (e: sigelt') = { 
     sigel = e;
@@ -626,6 +627,11 @@ instance hasRange_binder : hasRange binder = {
   setPos = (fun r b -> { b with binder_bv = setPos r b.binder_bv });
 }
 
+instance hasRange_letbinding : hasRange letbinding = {
+  pos = (fun lb -> lb.lbpos);
+  setPos = (fun r lb -> { lb with lbpos = r });
+}
+
 instance showable_lazy_kind = {
   show = (function
           | BadLazy -> "BadLazy"

src/syntax/FStarC.Syntax.Syntax.fsti

@@ -651,7 +651,10 @@ type sig_metadata = {
     sigmeta_already_checked:bool;
     // ^ This sigelt was created from a splice_t with a proof of well-typing,
     // and does not need to be checked again.
-    sigmeta_extension_data: list (string & dyn) //each extension can register some data with a sig
+    sigmeta_extension_data: list (string & dyn); //each extension can register some data with a sig
+    sigmeta_is_typ_abbrev:bool;
+    // ^ true iff this sigelt is a `type t = expr` decl, to trigger a
+    // final check that expr is indeed a type (see #2933).
 }
 
 
@@ -941,6 +944,7 @@ instance val has_range_sigelt : hasRange sigelt
 instance val hasRange_fv : hasRange fv
 instance val hasRange_bv     : hasRange bv
 instance val hasRange_binder : hasRange binder
+instance val hasRange_letbinding : hasRange letbinding
 
 instance val showable_emb_typ : showable emb_typ
 instance val showable_delta_depth : showable delta_depth

src/tosyntax/FStarC.ToSyntax.ToSyntax.fst

@@ -2904,7 +2904,7 @@ let mk_typ_abbrev env d lid uvs typars kopt t lids quals rng =
     { sigel = Sig_let {lbs=(false, [lb]); lids};
       sigquals = quals;
       sigrng = rng;
-      sigmeta = default_sigmeta ;
+      sigmeta = { default_sigmeta with sigmeta_is_typ_abbrev = true };
       sigattrs = U.deduplicate_terms (val_attrs @ attrs);
       sigopts = None;
       sigopens_and_abbrevs = opens_and_abbrevs env

src/typechecker/FStarC.TypeChecker.Normalize.fst

@@ -3243,16 +3243,16 @@ let get_n_binders' (env:Env.env) (steps : list step) (n:int) (t:term) : list bin
       (bs, c)
 
     (* Exactly what we wanted, return *)
-    | bs, c when len = n ->
+    | bs, c when n >= 0 && len = n ->
       (bs, c)
 
     (* Plenty of binders, grab as many as needed and finish *)
-    | bs, c when len > n ->
+    | bs, c when n >= 0 && len > n ->
       let bs_l, bs_r = List.splitAt n bs in
       (bs_l, S.mk_Total (U.arrow bs_r c))
 
     (* We need more, descend if `c` is total *)
-    | bs, c when len < n && U.is_total_comp c && not (U.has_decreases c) ->
+    | bs, c when U.is_total_comp c && not (U.has_decreases c) ->
       let (bs', c') = aux true (n-len) (U.comp_result c) in
       (bs@bs', c')
 

src/typechecker/FStarC.TypeChecker.Normalize.fsti

@@ -73,8 +73,10 @@ val has_extract_as_attr : Env.env -> Ident.lid -> option term
 val reflection_env_hook : ref (option Env.env)
 
 (* Destructs the term as an arrow type and returns its binders and
-computation type. Only grabs up to [n] binders, and normalizes only as
-needed to discover the shape of the arrow. The binders are opened. *)
+computation type. If [n] is non-negative, this function only grabs up to
+[n] binders, and normalizes only as needed to discover the shape of the
+arrow. If [n] is negative it will keep unfolding and normalizing until
+it is no longer possible. The returned binders are opened. *)
 val get_n_binders : Env.env -> int -> term -> list binder & comp
 
 val maybe_unfold_head : Env.env -> term -> option term

src/typechecker/FStarC.TypeChecker.Tc.fst

@@ -887,8 +887,31 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env =
                                                          kind=Some k} }) in
     [se], [], env0)
 
+let tc_decl_post env (res : list sigelt & list sigelt & Env.env) : unit =
+  (* Do the post-tc attribute/qualifier check. *)
+  let (ses, _, _) = res in
+  List.iter (Quals.check_sigelt_quals_post env) ses;
+
+  (* Check that all `type t = ...` indeed define types. *)
+  let is_type_arr univs t =
+    let univs, t = SS.open_univ_vars univs t in
+    let env = Env.push_univ_vars env univs in
+    let bs, ret = N.get_n_binders env (-1) t in
+    S.is_type (U.comp_result ret)
+  in
+  ses |> List.iter  (fun se ->
+    if se.sigmeta.sigmeta_is_typ_abbrev then
+      match se.sigel with
+      | Sig_let {lbs=(_, [lb])} ->
+        if not (is_type_arr lb.lbunivs lb.lbtyp) then
+          Errors.log_issue lb Error_InductiveAnnotNotAType [
+            text "`type` declarations must define types.";
+          ]
+      | _ -> failwith "gg unexpected"
+  );
+  ()
 
-(* [tc_decl env se] typechecks [se] in environment [env] and returns *
+(* [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 *)
 let tc_decl env se: list sigelt & list sigelt & Env.env =
@@ -915,11 +938,8 @@ let tc_decl env se: list sigelt & list sigelt & Env.env =
     ) else
       tc_decl' env se
   in
-  let () =
-    (* Do the post-tc attribute/qualifier check. *)
-    let (ses, _, _) = result in
-    List.iter (Quals.check_sigelt_quals_post env) ses
-  in
+  (* Post checks, may log errors. *)
+  tc_decl_post env result;
   (* Restore admit *)
   let result =
     let ses, ses_e, env = result in

tests/bug-reports/closed/Bug2933.fst

@@ -0,0 +1,4 @@
+module Bug2933
+
+[@@expect_failure [309]]
+type t = 123

tests/micro-benchmarks/BinderAttributes.fst

@@ -9,7 +9,7 @@ let default_to (def : 'a) (x : option 'a) : Tot 'a =
     | None -> def
     | Some a -> a
 
-type description (d : string) = ()
+let description (d : string) = ()
 
 type inductive_example =
     | CaseExplicit : [@@@ description "x"] x:int -> [@@@ description "y"] y:string -> inductive_example

tests/micro-benchmarks/MultipleAttributesBinder.fst

@@ -7,9 +7,9 @@ type attr_value =
     | String : v:string -> attr_value
     | Int : v:int -> attr_value
 
-type attr1 (v : string) = ()
-type attr2 (v : int) = ()
-type attr3 (v : attr_value) = ()
+let attr1 (v : string) = ()
+let attr2 (v : int) = ()
+let attr3 (v : attr_value) = ()
 
 let f (#[@@@ attr1 "imp"; attr2 1; attr3 (String "x")] x_imp:int) ([@@@ attr1 "exp"; attr2 2; attr3 (String "y")] y:string) : Tot unit =
     ()

tests/micro-benchmarks/RecordFieldAttributes.fst

@@ -2,7 +2,7 @@ module RecordFieldAttributes
 
 module T = FStar.Tactics.V2
 
-type description (d : string) = ()
+let description (d : string) = ()
 
 type r = 
     {

tests/micro-benchmarks/Unit1.Basic.fst

@@ -219,7 +219,7 @@ let test_skolem_match (x:int) =
   match apply (fun x -> x) 0  with
   | 0 -> 0
 
-type _T = (apply (fun x -> x) 0 = 1)
+type _T = (apply (fun x -> x) 0 == 1)
 
 val test_skolem_refinement: x:int{_T} -> Tot unit
 let test_skolem_refinement x = assert false

ulib/Prims.fst

@@ -729,4 +729,4 @@ val string_of_int: int -> Tot string
 (** THIS IS MEANT TO BE KEPT IN SYNC WITH FStar.CheckedFiles.fs
     Incrementing this forces all .checked files to be invalidated *)
 irreducible
-let __cache_version_number__ = 72
+let __cache_version_number__ = 73