#eval: kernel declaration has metavariables

[tydeu]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

A code sample using #eval produces (kernel) declaration has metavariables '_eval' when the evaluated term has a type with no metavariables.

Steps to Reproduce

def Generator {α : Type u} (init : α) (step : α → α) : Type w := PUnit

namespace Generator
variable {α : Type u} {init : α} {step : α → α}

protected partial def forIn [Monad m]
(self : Generator init step) (b : β) (f : α → β → m (ForInStep β)) : m β := do
  let rec loop a b := do
    match (← f a b) with
    | ForInStep.yield b => loop (step a) b
    | ForInStep.done b => pure b
  loop init b

instance : ForIn m (Generator init step) α := ⟨Generator.forIn⟩
end Generator

def generate (init : α) (step : α → α) :
  Generator init step := ⟨⟩

def array [ForIn Id ρ α] (it : ρ) : Array α := Id.run do
  let mut arr := #[]
  for a in it do
    arr := arr.push a
  return arr

def test :=
  generate 0 (· + 1) |> array

#check test -- test : Array Nat
#eval test -- (kernel) declaration has metavariables '_eval'

Expected behavior:

For the #eval to succeed (in this case, loop indefinitely).

Actual behavior:

Get a metavariable error for a term whose type has no metavariables.

Reproduces how often:

Always.

Versions

Windows 10 20H2
Lean (version 4.0.0-nightly-2021-12-17, commit e65f3fe81032, Release)

Additional Information

None.

[Kha]

#print is usually a better idea for checking signatures than #check

def test.{u_1} : Array Nat :=
array (generate 0 fun a => a + 1)

[tydeu]

@Kha ah, but why does test have a universe parameter? Isn't that still a bug?

[Kha]

The output universe of Generator is not sufficiently constrained, so in a way Lean did exactly what you asked it to do. But I can see some improvements here:

• the hover was confusing; https://github.com/leanprover/lean4/tree/51dc32957b676f9391d3995d69f96f0f8fc554d1/
• #check already checks for synthetic mvars eagerly, but it should do so for all mvars to avoid the kernel error message
• IMO, def should not allow universe mvars from the body to escape into the signature. Users should introduce an explicit universe variable if they want that. But might be good to hear if that is a common pattern in mathematics (@digama0 @gebner?)

@leodemoura What do you think? I think I'll leave the two last ones to you if you agree.

[tydeu]

@Kha Ah, sounds good. I am surprised that PUnit (which has a similarly unconstrained universe) doesn't often produce this kind of confusion.

[Kha]

I think that's because PUnit isn't exactly useful in itself, so you only use it as part of larger types that do constrain its universe.

[gebner]

Users should introduce an explicit universe variable if they want that. But might be good to hear if that is a common pattern in mathematics.

It's certainly not common by any means, but it does happen in cardinals/ordinals. By "introducing an explicit universe variable", do you mean def foo.{u, v} := 42? That seems reasonable to me.

IMHO #eval should just instantiate all unassigned universe metavariables with 0.

[Kha]

It's certainly not common by any means, but it does happen in cardinals/ordinals. By "introducing an explicit universe variable", do you mean def foo.{u, v} := 42? That seems reasonable to me.

You would still need to reference the new variables in the body to escape the new check, as in

def test.{u} :=

  generate.{_, u} 0 (· + 1) |> array

IMHO #eval should just instantiate all unassigned universe metavariables with 0.

Ooh, I like it.

[gebner]

It's certainly not common by any means, but it does happen in cardinals/ordinals. By "introducing an explicit universe variable", do you mean def foo.{u, v} := 42? That seems reasonable to me.

You would still need to reference the new variables in the body to escape the new check, as in

def test.{u} :=

  generate.{_, u} 0 (· + 1) |> array

And since they are no longer metavariables, they escape the check anyhow?

def test := generate.{_, u} 0 (∙ + 1) |> array

(I don't think it would cause huge issues to forbid the above as well.)

Another option to avoid unexpected universe parameters is to instantiate all universe metavariables that only occur in the body by 0.

[Kha]

Another option to avoid unexpected universe parameters is to instantiate all universe metavariables that only occur in the body by 0.

Hmm, intriguing. We can't claim parametricity over universes because TC resolution and other parts can distinguish them, but in practice it really shouldn't matter.

[leodemoura]

#check already checks for synthetic mvars eagerly, but it should do so for all mvars to avoid the kernel error message

I agree.

IMO, def should not allow universe mvars from the body to escape into the signature. Users should introduce an explicit universe variable if they want that. But might be good to hear if that is a common pattern in mathematics (@digama0 @gebner?)

Another option to avoid unexpected universe parameters is to instantiate all universe metavariables that only occur in the body by 0.

The two options above look reasonable to me. The second is more convenient for users but I wonder whether it will confuse users or not. I think the first option may be helpful to expose issues in the definition.

[leodemoura]

The original issue has been fixed, but the other suggestion has not been implemented.
I am planning to close this issue and open a new one with the suggested enhancement:

IMO, def should not allow universe mvars from the body to escape into the signature. Users should introduce an explicit universe variable if they want that. But might be good to hear if that is a common pattern in mathematics (@digama0 @gebner?)

@Kha @gebner Ok?

[digama0]

In my experience, whenever this happens it is a bug, and tracking it down is tricky since universes are so thoroughly hidden most of the time, so the errors can persist for a while. I'm fully in support of not letting def bodies have free universe metavariables not determined by the type.