Command affects line before it

Stream: general

[Heather Macbeth]

In this example, there is an error on the variable declaration line (on CompleteSpace E) which seems to be induced by the line after it (locally erasing various instances).

import Mathlib.Analysis.InnerProductSpace.Dual

variable {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]

attribute [-instance]
  PseudoMetricSpace.toUniformSpace
  MetricSpace.toEMetricSpace
  PseudoMetricSpace.toPseudoEMetricSpace

#check InnerProductSpace.toDual

[Heather Macbeth]

I cannot minimize this today, but is this indeed a bug and is it known?

[Joachim Breitner]

As you probably noticed, reducing the last line makes the error go away. It may be a small UX bug, but maybe qualifies as “you get to keep both pieces” if you write a variable declaration that becomes invalid later in the same file. I’d suggest to not bother reporting unless it turns out to be often cause confusion

[Mario Carneiro]

this is another manifestation of the late elaboration of variable lines, I think there is at least one issue open about it

[Heather Macbeth]

Joachim Breitner said:

reducing the last line makes the error go away.

@Joachim Breitner Do you mean if I change the #check line to

#reduce InnerProductSpace.toDual

? The error is still present.

[Heather Macbeth]

(@Mario Carneiro I tried to find the related issues you mentioned, but didn't find them with the obvious searches -- maybe the underlying issue is not well-reflected in the keywords used when the issues were filed.)

[Kyle Miller]

Maybe Joachim meant "removing" instead of "reduced"?

The underlying issue is that variable re-elaborates from scratch on each definition. So, it's like you did

attribute [-instance]
  PseudoMetricSpace.toUniformSpace
  MetricSpace.toEMetricSpace
  PseudoMetricSpace.toPseudoEMetricSpace

#check fun {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] => InnerProductSpace.toDual

Because the instances are removed, elaboration of #check fails. The variable command makes the assumption "if elaborating this binder now works, it will keep working", but as you see, removing instances is a way to break this assumption.

[Kyle Miller]

Here's another example of the assumption failing:

set_option autoImplicit true

variable (x : Fin n)

set_option autoImplicit false

#check x
-- x : Fin (sorryAx ℕ true)

[Heather Macbeth]

Thanks Kyle, that's a helpful example! In particular, I see that the issue was "blunter" than I realised. I had assumed that the error on [CompleteSpace E] triggered by the use of InnerProductSpace.toDual had something to do with the fact that toDual itself has arguments [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]. But that's not the case -- changing the #check line to anything at all, for example

example (a b : ℕ) : a + b = b + a := add_comm ..

gives the same error.