rage

Stream: general

[Alex Meiburg]

recommended ways to deal with this? so far I have "turning on pp.all true", "chocolate or tea", and "video games"
image.png

[Adam Topaz]

#mwe ?

[Adam Topaz]

do you have two isntances of some class around?

[Alex Meiburg]

I could make one but it'd be a pain, I'm not really asking for help in this particular scenario, just like "when you see this error message what is the first things you think"

[Alex Meiburg]

and wanting to vent :P

[Riccardo Brasca]

try convert instead of apply/exact

[Adam Topaz]

I understand :)

[Adam Topaz]

yeah, convert will tell you the difference. My first guess is that there are two incompatible instances of some class.

[Alex Meiburg]

Ah, the issue (in this case) was this. AffineMap is defined by

structure AffineMap (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*}
  (P2 : Type*) [Ring k] [AddCommGroup V1] [Module k V1]
  [AffineSpace V1 P1] [AddCommGroup V2] [Module k V2] [AffineSpace V2 P2] where ...

and so affine maps from a module [Module M R] to a ring [Ring R], over that ring R, are written in notation as M →ᵃ[R] R.

But there are two sort of "natural" meanings to that notation:
@AffineMap R M M R R, or @AffineMap R R M R R. The first is inferring

[AddCommGroup V1] [Module k V1] [AffineSpace V1 P1]

with V1 := M and P1 := M, which has the AddCommGroup and Module structure of M over R, and the AffineSpace of M over itself.

The second is inferring V1 := R and P1 := M, which only the AddCommGroup structure over R and the Module structure of R over itself, and the AffineSpace of M over R (derived from being a module).

But those are different types that render with the same notation!

ayiyi...

[Alex Meiburg]

I feel like my linear algebra isn't strong enough to actually say if those are secretly the same type under some isomorphism, or if they're meaningfully distinct, and in that case, which I want! harumph!

[Alex Meiburg]

mm, seems the "bad" inference was caused by having an extra instance of [AddTorsor R M] lying around. Didn't need that, didn't want that, caused it use that instance instead and deduce the bad value for V1. (should've been M not R)

[Yury G. Kudryashov]

Most probably, your affine space is not an add torsor over the base ring.

[Martin Dvořák]

I also find these parts challenging.

[Julian Berman]

It would be great if Lean at least sent enough information to show at least a suggestion of what to do in VSCode/an editor

[Bolton Bailey]

"If these terms seem like they should unify, it is possible that implicit arguments do not match. You can try using set_option pp.explicit true to see the full explicit terms"

[Bolton Bailey]

Is what the error message should say.

[Joachim Breitner]

No, the error message should show the proofs with explicit or raw arguments when needed, maybe with a comment
“(shown here with pp.explicit := true, as otherwise the terms look identical)” added. It’s just plain silly to offer the user an error message saying two identical things differ. Filed as lean4#3232.

[Bolton Bailey]

Joachim Breitner said:

No, the error message should show the proofs with explicit or raw arguments when needed, maybe with a comment
“(shown here with pp.explicit := true, as otherwise the terms look identical)” added. It’s just plain silly to offer the user an error message saying two identical things differ. Filed as lean4#3232.

This is an even better suggestion, I encourage people who have been affected by this problem before to give that issue an upvote.

[Bolton Bailey]

(I was a little nervous about telling the lean maintainers to do something that complicated given how many hoops you have to jump through to even submit a PR to that repo, but I agree that this would be better)

[Joachim Breitner]

I understand; I probably wouldn’t have phrased my suggestion just as bluntly if I weren’t part of the addressed group here :-)

[Joachim Breitner]

Do you find contributing to lean unnecessary hard?

[Alex Meiburg]

The thread linked (on GH issue) of https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Why.20failing.20to.20unify.3F suggests an even more ambitious way to do useful suggestions. When faced with

tactic 'apply' failed, failed to unify
  1 • ?b = ?b
with
  1 • b = b

one could imagine a regex parser that realizes that, in fact, the string 1 • b = b matches the string pattern 1 • ?b = ?b and then (tries to) suggest something in more detail about what's going wrong. Of course a _full_ set of useful suggestions/explanations could be extremely difficult, as complicated as unification itself -- but, I dunno, maybe some cases...

One could imagine a scenario where it tries to convert the 1 • b = b into the necessary form, removing the ?bs, and then instead it could print out something like couldn't synthesize instance [SMul (ℕ → F)] or whatever the appropriate thing is.

I have no idea how hard that is :upside_down: in like a https://xkcd.com/1425/ sense

[Bolton Bailey]

Joachim Breitner said:

Do you find contributing to lean unnecessary hard?

I have not attempted to contribute to lean because the contribution guidelines give me the sense that I have to establish a clear consensus on the part of the community before a PR will be considered, and that seems hard to do. I was going to start a PR for this issue but then I got told I had to make an RFC first, and by the time I did that it seems you got in first with the bug report. I guess classifying this behavior as a bug maybe makes the process easier? It doesn't seem like what I would call a bug, but if that sidesteps having to convince a bunch of people from the forum to come and upvote the issue, that's fine by me.

[Kyle Miller]

I think it counts as a usability bug -- we've all been bit by this. Having the issue means it's easier to keep track of :+1:'s as a measure of how much it impacts the community.

We might still need an RFC of some sort. It's not clear to me what the right design is for something that tries to explain why two terms are not defeq. There are approximate solutions that insert pp.explicit hints where terms differ (and hopefully do something sensible when there is notation), and there are complicated solutions that make the defeq algorithm be self-explaining on failure.

[Bolton Bailey]

How many upvotes are even required before an RFC is eligible to have a PR made for it? Is it even a hard requirement? The contribution guidelines do not make this clear.

[Joachim Breitner]

Sebastian pointed me to an existing function that helps here, so at least using that in apply is a no-brainer I’d say, and I PRed that (lean4#3234). It’s probably necessary to keep the bar for contributions a bit high, as a filter to not be distracted by crazy, half-baked, disruptive ideas. But personally I’d suggest to apply common sense: If there is something that annoys you as a regular user, e.g. a bad error message, then that' doesn’t need a RFC in my view, the PR will describe the idea well enough.

[Kyle Miller]

Fundamentally, for contributing you need to know if a PR is going to be something that the Lean developers will want to merge. Having :+1:'s is not a requirement, but it can be used by the Lean developers to decide what features to pursue. Community consensus is a part of the process, but even if there's consensus that doesn't mean a PR will be merged.

This does add friction to the process, and it can be hard to tell how much effort to put into the different stages of trying to contribute to the project.

[Bolton Bailey]

One person's common sense is unfortunately often another person's nuanced issue. The RFC template asks if the change will streamline the code or make it harder to maintain, and in this case it seems like the latter to me, so unfortunately I would not have been confident enough on my own to make a PR here without at least a few upvotes on my RFC. I am left with the sense in my heart of hearts that if you all hadn't swooped in to save the day at the right moment, this issue would not have gotten traction.

But if this is anyone's fault it's that of people like me who are not confident enough to forcefully move the ball forward on issues. I appreciate your all's help and willingness to apply your talents and submit Github issues and PRs for this. I will try to be more proactive in the future about submitting RFCs and PRs when I encounter pain points.

[Joachim Breitner]

It's also perfectly fine to rant on Zulip until someone picks it up. there are many ways to help, and if an issue alloys enough people, and these people learn that they are not alone in their annoyance, eventually one of them will likely act. (Or else it wasn't annoying enough :-))

[Mario Carneiro]

annoying enough to the devs?

[Mario Carneiro]

It's entirely possible that something very annoying and frequent to a user doesn't show up as an issue to the devs

[Julian Berman]

@Bolton Bailey if it helps to hear I thought of what Joachim filed but also tapered the message I sent for the reasons you mentioned :). But clearly it's good as we still got to some chance of improvement.

[Joachim Breitner]

I’m annoyed when my users are annoyed, so as long as annoyance is radiated, there is a chance it can get fixed :-)