Type/data instances: require that variables on the RHS are mentioned on the LHS

GHC Proposal #425 "Invisible binders in type declarations" restricts the scope of type and data family instances as follows:

• In type family and data family instances, require that every variable mentioned on the RHS must also occur on the LHS.

For example, here are three equivalent type instance definitions accepted today:

type family F1 a :: k
type instance F1 Int = Any :: j -> j

type family F2 a :: k
type instance F2 @(j -> j) Int = Any :: j -> j

type family F3 a :: k
type instance forall j. F3 Int = Any :: j -> j

• In F1, j is implicitly quantified and it occurs only on the RHS;
• In F2, j is implicitly quantified and it occurs both on the LHS and the RHS;
• In F3, j is explicitly quantified.

As the result of the proposed change, F1 will be rejected with an out-of-scope error, while F2 and F3 will continue to be accepted.