Better pp.analyze please!

Stream: lean4

[Alex Meiburg]

It's always frustrating when something doesn't unify and you think it should, in this case I got

application type mismatch
  Eq.trans h_sub
argument
  h_sub
has type
  ↑(⨆ i, ⨅ T, ⟨MState.exp_val ↑T ↑i, ⋯⟩) = ⨆ i, ↑(⨅ T, ⟨MState.exp_val ↑T ↑i, ⋯⟩) : Prop
but is expected to have type
  ↑(⨆ i, ⨅ T, ⟨MState.exp_val ↑T ↑i, ⋯⟩) = ?m.28873 : Prop

but when I say pp.analyze true I get the no-more-useful

application type mismatch
  Eq.trans h_sub
argument
  h_sub
has type
  ↑(⨆ i, ⨅ T, (⟨MState.exp_val ↑T ↑i, ⋯⟩ : { p : ℝ // 0 ≤ p ∧ p ≤ 1 })) = ⨆ i, ↑(⨅ T, ⟨MState.exp_val ↑T ↑i, ⋯⟩) : Prop
but is expected to have type
  ↑(⨆ i, ⨅ T, (⟨MState.exp_val ↑T ↑i, ⋯⟩ : { p : ℝ // 0 ≤ p ∧ p ≤ 1 })) = ?m.28873 : Prop

:sad:
(I tried setting pp.all true and pp.universes false and it makes VSCode hang. This is on 4.17.0-rc1)

[Alex Meiburg]

Actually, after clearing all the local variables I can, pp.all true doesn't hang any more, and the message is this. Which is still not very useful.

[Aaron Liu]

I analyzed this using a free online text comparison tool. Is the complete lattice arising from the complete linear order on Prob defeq to the complete lattice instance on Icc 0 1?

[Alex Meiburg]

Indeed it turned out it was not. (But it was propositionally equal.)

[Alex Meiburg]

I was able to move past this particular thing, but it's more just ... I would still really like a better way to highlight why unification fails.

[Alex Meiburg]

I admit I have no idea how to actually accomplish this in Lean, because I am not a Lean programmer. But I can imagine a world where it comes down to "pick the most atomic things in the expressions that were tested for defeq-ness and failed, and then expand pretty-printing up to that point to show which two failed".

[Aaron Liu]

That actually sounds doable

[Aaron Liu]

One thing you can do is to put a cast in between the terms, and then congr on the resulting goal.

[Alex Meiburg]

I did something similar to narrow it down - convert <term>, which pretty much does the congr automatically.

[Mario Carneiro]

There is a thing which does diff on the results of a type mismatch

[Mario Carneiro]

Or at least I thought so... lean has both an expression diff and a text diff tool but the former is only being used to diff goal states (for green/red highlights) and the latter is used to diff #guard_msgs output

[Kyle Miller]

An expression diff is definitely being used in "application type mismatch" errors. (It doesn't use the red/green highlighting yet however.)

[Kyle Miller]

(pp.analyze is only for trying to make expressions round trip; it doesn't interact with expression diff, and the interaction is not tested)

[Kyle Miller]

Can you give an MWE @Alex Meiburg?

There have been a number of improvements to this feature over the last handful of releases (e.g. #rss > Recent Commits to lean4:master @ 💬 ). We use examples to help improve it.

[Mario Carneiro]

It's possible that in this example the expression diff gives up early because the RHS are clearly different (metavariable vs expression), even though the actual reason it's a type mismatch is because of subtle differences on the LHS

[Kyle Miller]

I was thinking that, but the algorithm tries temporarily assigning metavariables during diffing.