Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information