Note [Injective type families]
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
- Verifying injectivity annotation GHC.Core.FamInstEnv
- Type synonym families GHC.Core.TyCon
- Type inference for type families with injectivity GHC.Tc.Solver.Equality
- Language.Haskell.Syntax.Decls call site