Changed approach to unification
Instead of failing immediately, maintain a list of blocked problems and
refine during elaboration.
Add a reducing version of believe_me (be careful!)
Fix mysterious "no such variable" bug
Arguments under type constructors are not forceable!
HNF in unification to speed things up
Distinguish parameters and indices internally in data types
This doesn't do anything, yet, but will become important soon!
Some progress on implementation paper revisions
More sane scoping rules for where/type classes
Parameters in the type signature get propagated, indices do not.
So you no longer need to pass parameters explicitly if you need them
in a where clause, and you no longer need to give explicitly typed
helpers in type class instances for types with indices.
Small library tweaks and documentation update
Magic with explanation in impl-paper