Quantifiers in CanonM

Stream: lean4

[Heather Macbeth]

In the following example, the canonicalizer seems to be failing when asked to canonicalize the expression ∃ f : Nat → Nat, ∀ x, f x = 0. The error message is "unexpected bound variable #1". Is this a bug? If so, any diagnoses?

import Lean.Meta.Canonicalizer
import Lean.Elab.Tactic

elab "foo" t:term : tactic => do
  let e ← Lean.Elab.Tactic.elabTerm t none
  trace[debug] "canonicalizing {e}"
  let e' ← (Lean.Meta.canon e).run'
  trace[debug] "canonicalized it to {e'}"

#check (∃ f : Nat → Nat, ∀ x, f x = 0) -- works fine

set_option trace.debug true in
example : True := by
  foo (∃ f : Nat → Nat, ∀ x, f x = 0) -- unexpected bound variable #1

[Kim Morrison]

Yes, the problem is in src#Lean.Meta.Canonicalizer.mkKey

[Kim Morrison]

When we call mkKey on the f inside the existential, we hit the app branch with f being a bound variable, and then getFunInfo calls inferType on it and crashes with the observed error.

[Kim Morrison]

I'm uncertain whether we should be replacing the bound variables via an appropriate telescope function, or just adding an extra isBVar test after the current isMVar test.

[Heather Macbeth]

OK, thanks for investigating and confirming! I can open an issue if you like, let me know.

[Kim Morrison]

No need for an issue. lean#6082 fixes the reported problem, and doesn't break omega tests, but my spidey-sense says that I am doing it wrong... @Kyle Miller, could you take a quick look at this?

[Heather Macbeth]

Even better. Thanks!