Make type-level evaluation work with :kind!

The main change is to add a case to `reduceTyFamApp_maybe` to evaluate
built-in type constructors (e.g., (+), (*), and friends).

To avoid problems with recursive modules, I moved the definition of
TcBuiltInSynFamily from `FamInst` to `FamInstEnv`.  I am still not sure if
this is the right place.

There is also a wibble that it'd be nice to fix:

when we evaluate a built-in type function, using`sfMatchFam`, we get
a `TcCoercion`.  However, `reduceTyFamApp_maybe` needs a `Corecion`.
I couldn't find a nice way to convert between the two, so I resorted to
a bit of hack (marked with `XXX`).

The hack is that we happen to know that the built-in constructors for
the type-nat functions always return coercions of shape `TcAxiomRuleCo`,
with no assumptions, so it easy to convert `TcCoercion` to `Coercion`
in this one case.  This is enough to make things work, but it is clearly
a cludge.

0 files changed, 0 insertions, 0 deletions