[Ur] The future of [class] declarations

[Karn Kallio]

> 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?
 
> 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?

Also, now that you are a professor, maybe you could put a student to showing
undecidability by working through your reduction!