[Ur] The future of [class] declarations

[Adam Chlipala]

The type class machinery of Ur/Web is a bit unsatisfying at the moment.  
There is a [class] declaration form, which is able to add new type 
classes locally, and one can even declare new instances (properly typed 
[val] declarations) shortly afterward and get them added to an internal 
database.  However, these instances generally won't be picked up for 
automatic resolution within the current module, because the type checker 
tries to "help" and expand out type class definitions, so that it's no 
longer obvious one is working with a particular type class.

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.

Any opinions?