Zulip Chat Archive
Stream: lean4
Topic: (kernel) declaration has metavariables
Jason Gross (Mar 05 2021 at 17:44):
When I see (kernel) declaration has metavariables
, is there a way to be told where the metavariables came from and what types they have?
Leonardo de Moura (Mar 05 2021 at 17:51):
Jason Gross said:
When I see
(kernel) declaration has metavariables
, is there a way to be told where the metavariables came from and what types they have?
This is a bug. Could you post the example?
I use the following workaround
set_option trace.Elab.definition true
Lean will display the definition before sending it to the kernel.
If the metavariable doesn't appear there because it is in an implicit argument, then I also use
set_option pp.all true
Jason Gross (Mar 05 2021 at 17:54):
Unminimized example:
section
variable (G : Type) (T : Type) (Tm : Type)
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
(getCtx : T → G) (getTy : Tm → T)
inductive CtxSyntaxLayer where
| emp : CtxSyntaxLayer
| snoc : (Γ : G) → (t : T) → EG Γ (getCtx t) → CtxSyntaxLayer
end
section
variable (G : Type) (T : Type) (Tm : Type)
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
(getCtx : T → G) (getTy : Tm → T)
: CtxSyntaxLayer G T EG getCtx → G)
inductive TySyntaxLayer where
| top : {Γ : G} → TySyntaxLayer
| bot : {Γ : G} → TySyntaxLayer
| nat : {Γ : G} → TySyntaxLayer
| arrow : {Γ : G} → (A B : T) → EG Γ (getCtx A) → EG Γ (getCtx B) → TySyntaxLayer
def getCtxStep : TySyntaxLayer G T EG getCtx → G
| TySyntaxLayer.top (Γ := Γ) .. => Γ
| TySyntaxLayer.bot (Γ := Γ) .. => Γ
| TySyntaxLayer.nat (Γ := Γ) .. => Γ
| TySyntaxLayer.arrow (Γ := Γ) .. => Γ
end
section
variable (G : Type) (T : Type) (Tm : Type)
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
(EGrfl : ∀ {Γ}, EG Γ Γ)
(getCtx : T → G) (getTy : Tm → T)
(GAlgebra : CtxSyntaxLayer G T EG getCtx → G) (TAlgebra : TySyntaxLayer G T EG getCtx → T)
inductive TmSyntaxLayer where
| tt : {Γ : G} → TmSyntaxLayer
| zero : {Γ : G} → TmSyntaxLayer
| succ : {Γ : G} → TmSyntaxLayer
| app : {Γ : G} → (A B : T) → (Actx : EG Γ (getCtx A)) → (Bctx : EG Γ (getCtx B))
→ (f x : Tm)
→ ET (TAlgebra (TySyntaxLayer.arrow A B Actx Bctx)) (getTy f)
→ ET A (getTy x)
→ TmSyntaxLayer
def getTyStep : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra → T
| TmSyntaxLayer.tt .. => TAlgebra TySyntaxLayer.top
| TmSyntaxLayer.zero .. => TAlgebra TySyntaxLayer.nat
| TmSyntaxLayer.succ .. => TAlgebra (TySyntaxLayer.arrow (TAlgebra TySyntaxLayer.nat) (TAlgebra TySyntaxLayer.nat) EGrfl EGrfl)
| TmSyntaxLayer.app (B:=B) .. => B
end
gives
44:7: (kernel) declaration has metavariables 'getTyStep'
Educated guesswork led me to replace TySyntaxLayer.arrow
with @TySyntaxLayer.arrow _ _ _ _ _
, and indeed doing this gives me an error message about the final underscore not being synthesizable. If you want a smaller example, I can probably minimize this one to one that's just a couple lines
Leonardo de Moura (Mar 05 2021 at 17:55):
@Jason Gross Yes, a smaller version would be super useful :)
Jason Gross (Mar 05 2021 at 17:56):
Cool, I'll minimize it then. Is there a version of set_option pp.all true
that prints implicits but doesn't desugar, e.g., matches?
Jason Gross (Mar 05 2021 at 17:59):
inductive Foo {x : Nat} : Type where
| foo : Foo
def bar := (fun _ : Foo => 0) Foo.foo
gives
4:5: (kernel) declaration has metavariables 'bar'
Leonardo de Moura (Mar 05 2021 at 18:00):
You can use
set_option pp.explicit true
However, metavariables may still be hidden inside the syntax sugar.
Leonardo de Moura (Mar 05 2021 at 18:00):
Jason Gross said:
inductive Foo {x : Nat} : Type where | foo : Foo def bar := (fun _ : Foo => 0) Foo.foo
gives
4:5: (kernel) declaration has metavariables 'bar'
Perfect. Thanks!
Jason Gross (Mar 05 2021 at 18:08):
Leonardo de Moura said:
You can use
set_option pp.explicit true
However, metavariables may still be hidden inside the syntax sugar.
Thanks! For now I'm only hitting this in places where I know that I'm failing to fill all implicits somewhere
Alex J. Best (May 17 2022 at 15:16):
@Sacha Huriot ran across this error in the wild, the most minimal version I can reduce to is:
def sacha : Nat :=
let (v, k) := match 0 with
| (n) => (0, 0)
v + k
with the current master I see (kernel) declaration has metavariables 'sacha'
set_option trace.Elab.definition true
gives
[Elab.definition] sacha : Nat :=
let _discr :=
let _discr := 0;
match 0 with
| n => (0, 0);
?m.22 _discr
t.lean:3:0
[Elab.definition.body] sacha : Nat :=
?m.22
(match 0 with
| n => (0, 0))
t.lean:3:0
[Elab.definition.scc] [sacha]
Adding type ascription after (v, k)
fixes it in the MWE, but my understanding is that this is considered a bug still if the tactic state shows no error and only the kernel does, right?
Alex J. Best (May 18 2022 at 07:48):
I made lean4#1155 to track this now.
Last updated: Dec 20 2023 at 11:08 UTC