change how ADT/Rec are stored and used in type checking

Specifically we do not rely on tricks regarding on the names
of the ty/datacons or eliminators, but instead we go directly to
the reification in the environment.

Also, now formed types are stored in a canonical form, like data.
This will be helpful when checking for equality or unifying or
stuff like that.