Note [Injective type families]

GHC/Core/TyCon.hs:414 compiler

We allow injectivity annotations for type families (both open and closed):

  type family F (a :: k) (b :: k) = r | r -> a
  type family G a b = res | res -> a b where ...

Injectivity information is stored in the `famTcInj` field of `FamilyTyCon`.
`famTcInj` maybe stores a list of Bools, where each entry corresponds to a
single element of `tyConTyVars` (both lists should have identical length). If no
injectivity annotation was provided `famTcInj` is Nothing. From this follows an
invariant that if `famTcInj` is a Just then at least one element in the list
must be True.

See also:
 * [Injectivity annotation] in GHC.Hs.Decls
 * [Renaming injectivity annotation] in GHC.Rename.Module
 * [Verifying injectivity annotation] in GHC.Core.FamInstEnv
 * [Type inference for type families with injectivity] in GHC.Tc.Solver.Equality

References 0

This Note does not link to any other.

Referenced by 4