Non-canonical instances kill where notation

Stream: lean4

[Yaël Dillies]

Where are we at in removing the new Lean 4 behavior of not letting instance arguments being filled in by unification? I just got hit by a nasty occurrence of it: After #15021, Kernel.mk takes [MeasurableSpace α] [MeasurableSpace β] as instance arguments

class MeasurableSpace (α : Type) where
  foo : Nat

structure Kernel (α β : Type) [MeasurableSpace α] [MeasurableSpace β] where

def myKernel (α : Type) {noncanonical : MeasurableSpace α} [canonical : MeasurableSpace α] :
    @Kernel α α noncanonical canonical where

/-
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  canonical
inferred
  noncanonical
-/

[Notification Bot]

3 messages were moved from this topic to #Zulip meta > Weird whitespace in code snippets by Eric Wieser.

[Eric Wieser]

:= {} also fails in the same way; you need := @Kernel.mk _ _ (_) (_) to make this work

[Yaël Dillies]

I know. That's precisely what I am complaining about.

[Yaël Dillies]

If there was a way to customise the constructor that where notation uses (wink wink), I could just rename Kernel.mk to Kernel.mk and roll my own constructor with the correct implicitness, but that's currently not the case.

[Yaël Dillies]

May I also complain that this "synthesized type class instance is not definitionally equal to expression inferred by typing rules" error is really unhelpful for debugging? Since it doesn't tell me which part of the expression the typeclass was found in and since it prevents type-checking, all I can do is guesswork to figure out which part of the expression is causing the issue.

[Yaël Dillies]

In this specific case, it took me a solid 15min of debugging to find out that the where was the cause of the error (it was used in a pretty chunky definition whose parts I could not easily remove).

[Kyle Miller]

Where are we at in removing the new Lean 4 behavior of not letting instance arguments being filled in by unification?

What's the context of this? As far as I know, there is no plan to backtrack on this feature, so I'm not sure what you mean by "where are we at in removing [it]".

It helps prevent noncanonical instances from slipping into expressions, which can lead to much worse debugging issues.

[Kyle Miller]

May I also complain that this "synthesized type class instance is not definitionally equal to expression inferred by typing rules" error is really unhelpful for debugging?

Sure, I think it should be possible to say which argument of which expression is at fault. Feel free to create an issue explaining how debugging this error can be difficult.

[Yaël Dillies]

Kyle Miller said:

What's the context of this? As far as I know, there is no plan to backtrack on this feature, so I'm not sure what you mean by "where are we at in removing [it]".

Oh, when we talked about it in Bonn last September I had understood you had something in the works to make the new behavior useful against accidental noncanonical instances while allowing conscious ones. My understanding was along the lines of "We only want to forbid simp from using non-canonical instances, but we instead forbid everyone (including the user). Let's not be so drastic.".

[Kyle Miller]

Hmm, I remember talking about simp, though not the specifics. What ended up happening in the meantime is that simp now allows non-canonical instances via unification (in particular, it allows skipping synthesis resynthesis, which is also good for performance). For general elaboration though, it seems like relaxing this would create lots of confusing issues, so I would not expect to see it.

[Kyle Miller]

If I remember correctly, even Lean 3 was strict about this.

[Kyle Miller]

Here: https://github.com/leanprover-community/lean/blob/f91b574c40ad862c5134d48995ad083fe48e4cd4/src/frontends/lean/elaborator.cpp#L3633-L3634

[Yaël Dillies]

Interesting... that definitely disagrees with my (remembered) experience of Lean 3: [] arguments are unified if possible, and filled in by typeclass search if not

[Eric Wieser]

A compromise here might be to make these messages (disableable) warnings rather than errors

[Yaël Dillies]

Yes, certainly it is strange that Lean tells me "I can do this but I don't want to. Error." rather than just doing it + maybe warning me.

[Kyle Miller]

that definitely disagrees with my (remembered) experience of Lean 3

I think we've collectively misremember this (I too thought this was a new Lean 4 feature for awhile), but perhaps we're just remembering that simp was more restrictive in Lean 4 until the changes I mentioned. I can't see anywhere that the Lean 3 elaborator would skip this defeq check.

Eric's idea is interesting, and I think it's worth an RFC. I don't think we'll see disableable warnings, but I think we could see, perhaps, warnings in all contexts where errToSorry is true and errors where it's not, expanding the meaning of errToSorry.

[Yaël Dillies]

Should I open a single RFC for both of mine and Eric's suggestion, or should they be two separate RFCs? The context and motivation are the same, but maybe they will be fixed separately.

[Kyle Miller]

Good question — I think yours could be an issue and Eric's suggestion could be a related RFC (or issue)? It's good to have usability issues clearly explained without any reference to a proposed solution. Eric's is on the edge between an issue and an RFC; the issue is that elaboration errors are getting in the way of debugging or otherwise working with the terms, and it's easily recoverable so there's no reason to be so strict.

[Eric Wieser]

I don't think we'll see disableable warnings,

These are called linters, right?

[Kyle Miller]

A counterargument to relieving strict errors is that it can lead to compounding errors, and these can be confusing if you don't know the precipitating error.

[Eric Wieser]

I'm thinking of Yael's situation, where they'd prefer to write an "I know what I'm doing" command of some kind rather than writing the ugly (_) thing.

[Kyle Miller]

@Eric Wieser Certainly, but I don't mean whether disableable warnings are technically possible. I mean I doubt we'll see this be a disableable warning.

[Kyle Miller]

I take this back slightly — it's plausible (but still very unlikely anytime soon) that there could be a flag for instance metavariables that disables the defeq check. Then, there could be a term elaborator, like imagine (with_relaxed_instances% {} : @Kernel α α noncanonical canonical), but given the fact that there are easy (even if slightly annoying) workarounds I would be surprised to see it implemented.

[Yaël Dillies]

Kyle Miller said:

I think yours could be an issue and Eric's suggestion could be a related RFC (or issue)?

I can't make a non-rfc non-bug issue though. Do you mean my suggestion should be a bug issue?

[Eric Wieser]

Yaël Dillies said:

I can't make a non-rfc non-bug issue though.

yes you can

[Eric Wieser]

(there is a "create a blank issue" button below the two you saw)

[Yaël Dillies]

lean#5085, lean#5086