Prototype work for closed type families

 * reject equations with unused tyvars in the RHS
 * reject equations that use type families
 * erro fix for open type families
Provisional injectivity check for closed type families