unexpected `variable` behaviour?

Stream: lean4

[Damiano Testa]

The #mwe below surprises me: it seems that updating the binder type in variable makes the available typeclasses disappear.

class one (A : Type)
class two (A B : Type) [one A]

variable {A B : Type} [one A] [one B]
variable (A)
variable  -- comment `variable`, and `[two A B]` says `failed to synthesize instance one A`
         [two A B]

The analogous Lean 3 code, with variable replaced by variables appears to work.

Is this expected? Am I missing something?

[Kevin Buzzard]

I think that you now can't change binder types and add new instances in the same variable command, for some unknown reason (don't know if this was an oversight or intentional)

[Damiano Testa]

Ok, the workaround is easy, I just wanted to confirm that I was not doing something silly!

[Kevin Buzzard]

Wait I'm confused: this seems to work fine

variable (A : Type)
variable {A} (B : Type)

[Damiano Testa]

Yes, this seems to work. I think that the issue is that when you change the binder type, the instances on the re-bound variable disappear, for the rest of the variable command.

[Damiano Testa]

At least, this is compatible with what I tried.

[Kevin Buzzard]

Sorry, I think that I have seen this issue before and incorrectly diagnosed it at the time. It's more subtle than what I had thought maybe, unless I'm missing something too

[Kevin Buzzard]

Maybe open an issue in a few days unless there is more discussion here?

[Damiano Testa]

Sure, I'll wait to see if there are more comments and otherwise I'll open an issue.

[Mario Carneiro]

this is expected behavior (or a known bug, depending on your POV), you can't mix binder updates and regular variables in the same command

[Mario Carneiro]

TBH it should be a different keyword

[Mario Carneiro]

that is,

variable (A) [two A B]

is declaring another variable named A, without the typeclass assumption of the other one

[Damiano Testa]

Indeed, this also happens:

class one (A : Type)
class two (A : Type) [one A]

variable (A) [one A]
variable {A} [one A] [two A]

example (_ : A) : True := by trivial  -- the tactic state is
/-
A: Type
inst✝² inst✝¹: one A
inst✝: two A
x✝: A
⊢ True
-/

There is one type A and two instances one A.

[Kevin Buzzard]

Mario Carneiro said:

this is expected behavior (or a known bug, depending on your POV), you can't mix binder updates and regular variables in the same command

But that seemed to work fine.

[Mario Carneiro]

are you sure it isn't introducing two variables named A?

[Kevin Buzzard]

I'm not sure how to check.

variable (A : Type)
variable (x : A)
variable {A} (B : Type)
variable (y : A)

#check (x,y) -- A × A

[Damiano Testa]

I'm not at my computer now, but I will be soon. How can I check if there are two variables named A?

[Mario Carneiro]

I think this shows it is a binder update:

variable (A : Nat)
variable {A} (B : Type)

def foo := (A, B)
#print foo
-- def foo : {A : Nat} → Type → Nat × Type :=
-- fun {A} B => (A, B)

[Mario Carneiro]

since I never wrote anything about an implicit variable of type Nat

[Mario Carneiro]

Actually it seems my original assertion was incorrect, {A} is treated as a binder update in almost all circumstances, even when there are other things going on in the variable line. However, the variable line is prechecked, and it is this that is failing:

class one (A : Nat)
class two (A : Nat) [one A] := t : Nat

variable (A : Nat) [one A]
variable {A} [two (by exact A)] -- ignore the unreachable tactic linter warning here

def foo := two.t A
#print foo

-- def foo : {A : Nat} → [inst : one A] → [inst : two A] → Nat :=
-- fun {A} [one A] [two A] => two.t A

[Mario Carneiro]

Using by exact A here circumvents the precheck, delaying elaboration of the variable body until foo

[Mario Carneiro]

the linter is pointing out that the tactic is never run during the variable command

[Mario Carneiro]

Oh, here's an interesting behavior:

variable (A : Nat) (B : by skip)
def foo := A = B -- no error is reported

#print foo -- unknown constant 'foo'

[Mario Carneiro]

(lean4#2226)

[Mario Carneiro]

@Sebastian Ullrich What do you think about fixing this issue by identifying binder updates before the precheck, simply by checking if they are binders without type where the variable name is already in scope? And then the precheck would run on the variables with the binder updates filtered out.

[Sebastian Ullrich]

I think I tried that once. It looked messy, but might still be the correct solution.

[Adam Topaz]

There’s a lean4 issue open about this

[Sophie Morel]

Damiano Testa said:

The #mwe below surprises me: it seems that updating the binder type in variable makes the available typeclasses disappear.

class one (A : Type)
class two (A B : Type) [one A]

variable {A B : Type} [one A] [one B]
variable (A)
variable  -- comment `variable`, and `[two A B]` says `failed to synthesize instance one A`
         [two A B]

The analogous Lean 3 code, with variable replaced by variables appears to work.

Is this expected? Am I missing something?

FWIW, I just ran into what I think is the same issue (I updated a variable from implicit to explicit and lost a previously declaredFintype instance on it). As you mentioned, the workaround is easy, I'm just glad that I had read and so was confused only for a short while.

[Damiano Testa]

I am happy that this was helpful! If I understand correctly, if you update with variable (A), instead of variable (A : Type _), you may still get the instances on the previously defined variable A.

[Damiano Testa]

variable (A) [a : Add A]
#synth Add A  -- finds `a`

variable {A}
#synth Add A  -- finds `a`

variable {A : Type _} --[Add A]
#synth Add A  -- failed to synthesize `Add A`

[Sophie Morel]

Damiano Testa said:

I am happy that this was helpful! If I understand correctly, if you update with variable (A), instead of variable (A : Type _), you may still get the instances on the previously defined variable A.

Yes, I tested in a MWE and in my working file, and it seems that I am keeping my Fintype instance through several updates. Thanks !

[Eric Wieser]

Damiano Testa said:

If I understand correctly, if you update with [...] instead of variable (A : Type _)

variable (A : Type _) is not an update at all, it's "create a new A in addition to the old one"

[Damiano Testa]

Yes, I expressed it badly: variable can perform two separate actions.

• It can introduce previously non-existing variables (possibly making inaccessible pre-existing ones);
• it can modify the binder type of previously existing variables.

Some of the examples are confusing, because they mix these two behaviours. I think that someone, maybe Mario, even commented that it would have been clearer if these two actions had different names.

[Sophie Morel]

Eric Wieser said:

Damiano Testa said:

If I understand correctly, if you update with [...] instead of variable (A : Type _)

variable (A : Type _) is not an update at all, it's "create a new A in addition to the old one"

Ah, that makes more sense now, thank you for the explanation!

[Eric Wieser]

I've opened #6079 which corrects hundreds of accidentally-duplicated-variables in mathlib, though I imagine it will take some work to get it through CI

[Yury G. Kudryashov]

Build fails

[Sebastien Gouezel]

Is it a bug in variable, that we should try to fix instead of circumventing it? Or is it by design?

[Eric Wieser]

I don't know whether this is a bug or by design, nor it seems does Mario:

@Mario Carneiro said:

this is expected behavior (or a known bug, depending on your POV), you can't mix binder updates and regular variables in the same command

[Mario Carneiro]

Note that what I said there was wrong, see the follow up message:

Mario Carneiro said:

Actually it seems my original assertion was incorrect, {A} is treated as a binder update in almost all circumstances, even when there are other things going on in the variable line. However, the variable line is prechecked, and it is this that is failing:

class one (A : Nat)
class two (A : Nat) [one A] := t : Nat

variable (A : Nat) [one A]
variable {A} [two (by exact A)] -- ignore the unreachable tactic linter warning here

def foo := two.t A
#print foo

-- def foo : {A : Nat} → [inst : one A] → [inst : two A] → Nat :=
-- fun {A} [one A] [two A] => two.t A

[Eric Wieser]

Would you vote against salvaging #6079 then?

[Eric Wieser]

Did we ever decide whether this was a bug? I raise in https://github.com/leanprover/lean4/pull/2645/files#r1358511268 (cc @David Thrane Christiansen) that we should document that mixing binder updates and new variables is a bad idea, but it's hard to justify something where no one knows if its a feature.

[Patrick Massot]

From the UX point of view it is definitely a bug. And it is confusing when porting Lean 3 code.

[Eric Wieser]

lean4#2789

[David Thrane Christiansen]

Thank you!