autoImplicit confusion?

Stream: lean4

[James Gallicchio]

Ah okay, thanks for taking a look

(Also, I didn't mean to make this in #mathlib4, if someone has the power to move it to #lean4 I'd be grateful)

[Notification Bot]

Sebastian Ullrich has marked this topic as resolved.

[Notification Bot]

Sebastian Ullrich has marked this topic as resolved.

[Sebastian Ullrich]

(whoops, wrong button... also, race condition in Zulip)

[Notification Bot]

This topic was moved here from #mathlib4 > ✔ autoImplicit confusion? by Sebastian Ullrich.

[Notification Bot]

Sebastian Ullrich has marked this topic as unresolved.

[Leonardo de Moura]

The declaration is accepted because of the "auto implicit chaining" feature. We can try to refine this feature, but this is the expected behavior for this feature. From our release notes:

• Added auto implicit "chaining". Unassigned metavariables occurring in the auto implicit types now become new auto implicit locals. Consider the following example:

  inductive HasType : Fin n → Vector Ty n → Ty → Type where
    | stop : HasType 0 (ty :: ctx) ty
    | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty

ctx is an auto implicit local in the two constructors, and it has type ctx : Vector Ty ?m. Without auto implicit "chaining", the metavariable ?m will remain unassigned. The new feature creates yet another implicit local n : Nat and assigns n to ?m. So, the declaration above is shorthand for

  inductive HasType : {n : Nat} → Fin n → Vector Ty n → Ty → Type where
    | stop : {ty : Ty} → {n : Nat} → {ctx : Vector Ty n} → HasType 0 (ty :: ctx) ty
    | pop  : {n : Nat} → {k : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty

[Leonardo de Moura]

We can claim this is a bug since x is not an auto implicit in the Foo example above. So, the metavariable occurring there should not become a new parameter.

[James Gallicchio]

That makes sense -- I too would consider it a bug, since the behavior feels surprising in a way that auto-implicit generally does not

[Leonardo de Moura]

Pushed the following.
https://github.com/leanprover/lean4/commit/04d3c6feebb81eb684be1c64289b8a5ddf7b7ba8

inductive Foo
| bar (x) : Foo

now produces an error.