The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 03/14/2013 08:47 PM, Ben Lerner wrote:
> Or might there be a Hint form that typeclass resolution could take, to
> tell it that it's ok to leave some goals unproven after normevars?
What do you expect to happen in case of overlapping instances?

Instance proper1: forall x, A x -> Proper bla (f x)
Instance proper2: forall x, B x -> Proper bla (f x)

What would you expect to happen here? A goal "A x \/ B x", to 
non-deterministically get the goal "A x" or "B x"? To get the goal 
belonging to the first declared instance?

Besides, the premisses of a hint (or instance) can also have arrows in 
them, making the situation even more peculiar.

Robbert