ToSyntax: annotate type decls to expect a Type

Fixes FStarLang#2933
mtzguido · Nov 30, 2023 · f12a3bc · f12a3bc
1 parent 7e11e10
commit f12a3bc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
@@ -3000,7 +3000,7 @@ let rec desugar_tycon env (d: AST.decl) (d_attrs:list S.term) quals tcs : (env_t
             | None ->
               if BU.for_some (function S.Effect -> true | _ -> false) quals
               then Some teff
-              else None
+              else Some ktype
             | Some k -> Some (desugar_term env' k) in
         let t0 = t in
         let quals = if quals |> BU.for_some (function S.Logic -> true | _ -> false)