[Ur] The future of [class] declarations

[Adam Chlipala]

Karn Kallio wrote:
>> Well, while Ur is full of undecidable type inference issues, I generally
>> try to keep type _checking_ (of sufficiently annotated programs)
>> decidable or at least predictable.  It seems hard to support predictable
>> checking of same-module type class usage without requiring restrictions
>> that don't apply elsewhere.  To explain:
>>
> If picking up the instances must lead to undecidable type checking then
> removing the class declaration seems very good to me.  Yet if the restrictions
> you mention could be mild while still leaving type checking decidable and
> allowing instance detection then maybe keeping the class declaration could be
> considered.  What sort of restrictions would be required?

The restriction would be that it is not always legal to replace a type 
annotation with another that is definitionally equivalent.

>> When a type class is considered as an abstract type-level function, I
>> believe it is decidable whether a particular type equals an application
>> of the class.  However, when inference must be done where a type class's
>> definition is exposed, I _think_ the problem is clearly undecidable,
>> being an easy reduction target for the problem of higher-order
>> unification.
> So I guess a sufficient (but perhaps too onerous) restriction could be for the
> programmer to provide annotations showing which types are class applications?

I can certainly imagine some feature marking mentions of type family 
identifiers, saying "don't unfold the definition here."  But that seems 
too groaty to me, so I'm going to implement my original proposal. :)