The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

I'm trying to use typeclass inheritance (using :>) to model a specialization hierarchy in which subclasses provide values for certain fields that are declared but left abstract in a superclass. This seems not possible. Can someone (a) confirm, and (b) suggest an alternative design pattern. 

The problem: it appears that a super-typeclass has to be fully instantiated before one can instantiate a subclass, but values defined in a subclass are unavailable until the subclass is instantiated -- catch 22. 

In a little more detail, I want to provide an implementation, in a subclass, of a function that is declared but not defined in a type superclass. The implementation is defined in terms of other functions introduced in the subclass.

Kevin