The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/18/2016 06:09 AM, Soegtrop, Michael wrote:
> Dear Guillaume,
>
> > There has been a lot of confusion in this thread. While decidable equality is
> > the reason why it is possible in the first place, Coq does not care about it 
> > at
> > all. As Hugo explained, Coq just happens to implement a limited version of
> > the small inversion trick.
> Thanks for the clarification!
>
> I wonder if it wouldn't be a better approach to have a type class for decidable 
> equality (in the standard library) and a variant of UIP_dec which takes an instance of 
> such a type class to solve "Proof irrelevance of equalities" goals. It would 
> be a simple apply with some straight forward type class inference then.

One can already do this, to some extent.  The procedure involves 
declaring sumbool to be an Existing Class, and then declaring each 
decidable equality an Existing Instance.  Then, applying 
Eqdep_dec.UIP_dec will automatically infer the necessary instance.

I've used this in https://github.com/jonleivent/deptacs.

I'm not so much a fan of Existing Class as a standard way to get this 
done, mostly because it is not a controllable declaration (there is no 
Local variant, and it greedily makes instances out of all subsequent 
matching declarations (but not definitions!).). Having an alternative 
definition of UIP_dec that expects an actual typeclass instance instead 
would be better, if all of the individual eqdec definitions were instances.

-- Jonathan