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

[DeLectionnes]

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.

We provide a better MWE in the posts below.

[MathisBD]

I have a MWE for this bug (or a related one) :
Actually it's a different bug, see #1115

[DeLectionnes]

Here is a MWE with the same error as my previous message.
It's a different error message from what MathisBD got :

MWE

From MetaCoq.Utils Require Import utils.
From MetaCoq.Template Require Import All.
From MetaCoq.Template Require Import Checker.
Import MCMonadNotation.
Notation nameAnon := {| binder_name := nAnon; binder_relevance := Relevant |}.


Definition AST_Ind := {|
                      ind_finite := Finite;
                      ind_npars := 1;
                      ind_params := [];
                      ind_bodies := [{|
                          ind_name := "Ind";
                          ind_indices := [];
                          ind_sort := sProp;
                          ind_type :=
                            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) (tSort sProp));
                          ind_kelim := IntoPropSProp;
                          ind_ctors :=[];
                          ind_projs := [];
                          ind_relevance := Relevant
                        |}];
                      
                      ind_universes := Monomorphic_ctx;
                      ind_variance := None
                    |}.



Definition AST_match :=
 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
         |}))
   
   (tCase
      {|
        ci_ind :=
          {| inductive_mind :=(MPfile ["Logic"; "Init"; "Coq"], "True"); inductive_ind := 0 |};
        ci_npar := 0;
        ci_relevance := Relevant
      |}
      {|
        puinst := [];
        pparams := [];
        pcontext := [nameAnon];
        preturn := tProd nameAnon (tRel 1) (tSort sProp)
      |} (tConstruct {| inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "True"); inductive_ind := 0 |} 0 [])
      [{|
          bcontext := [];
          bbody :=
            tLambda nameAnon (tRel 0)
              (tApp
                 (tInd
                    {|
                      inductive_mind := (MPfile ["recherche"; "tests"], "Ind");
                      inductive_ind := 0
                    |} []) [tRel 1; tRel 0])
        |}
   ]).

Definition define_ind : TemplateMonad unit :=
 tmMkInductive true (mind_body_to_entry AST_Ind).

Definition define_dispatch  : TemplateMonad unit :=
 tmMkDefinition "dispatch" AST_match.

Unset MetaCoq Strict Unquote Universe Mode.

Fail MetaCoq Run (_ <- define_ind;;
                 define_dispatch).

MetaCoq Run (define_ind).

MetaCoq Run (define_dispatch).

These AST correspond to the definitions

Inductive Ind (T:Type) : T -> Prop :=.

Definition dispatch := fun (T:Type) => match I with I => fun t => Ind T t end.

The error message is

Illegal application: 
The term "Ind" of type "forall T : Type, T -> Prop"
cannot be applied to the terms
 "T" : "Type"
 "t" : "T"
The 1st term has type "Type@{tests.recherche.45}" which should be a subtype of "Type@{tests.recherche.43}".

[MathisBD]

It's a different error message from what MathisBD got :

Indeed, this now seems like two different bugs. I'll open a new issue.

[MathisBD]

Also I shortened your MWE a bit :

MWE

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

(* Modify this based on the current file. *)
Definition ind : term := 
  tInd {| inductive_mind := (MPfile ["Bug1"], "Ind") ; inductive_ind := 0 |} [].

(* AST of [Inductive Ind (T : Type) : Prop :=.]. *)
Definition AST_Ind := {|
  ind_finite := Finite;
  ind_npars := 1;
  ind_params := [{|
    decl_name := {| binder_name := nNamed "T"; binder_relevance := Relevant |};
    decl_body := None;
    decl_type := tSort (sType fresh_universe)
  |}];
  ind_bodies := [{|
      ind_name := "Ind";
      ind_indices := [];
      ind_sort := sProp;
      ind_type :=
        tProd {| binder_name := nNamed "T"; binder_relevance := Relevant |}
          (tSort (sType fresh_universe)) (tSort sProp);
      ind_kelim := IntoPropSProp;
      ind_ctors :=[];
      ind_projs := [];
      ind_relevance := Relevant
    |}];
  ind_universes := Monomorphic_ctx;
  ind_variance := None
|}.

(* AST of [fun T : Type => Ind T]. *)
Definition AST_fun :=
  tLambda 
    {| binder_name := nNamed "T"; binder_relevance := Relevant |}
    (tSort (sType fresh_universe))
    (tApp ind [tRel 0]).

Definition define_ind : TemplateMonad unit :=
 tmMkInductive true (mind_body_to_entry AST_Ind).

Definition define_fun : TemplateMonad unit := 
  tmMkDefinition "def" AST_fun. 

Unset MetaCoq Strict Unquote Universe Mode.

Fail MetaCoq Run (define_ind ;; define_fun).

MetaCoq Run (define_ind).
MetaCoq Run (define_fun).

The error message is still the same.