Bug in instance synthesis?

Stream: mathlib4

[Sébastien Gouëzel]

The following looks like a bug to me, where Lean finds an instance it shouldn't find:

import Mathlib

variable {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]

def my_copy (E : Type*) := E

instance : AddCommGroup (my_copy E) := inferInstanceAs (AddCommGroup E)
instance : TopologicalSpace (my_copy E) := inferInstanceAs (TopologicalSpace E)
instance : Module 𝕜 (my_copy E) := inferInstanceAs (Module 𝕜 E)

set_option trace.Meta.synthInstance true in
#synth Norm (E →L[𝕜] my_copy E) -- works, while it shouldn't

To have a norm on a space of linear maps, you should have a norm on both sides. But there is no norm on my_copy E, it is a type synonym on which I've not registered the norm. The trace shows failure but success, it's very weird.

Does anyone understand what is going on here?

[Sébastien Gouëzel]

(It's not a theoretical question, this is blocking me on my work on Riemannian metrics)

[Eric Wieser]

Unsurprisingly this still reproduces with import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic

[Aaron Liu]

It is using the instance for E (but why?)

[Etienne Marion]

If you comment out the AddCommGroup and the TopologicalSpace instances, then the Module instance fails because it cannot synthesize AddCommMonoid (my_copy E). But if you uncomment only the TopologicalSpace instance, then it works. Looking at the synthesized value, it seems to infer a NormedAddCommGroup structure on my_copy E, but it is not able to synthesize NormedAddCommGroup E.

[Sébastien Gouëzel]

It's even more funny when synthetizing Norm (my_copy E →L[𝕜] my_copy E), which also works. In the synthInstance trace, one sees that Lean fails to solve all the subgoals of ContinuousLinearMap.hasOpNorm, with only red crosses, but still it comes back with a green tick saying it has solved the problem!
crazyTrace.png

[Matthew Ballard]

It is probably caching a NormedAddCommGroup instance on my_copy E when it unifies some other non-normed instance using a projection and notices that it unfolds to E.

[Matthew Ballard]

We get a line

@SeminormedAddCommGroup.toAddCommGroup (my_copy E) inst✝¹ : AddCommGroup (my_copy E)

from

 ✅️ E →L[𝕜] my_copy E =?= ?m.4956 →SL[?m.4964] ?m.4957

where [inst✝¹ : SeminormedAddCommGroup E] (changed slightly from example above)

[Matthew Ballard]

@ContinuousLinearMap 𝕜 𝕜 Field.toSemifield.toDivisionSemiring.toSemiring Field.toSemifield.toDivisionSemiring.toSemiring (RingHom.id 𝕜) E
  PseudoMetricSpace.toUniformSpace.toTopologicalSpace inst✝¹.toAddCommMonoid
  (my_copy E) PseudoMetricSpace.toUniformSpace.toTopologicalSpace inst✝¹.toAddCommMonoid inst✝.toModule inst✝.toModule : Type u_2

is what applying ContinuousLinearMap.hasOpNorm says we have to unify with where we get a PseudoMetricSpace (my_copy E) from the projection from SeminormedAddCommGroup E.

[Sébastien Gouëzel]

Thanks for investigating! Does this mean that unifying some projections is done at the wrong reducibility level?

[Matthew Ballard]

Certainly we end up in a unification problem at semi-reducible transparency. You can see this in the trace. I am not sure the exact entry point yet

[Matthew Ballard]

Note: if you make my_copy irreducible and unseal it in the instances we fail correctly

[Sébastien Gouëzel]

Not an option in my use case, unfortunately.

[Sébastien Gouëzel]

Reported at lean4#9077

[Mario Carneiro]

isn't this the reason we switched from defs to wrapper structures for Opposite and friends?

[Kevin Buzzard]

I thought that it was because things randomly got unfolded due to incomplete API and/or accidental defeq abuse, not this: I've never seen anything like this before. It would probably be good to minimise :-/

[Mario Carneiro]

no I distinctly remember lean unfolding things more aggressively than it used to in defeq problems and instance search

[Mario Carneiro]

there were some cases that we just couldn't work around

[Mario Carneiro]

it wasn't about users unfolding and getting themselves confused, lean was doing it without us asking it to

[Jovan Gerbscheid]

Lean's unification has the following feature: when unifying two applications of the same head constant (in this case ContinuousLinearMap), then in the (instance) implicit arguments it sets the reducibility to default (in this case in the argument of type TopologicalSpace (my_copy E)). It does this using the funtion withInferTypeConfig. Arguably, when checking the type of the assignment of an instance metavariable, the reducibility should be at most instances, and not default.

[Sébastien Gouëzel]

Interesting (and surprising to me) comment of @Sebastian Ullrich on the issue:

I believe this amounts to a misuse of def which is hard/unlikely to be addressed across the entire elaborator. Because of its context-dependent reducibility, the main difference of def to abbrev is performance-related, it should not be used to create semantically distinct types. Actually irreducible declarations like structure should be the preferred way for doing so.

I read this as a "won't fix", if I understand correctly.

[Kevin Buzzard]

So type synonyms literally don't work any more and this won't be fixed?

[Jireh Loreaux]

Posted this also on GitHub, but I'm not sure where is the preferred place for conversation about it (since this is in the Mathlib4 stream, but the GitHub issue is on the Lean4 repo):

Aside from the fact that this is ubiquitous throughout Mathlib, I really don't understand the idea that this is misuse of def. If it were the case that default transparency is the correct setting for instance synthesis, then it should always work. But, unsurprisingly, this doesn't:

class Foo (α : Type) where

instance : Foo Unit where

def Unit' := Unit

#synth Foo Unit' -- fails

That's because we have a different transparency setting for instance synthesis. As it currently stands, evidenced by this bug report, it's completely unpredictable whether unification will cause Lean to find an instance on a defeq type (not an abbrev) or not. That unpredictability seems like a problem to me.

If this really is supposed to be a misuse of def, then it argues that we should only ever write abbrev α := β or irreducible_def α := β or structure α where toBeta : β, and never def α := β, when β is a type.

[Matthew Ballard]

Jovan Gerbscheid said:

Lean's unification has the following feature: when unifying two applications of the same head constant (in this case ContinuousLinearMap), then in the (instance) implicit arguments it sets the reducibility to default (in this case in the argument of type TopologicalSpace (my_copy E)). It does this using the funtion withInferTypeConfig. Arguably, when checking the type of the assignment of an instance metavariable, the reducibility should be at most instances, and not default.

Why is this? What happens if you change this?

I confess to thinking of def as a mild semantic boundary.

[Eric Wieser]

Even with the assumed status quo, I think def α := β trips up enough new users that it should come with a linter warning that you have to silence with @[type_synonym] or something.

[Jovan Gerbscheid]

Matthew Ballard said:

Why is this? What happens if you change this?

I haven't tried it yet, but I would assume lots of things would fail if we were to change this. In particular, the change would be that when unifying in the instances transparency, and entering an instance implicit argument, we don't change the transparency level.