Rust like kind error message

Stream: general

[Asei Inoue]

structure Point (α : Type) : Type where
  x : α
  y : α

def origin : Point Nat := ⟨0, 0⟩

/--
error: expression
  origin
has type
  Point Nat
but instance
  Lean.Eval (Point Nat)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
-/
#guard_msgs in
#eval origin

It seems to me that a suggestion could be made to ‘consider adding deriving instance Repr for Point’.

[Asei Inoue]

A similar proposal could be made for all typeclasses for which deriving is defined, except Repr.

[Mario Carneiro]

I think this is challenging because we don't really have a way to point at "what missing instance, if added, would make this instance synthesis work"

[Mario Carneiro]

in this example, you want to suggest Repr instead of Eval because there is an instance from one to the other; also the thing being eval'd might be (Point Nat × Nat) in which case there is a Repr instance for Prod but it failed after the initial application because of a missing Repr (Point A) instance

[Eric Wieser]

Maybe some mechanism for indicating that an instance is structural would help?

[Mario Carneiro]

what do you mean?

[Eric Wieser]

So that if an instance for Group (Prod A B) fails, we can assume that the user wanted to use Prod.instGroup since this produces the obviously useful error message, vs CommGroup.toGroup which does not

[Mario Carneiro]

Maybe just "preferred instance" to say that if there are multiple failing paths we should consider the ones that go through the most preferred instances

[Mario Carneiro]

Since in the above example we'd want to consider [Repr A] : Lean.Eval A as preferred even though it's not structural

[Kyle Miller]

For this particular case though, I've been planning on improving the error message for #eval to explain a few different ways to make #eval work.

[Kyle Miller]

(I think it would be neat to have it be able to use ToExpr as well, like in some code Mario shared a while back, since then you could hover over subterms in the result and see their types. And, maybe more importantly, have it rely on the main pretty printer.)

[Eric Wieser]

Mario Carneiro said:

Maybe just "preferred instance" to say that if there are multiple failing paths we should consider the ones that go through the most preferred instances

I think the algorithm is:

• Do instance search as normal
• If it fails, print our all leaves of the search tree of the subtree of nodes that are reachable only by "preferred instances" (and omit the intermediate branches)

[Mario Carneiro]

I don't think "all leaves" is viable, there are exponentially many in some cases

[Mario Carneiro]

I think it's better to have a scoring system and only show the best one

[Mario Carneiro]

Also, I expect you would have to rerun instance search in order to gather more information, because the default search needs to avoid the bookkeeping overhead

[Eric Wieser]

Mario Carneiro said:

I don't think "all leaves" is viable, there are exponentially many in some cases

Can you give an example?

[Asei Inoue]

I did not expect this issue to be challenging. Thank you for considering my views.