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