Type/data instances: require that the instantiation is determined by the LHS alone
GHC Proposal #425 "Invisible binders in type declarations" restricts the instantiation of type and data family instances as follows:
- In type family and data family instances, the instantiation is fully determined by the left hand side, without looking at the right hand side.
For example, here is a definition accepted today:
type family F a :: k
type instance F Int = Char
type instance F Int = Maybe
Even though the left-hand sides of the two equations are identical, they instantiate k
differently (based on the kind inferred for the RHS), and hence are distinct instances.
With the proposed change, this will no longer be accepted. The instantiation must be fully determined by the LHS alone. The example can be rewritten as follows:
type family F a :: k
type instance F @Type Int = Char
type instance F @(Type->Type) Int = Maybe
Now we can see that those are different instances by looking at the LHS alone.