Skip to content

Using tmMkInductive and tmUnquote unpredictably crashes #1114

@MathisBD

Description

@MathisBD

Declaring an inductive (tmMkInductive) and unquoting it (tmUnquote) in the same metacoq command unpredictably fails,
depending on which functions are inlined (see MWE).

Here is a MWE to reproduce the bug (I declare a (trivial) inductive and immediately try to unquote it) :

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 ["Bug2"], "Ind") ; inductive_ind := 0 |} [].

(* The simplest inductive you can make. *)
Definition mind_body := {|
  ind_finite := Finite;
  ind_npars := 0;
  ind_params := [];
  ind_bodies := [{|
      ind_name := "Ind";
      ind_indices := [];
      ind_sort := sProp;
      ind_type := tSort sProp;
      ind_kelim := IntoPropSProp;
      ind_ctors :=[];
      ind_projs := [];
      ind_relevance := Relevant
    |}];
  ind_universes := Monomorphic_ctx;
  ind_variance := None
|}.

Definition define_ind : TemplateMonad unit :=
  tmMkInductive' mind_body.

Definition unquote_ind : TemplateMonad unit := 
  tmUnquote ind ;; ret tt.

(* Anomaly : "Inductive Bug2.Ind does not appear in the environment." *)
MetaCoq Run (define_ind ;; unquote_ind).

(* Succeeds. *)
MetaCoq Run define_ind.
MetaCoq Run unquote_ind.

(* Succeeds. *)
MetaCoq Run (tmMkInductive' mind_body ;; unquote_ind).

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions