[Ur] The future of [class] declarations

[Adam Chlipala]

Karn Kallio wrote:
>> So, one alternative would be this: Remove [class] declarations but keep
>> [class] signature items.  This means type classes would only be a
>> concept in the module system.  Automatic resolution would only happen
>> for a type class hidden behind opaque signature ascription of a module,
>> though instances could then be declared elsewhere in the current way.
>> This is actually pretty close to what is de facto implemented right now,
>> so perhaps the [class] declaration is just a distraction.
> Perhaps a better alternative is to make instances get picked up in the
> current module (preserving the class declaration as it is).

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:

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.  With the current type class implementation, there is no 
worry about breaking type inference by replacing a type annotation with 
another, definitionally equal type, whereas that worry would necessarily 
appear with this straw man change.

One option would be to somehow make type classes abstract, even in their 
modules of definition.  Then there is the complication of how one 
defines a new instance in such a context, which seems to grow 
substantially more complex than the current "a type class is just a type 
family with a bit set to ask 'please infer my instances.'"  Yet the 
module system provides a natural means of segregating code that needs to 
know a definition from code that doesn't!

Talking through all this, I think I'm more convinced than before that I 
should implement the proposal quoted at the top of this message, but I 
might still be convinced otherwise. :)