inference of instances

Stream: lean4

[Alexandre Rademaker]

Consider

variable (α β : Type)
  [ToString α] [ToString β]
  [BEq α] [BEq β] [Hashable α] [Hashable β]

inductive Action where
 | reject    : β → α → Action
 | accepted  : β → α → Action
 | replaced  : β  → α → α → Action
 deriving Repr

when I tried

instance : ToString (Action α β) where
 toString a := repr a |> toString

and I got

failed to synthesize
  Repr (Action α β)

I didn't get any info about the missing instances of Repr for α and β

[Paul Reichert]

This works:

instance [Repr α] [Repr β] : ToString (Action α β) where
 toString a := repr a |> toString

Lean can only generate a Repr (Action α β) instance based on Repr α and Repr β instances.

[Robin Arnez]

I think the problem here is rather that you aren't being told that you might've needed Repr α or Repr β. This information can be seen indirectly through set_option trace.Meta.synthInstance true though

[Alexandre Rademaker]

The question is whether this is expected or not. I would expect Lean to complain about the missing [Repr α] and [Repr β] additional necessary restrictions.

[Kyle Miller]

It would be nice to attribute reasons to typeclass failures, but I don't think there's any obvious algorithm for how to do it. Certainly if there's just a single instance that applies Lean could commit to it, which would help in this particular example, but in general it seems like a problem that requires designing heuristics.

I remember at ICERM this year in a group with @Oliver Nash, @Eric Wieser, and others trying to brainstorm possible heuristics, but I'm forgetting what we came up with.

[Kyle Miller]

A problem here is that typeclasses aren't restrictions. Typeclass synthesis is like running a Prolog program. When a Prolog program outputs no solutions, what should it say to explain why there were none?

[Eric Wieser]

The proposal I made was to be able to tag instances as "structural", with semantics:

• Perform the search the same way as we do now
• If no match is found, follow the largest subree of "structural" edges in the graph of explored instances (from the root), and then report the remaining nodes as an error to the user

[Eric Wieser]

The instance above would be tagged in this way, as would things like docs#Prod.instGroup

[Eric Wieser]

Things like docs#CommGroup.toGroup would not be

[Eric Wieser]

Probably you could do the majority of the tagging automatically with a heuristic of "conclusion matches Class _ _ _ (Head _ _) where Head is a constant and not a free variable", but I think manual tagging could go a long way

[Kyle Miller]

Thanks for reminding me of the details! Now I recall there was also an idea we discussed of adding cuts that are activated during error attribution (cuts in the sense of the Prolog cut operator), though I don't remember if we thought that was something that would be usable, or that was a basis for implementing your idea.

Maybe the heuristic for "structural" has something to do with instances that reflect the intuition of typeclasses-as-constraints.

[Eric Wieser]

In my head that cut idea is the same as the one I just described, just phrased in a different way.