-
Iavor S. Diatchki authored
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.
b2fa2d41