Custom errors during instance synthesis?

Stream: lean4

[David Thrane Christiansen]

When using type classes for overloaded notation, I'd like to be able to provide custom error messages for intentionally-missing instances.

For instance, if I have a type of positive numbers, then it would be nice to make it so that attempting to synthesize an OfNat Positive Nat.zero gives a message like 0 is not positive instead of failed to synthesize instance OfNat Positive 0.

In Haskell, there's the TypeError constraint that causes GHC to fail with a given message. If Lean had it, then I could write something like:

instance [Fail "0 is not positive"] : OfNat Positive 0 where
  ofNat := Fail.failed

Here, failed is intended to make use of some evidence that Fail is uninhabited to discharge obligations in the instance.

Alternatively, I could imagine some way to add a custom hook through the metaprogramming API.

Is there some way to do what I'm thinking of here?

[Henrik Böving]

There is to my knowledge no way to do this right now, although I do think it sounds like a good idea.

[Mario Carneiro]

What if there was another way to find the instance? Would the failure take precedence?

[David Thrane Christiansen]

I would expect that the Lean would follow the usual instance search rules, including rules like "later takes precedence over earlier". If the final result ended up being Fail, then failure would be snatched from the jaws of victory.

This would allow things like improved default error messages in cases when an instance is missing, without it getting in the way of user definitions. For example, one could rewrite "failed to synthesize instance OfNat Foo 42" with "Can't interpret the numeric literal 42 as a Foo because no OfNat Foo 42 instance was found".

On the other hand, my main concern was finding out whether something like this exists already - I take this to mean that it doesn't :-)

[Mario Carneiro]

For example, one could rewrite "failed to synthesize instance OfNat Foo 42" with "Can't interpret the numeric literal 42 as a Foo because no OfNat Foo 42 instance was found".

That message is actually just a fancy way to explain the type of the goal, so I think you could do this without Fail, you would just need some kind of unexpander setup on the final error message

[David Thrane Christiansen]

That's a good point. Can you point me to any examples I can grep for in the source? I haven't written an unexpander yet :-)

[Mario Carneiro]

If Fail acts like a real instance, then I would worry about it getting spuriously picked in unrelated searches. For example, we want to prove Inhabited (Fin 1), so we use an instance saying OfNat (Fin 1) ?n |- Inhabited (Fin 1) (this would be a bad idea but let's just say this exists), and then Fail |- OfNat (Fin 1) 2 matches and you miss the other instance which directly proves Inhabited (Fin 1)

[Mario Carneiro]

If that fail instance hadn't been provided it would have found the normal instance

[Mario Carneiro]

I actually was just suggesting a possible way to implement this. There is currently no support for customizing the type class failure error message

[Mario Carneiro]

The idea would be that it calls throwTypeclassFailure ty given the type of the goal, and this is a user extensible function so you can say e.g. if ty = OfNat (Fin m) n and m < n then throwError "{n} is not a member of `Fin {m}`"