search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
378 stars 81 forks source link

Universe level error when defining dependent types in one metacoq call. #1108

Open DeLectionnes opened 6 days ago

DeLectionnes commented 6 days ago

When defining new objects and inductive types in one MetaCoq Run call from their term AST, if your definitions are dependent, it can lead to a universe level error not present when defining them with multiple calls.

For the code below to work, the notations filename and foldername must be modified to match your own file and containing folder names.

Example Version 8.20 ```coq From MetaCoq.Utils Require Import utils. From MetaCoq.Template Require Import All. Import MCMonadNotation. (* ************************************************************************ *) (* The monad CallMonad Sig X returning an element of type X *) (* The signature Sig is to be instantiated by an inductive Type family *) (* The type Sig X represents the calls to functions returning type X *) (* ************************************************************************ *) Set Printing Universes. Inductive CallMonad@{i j k l} (Sig:Type@{i} -> Type@{j}) (T:Type@{k}): Type@{l} := Cret: T -> CallMonad Sig T | Cbind : forall {X : Type@{k}}, CallMonad Sig X -> (X -> CallMonad Sig T) -> CallMonad Sig T | Ccall : Sig T -> CallMonad Sig T. Print CallMonad. Arguments Cret {Sig} {T}. Arguments Cbind {Sig} {T} {X}. Arguments Ccall {Sig} {T}. (* ************************************************************************ *) (* A recursive definition is given by: *) (* - a signature recsig *) (* - an implementation (in the CallMonad) for each function call in Sig *) (* ************************************************************************ *) Definition RecDef@{m n o} (Sig:Type@{m} -> Type@{n}) : Type@{o} := forall {X:Type@{m}} (call:Sig X), CallMonad Sig X. (* ************************************************************************ *) (* the Value (evaluation) relation *) (* ************************************************************************ *) Inductive Value@{p q r s} {Sig: Type@{p} -> Type@{q}} (def:RecDef Sig) {T:Type@{r}}: CallMonad Sig T -> T -> Prop := | Value_ret : forall (v:T), Value def (Cret v) v | Value_bind : forall {X:Type@{s}} {x} {k} (vx:X) (vkx:T), Value _ x vx -> Value _ (k vx) vkx -> Value _ (Cbind x k) vkx | Value_call : forall (call:Sig T) {vcall:T}, Value _ (def T call) vcall -> Value _ (Ccall call) vcall. (* ******************************************************************************* *) (* The intended targets of the AST definitions *) (* ******************************************************************************* *) Inductive Value_ret_ {Sig} (def:RecDef Sig) {X:Type} (x:X) : X -> Prop := | Value_ret' : Value_ret_ def x x. Inductive Value_bind_ {Sig} (def:RecDef Sig) {T X:Type} x (k:T -> CallMonad _ X) : X -> Prop := | Value_bind' : forall vx vkx, Value def x vx -> Value def (T:=X) (k vx) vkx -> Value_bind_ def x k vkx. Inductive Value_call_ {Sig} (def:RecDef Sig) X callX: X -> Prop := | Value_call' : forall vcall, Value def (def X callX) vcall -> Value_call_ def X callX vcall. Definition Value_dispatch2 {Sig} (def:RecDef Sig) {X:Type} (prg:CallMonad Sig X): X -> Prop := match prg return X -> Prop with Cret v => fun vv => Value_ret_ def v vv | Cbind T x k => fun vv => @Value_bind_ Sig def T X x k vv | Ccall callX => fun vv => Value_call_ def _ callX vv end. (* ******************************************************************************* *) (* The ASTs to define *) (* ******************************************************************************* *) Notation nameAnon := {| binder_name := nAnon; binder_relevance := Relevant |}. Notation filename := "bug_universe_level". Notation foldername := "tests". Definition AST_Value_Cret := {| ind_finite := Finite; ind_npars := 4; ind_params := []; ind_bodies := [{| ind_name := "Value_Cret"; ind_indices := []; ind_sort := sProp; ind_type := tProd {| binder_name := nNamed "Sig"; binder_relevance := Relevant |} (tProd nameAnon (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |}))) (tProd {| binder_name := nNamed "def"; binder_relevance := Relevant |} (tApp (tConst (MPfile [filename; foldername], "RecDef") []) [tRel 0]) (tProd {| binder_name := nNamed "T"; binder_relevance := Relevant |} (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tProd nameAnon (tRel 0) (tProd nameAnon (tRel 1) (tSort sProp))))); ind_kelim := IntoPropSProp; ind_ctors := [{| cstr_name := "Value_ret_Cret"; cstr_args := []; cstr_indices := []; cstr_type := tProd {| binder_name := nNamed "Sig"; binder_relevance := Relevant |} (tProd nameAnon (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |}))) (tProd {| binder_name := nNamed "def"; binder_relevance := Relevant |} (tApp (tConst (MPfile [filename; foldername], "RecDef") []) [tRel 0]) (tProd {| binder_name := nNamed "T"; binder_relevance := Relevant |} (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tProd nameAnon (tRel 0) (tApp (tRel 4) [tRel 3; tRel 2; tRel 1; tRel 0; tRel 0])))); cstr_arity := 1 |}]; ind_projs := []; ind_relevance := Relevant |}]; ind_universes := Monomorphic_ctx; ind_variance := None |}. Definition AST_Value_Cbind := {| ind_finite := Finite; ind_npars := 6; ind_params := []; ind_bodies := [{| ind_name := "Value_Cbind"; ind_indices := []; ind_sort := sProp; ind_type := tProd {| binder_name := nNamed "Sig"; binder_relevance := Relevant |} (tProd nameAnon (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |}))) (tProd {| binder_name := nNamed "def"; binder_relevance := Relevant |} (tApp (tConst (MPfile [filename; foldername], "RecDef") []) [tRel 0]) (tProd {| binder_name := nNamed "T"; binder_relevance := Relevant |} (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tProd {| binder_name := nNamed "X"; binder_relevance := Relevant |} (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tProd nameAnon (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "CallMonad"); inductive_ind := 0 |} []) [tRel 3; tRel 0]) (tProd nameAnon (tProd nameAnon (tRel 1) (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "CallMonad"); inductive_ind := 0 |} []) [tRel 5; tRel 3])) (tProd nameAnon (tRel 3) (tSort sProp))))))); ind_kelim := IntoPropSProp; ind_ctors := [{| cstr_name := "Value_bind_Cbind"; cstr_args := []; cstr_indices := []; cstr_type := tProd {| binder_name := nNamed "Sig"; binder_relevance := Relevant |} (tProd nameAnon (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |}))) (tProd {| binder_name := nNamed "def"; binder_relevance := Relevant |} (tApp (tConst (MPfile [filename; foldername], "RecDef") []) [tRel 0]) (tProd {| binder_name := nNamed "T"; binder_relevance := Relevant |} (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tProd {| binder_name := nNamed "X"; binder_relevance := Relevant |} (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tProd nameAnon (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "CallMonad"); inductive_ind := 0 |} []) [tRel 3; tRel 0]) (tProd nameAnon (tProd nameAnon (tRel 1) (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "CallMonad"); inductive_ind := 0 |} []) [tRel 5; tRel 3])) (tProd {| binder_name := nNamed "vx"; binder_relevance := Relevant |} (tRel 2) (tProd {| binder_name := nNamed "vkx"; binder_relevance := Relevant |} (tRel 4) (tProd nameAnon (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "Value"); inductive_ind := 0 |} []) [tRel 7; tRel 6; tRel 4; tRel 3; tRel 1]) (tProd nameAnon (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "Value"); inductive_ind := 0 |} []) [tRel 8; tRel 7; tRel 6; tApp (tRel 3) [tRel 2]; tRel 1]) (tApp (tRel 10) [tRel 9; tRel 8; tRel 7; tRel 6; tRel 5; tRel 4; tRel 2])))))))))); cstr_arity := 3 |}]; ind_projs := []; ind_relevance := Relevant |}]; ind_universes := Monomorphic_ctx; ind_variance := None |}. Definition AST_Value_Ccall := {| ind_finite := Finite; ind_npars := 4; ind_params := []; ind_bodies := [{| ind_name := "Value_Ccall"; ind_indices := []; ind_sort := sProp; ind_type := tProd {| binder_name := nNamed "Sig"; binder_relevance := Relevant |} (tProd nameAnon (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |}))) (tProd {| binder_name := nNamed "def"; binder_relevance := Relevant |} (tApp (tConst (MPfile [filename; foldername], "RecDef") []) [tRel 0]) (tProd {| binder_name := nNamed "T"; binder_relevance := Relevant |} (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tProd nameAnon (tApp (tRel 2) [tRel 0]) (tProd nameAnon (tRel 1) (tSort sProp))))); ind_kelim := IntoPropSProp; ind_ctors := [{| cstr_name := "Value_call_Ccall"; cstr_args := []; cstr_indices := []; cstr_type := tProd {| binder_name := nNamed "Sig"; binder_relevance := Relevant |} (tProd nameAnon (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |}))) (tProd {| binder_name := nNamed "def"; binder_relevance := Relevant |} (tApp (tConst (MPfile [filename; foldername], "RecDef") []) [tRel 0]) (tProd {| binder_name := nNamed "T"; binder_relevance := Relevant |} (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tProd nameAnon (tApp (tRel 2) [tRel 0]) (tProd {| binder_name := nNamed "vcall"; binder_relevance := Relevant |} (tRel 1) (tProd nameAnon (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "Value"); inductive_ind := 0 |} []) [tRel 4; tRel 3; tRel 2; tApp (tRel 3) [tRel 2; tRel 1]; tRel 0]) (tApp (tRel 6) [tRel 5; tRel 4; tRel 3; tRel 2; tRel 1])))))); cstr_arity := 1 |}]; ind_projs := []; ind_relevance := Relevant |}]; ind_universes := Monomorphic_ctx; ind_variance := None |}. Definition AST_Value_dispatch := (tLambda {| binder_name := nNamed "Sig"; binder_relevance := Relevant |} (tProd nameAnon (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |}))) (tLambda {| binder_name := nNamed "def"; binder_relevance := Relevant |} (tApp (tConst (MPfile [filename; foldername], "RecDef") []) [tRel 0]) (tLambda {| binder_name := nNamed "T"; binder_relevance := Relevant |} (tSort (sType {| t_set := {| LevelExprSet.this := [(Level.level "__metacoq_fresh_level__", 0)]; LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "__metacoq_fresh_level__", 0) |}; t_ne := eq_refl |})) (tLambda nameAnon (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "CallMonad"); inductive_ind := 0 |} []) [tRel 2; tRel 0]) (tCase {| ci_ind := {| inductive_mind := (MPfile [filename; foldername], "CallMonad"); inductive_ind := 0 |}; ci_npar := 2; ci_relevance := Relevant |} {| puinst := []; pparams := [tRel 3; tRel 1]; pcontext := [nameAnon]; preturn := tProd nameAnon (tRel 2) (tSort sProp) |} (tRel 0) [{| bcontext := [nameAnon]; bbody := tLambda nameAnon (tRel 2) (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "Value_Cret"); inductive_ind := 0 |} []) [tRel 5; tRel 4; tRel 3; tRel 1; tRel 0]) |}; {| bcontext := [nameAnon; nameAnon; {| binder_name := nNamed "X"; binder_relevance := Relevant |}]; bbody := tLambda nameAnon (tRel 4) (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "Value_Cbind"); inductive_ind := 0 |} []) [tRel 7; tRel 6; tRel 5; tRel 3; tRel 2; tRel 1; tRel 0]) |}; {| bcontext := [nameAnon]; bbody := tLambda nameAnon (tRel 2) (tApp (tInd {| inductive_mind := (MPfile [filename; foldername], "Value_Ccall"); inductive_ind := 0 |} []) [tRel 5; tRel 4; tRel 3; tRel 1; tRel 0]) |}]))))). (* ******************************************************************************* *) (* The definition functions of the ASTs *) (* ******************************************************************************* *) Definition define_ret : TemplateMonad unit := tmMkInductive true (mind_body_to_entry AST_Value_Cret). Definition define_bind : TemplateMonad unit := tmMkInductive true (mind_body_to_entry AST_Value_Cbind). Definition define_call : TemplateMonad unit := tmMkInductive true (mind_body_to_entry AST_Value_Ccall). Definition define_dispatch : TemplateMonad unit := tmMkDefinition "Value_dispatch" AST_Value_dispatch. Unset MetaCoq Strict Unquote Universe Mode. (*If we define all elements in one MetaCoq call, we have a universe problem*) Fail MetaCoq Run (_ <- define_ret;; _ <- define_bind;; _ <- define_call;; define_dispatch). (*But with two separate calls, it works*) MetaCoq Run (_ <- define_ret;; _ <- define_bind;; define_call). MetaCoq Run (define_dispatch). ```
MathisBD commented 8 hours ago

I have a MWE for this bug (or a related one) :

From MetaCoq.Template Require Import All.
From MetaCoq.Utils Require Import monad_utils.
Import MCMonadNotation.

Unset MetaCoq Strict Unquote Universe Mode.

Definition test :=
  mlet t1 <- tmUnquoteTyped Type (tSort (sType (Universe.make' fresh_level))) ;;
  mlet t2 <- tmUnquoteTyped Type (tSort (sType (Universe.make' fresh_level))) ;;
  tmPrint (t1, t2) ;;
  tmDefinitionRed "t1"%bs None t1 ;;
  tmDefinitionRed "t2"%bs None t2.

Fail MetaCoq Run test.
(* The command has indeed failed with message:
   Undeclared universe: Bug.174 (maybe a bugged tactic).*)

Basically the test function creates two universes (which you can check from the tmPrint output), and the second call to tmDefinitionRed fails because the universe of t2 is undeclared.

MathisBD commented 8 hours ago

I also think I found the source of the bug. In template-coq/run_template_monad.ml, this is the TmDefinition case of the main loop :

let name = unquote_ident (reduce_all env evm name) in
let opaque = unquote_bool (reduce_all env evm opaque) in
let evm, typ = (match unquote_option s with Some s -> let red = unquote_reduction_strategy env evm s in Plugin_core.reduce env evm red typ | None -> evm, typ) in
let cinfo = Declare.CInfo.make ~name () ~typ:(Some (EConstr.of_constr typ)) in
let info = Declare.Info.make ~poly ~kind:(Decls.IsDefinition Decls.Definition) () in
let n = Declare.declare_definition ~cinfo ~info ~opaque ~body:(EConstr.of_constr body) evm in
let env = Global.env () in
(* Careful, universes in evm were modified for the declaration of def *)
let evm = Evd.from_env env in
let evm, c = Evd.fresh_global (Global.env ()) evm n in
k ~st env evm (EConstr.to_constr evm c)

After adding the new definition to the global environment, we ditch the old evar map and create a fresh one from the environment (let evm = Evd.from_env env in ...). This has the effect of discarding the declarations for universes which were in the old evar map, and that we still might need later on (see the MWE).

MathisBD commented 8 hours ago

Anyone has an idea how to solve this ?