The Coq mailing list

[Ben Lerner <blerner AT cs.brown.edu>]

On 3/15/2013 6:12 AM, Robbert Krebbers wrote:
> 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
In that particular instance, it seems no more confusing than how 
"f_equiv" picks the first one it finds that unifies.  I like the 
\/-construction, but I see how this could get tricky, fast.  I don't 
see, though, how having hints with preconditions is an issue here: 
currently the hint either solves the goal or coq complains; so more 
precomditions just make it less likely to be a helpful hint.

Of course, the one unambiguous hint would be to write "rewrite ... using 
morphism proper1"...but at that point you're no longer needing the 
rewrite tactic itself...