Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ensure type decls are types #3118

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Tc: check that 'type' declarations really define types
Fixex #2933
mtzguido committed Jan 14, 2025
commit e824185b55c361d1edc54be0e551e79805283eb3
3 changes: 2 additions & 1 deletion src/syntax/FStarC.Syntax.Syntax.fst
Original file line number Diff line number Diff line change
@@ -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;
5 changes: 4 additions & 1 deletion src/syntax/FStarC.Syntax.Syntax.fsti
Original file line number Diff line number Diff line change
@@ -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).
}


2 changes: 1 addition & 1 deletion src/tosyntax/FStarC.ToSyntax.ToSyntax.fst
Original file line number Diff line number Diff line change
@@ -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
32 changes: 26 additions & 6 deletions src/typechecker/FStarC.TypeChecker.Tc.fst
Original file line number Diff line number Diff line change
@@ -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