:10:15: error: Type family equations violate injectivity annotation: F Char Bool Int = Int -- Defined at :10:15 F Bool Int Char = Int -- Defined at :11:15 :16:15: error: Type family equations violate injectivity annotation: I Int Char Bool = Bool -- Defined at :16:15 I Int Int Int = Bool -- Defined at :17:15 :26:15: error: Type family equation violates injectivity annotation. RHS of injective type family equation cannot be a type family: IdProxy a = Id a -- Defined at :26:15 :34:15: error: Type family equation violates injectivity annotation. RHS of injective type family equation is a bare type variable but these LHS type and kind patterns are not bare variables: ‘'Z’ P 'Z m = m -- Defined at :34:15 :40:15: error: Type family equation violates injectivity annotation. Type variable ‘b’ cannot be inferred from the right-hand side. In the type family equation: J Int b c = Char -- Defined at :40:15 :44:15: error: Type family equation violates injectivity annotation. Type variable ‘n’ cannot be inferred from the right-hand side. In the type family equation: K ('S n) m = 'S m -- Defined at :44:15 :49:15: error: Type family equation violates injectivity annotation. RHS of injective type family equation cannot be a type family: L a = MaybeSyn a -- Defined at :49:15 :55:41: error: Type family equation violates injectivity annotation. Kind variable ‘k’ cannot be inferred from the right-hand side. (enabling -fprint-explicit-kinds might help) In the type family equation: PolyKindVarsF '[] = '[] -- Defined at :55:41 :60:15: error: Type family equation violates injectivity annotation. Kind variable ‘k1’ cannot be inferred from the right-hand side. (enabling -fprint-explicit-kinds might help) In the type family equation: PolyKindVars '[] = '[] -- Defined at :60:15 :64:15: error: Type family equation violates injectivity annotation. Kind variable ‘k’ cannot be inferred from the right-hand side. (enabling -fprint-explicit-kinds might help) In the type family equation: forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int -- Defined at :64:15 :68:15: error: Type family equation violates injectivity annotation. Type and kind variables ‘k’, ‘a’, ‘b’ cannot be inferred from the right-hand side. (enabling -fprint-explicit-kinds might help) In the type family equation: forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int -- Defined at :68:15 :81:15: error: Type family equations violate injectivity annotation: F1 [a] = Maybe (GF1 a) -- Defined at :81:15 F1 (Maybe a) = Maybe (GF2 a) -- Defined at :82:15 :85:15: error: Type family equation violates injectivity annotation. RHS of injective type family equation is a bare type variable but these LHS type and kind patterns are not bare variables: ‘[a]’ W1 [a] = a -- Defined at :85:15 :88:15: error: Type family equation violates injectivity annotation. RHS of injective type family equation cannot be a type family: W2 [a] = W2 a -- Defined at :88:15 :92:15: error: Type family equations violate injectivity annotation: Z1 [a] = (a, a) -- Defined at :92:15 Z1 (Maybe b) = (b, [b]) -- Defined at :93:15 :96:15: error: Type family equations violate injectivity annotation: G1 [a] = [a] -- Defined at :96:15 G1 (Maybe b) = [(b, b)] -- Defined at :97:15 :100:15: error: Type family equations violate injectivity annotation: G3 a Int = (a, Int) -- Defined at :100:15 G3 a Bool = (Bool, a) -- Defined at :101:15 :104:15: error: Type family equation violates injectivity annotation. Type variable ‘b’ cannot be inferred from the right-hand side. In the type family equation: G4 a b = [a] -- Defined at :104:15 :107:15: error: Type family equations violate injectivity annotation: G5 [a] = [GF1 a] -- Defined at :107:15 G5 Int = [Bool] -- Defined at :108:15 :111:15: error: Type family equation violates injectivity annotation. Type variable ‘a’ cannot be inferred from the right-hand side. In the type family equation: G6 [a] = [HF1 a] -- Defined at :111:15