Add GHC-88333

message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/after/Test.hs

@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+module IncorrectTypeVarLHSInjectivityCondition where
+
+class Fcl a where
+  type Ft a = r | r -> a

message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/before/Test.hs

@@ -0,0 +1,4 @@
+module IncorrectTypeVarLHSInjectivityCondition where
+
+class Fcl a where
+  type Ft a = r | a -> a

message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/index.md

@@ -0,0 +1,5 @@
+---
+title: Incorrect type variable on the LHS of injectivity condition
+---
+
+In the example, the associated type family Ft is defined with an incorrect injectivity annotation. The left-hand side (LHS) of the injectivity condition should be the output type variable (r), but in the definition, it is the input type variable (a). This is what the error message is referring to.

message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/after/Test.hs

@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+module IncorrectTypeVarLHSInjectivityCondition where
+
+type family Fc a = r | r -> a where
+  Fc a = a

message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/before/Test.hs

@@ -0,0 +1,4 @@
+module IncorrectTypeVarLHSInjectivityCondition where
+
+type family Fc a = r | a -> a where
+  Fc a = a

message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/index.md

@@ -0,0 +1,5 @@
+---
+title: Incorrect type variable on the LHS of injectivity condition
+---
+
+In the example, type family Fc is defined with an incorrect injectivity annotation. The left-hand side (LHS) of the injectivity condition should be the output type variable (r), but in the definition, it is the input type variable (a). This is what the error message is referring to.

message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/after/Test.hs

@@ -0,0 +1,6 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+module IncorrectTypeVarLHSInjectivityCondition where
+
+type family F a = r | r -> a

message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/before/Test.hs

@@ -0,0 +1,3 @@
+module IncorrectTypeVarLHSInjectivityCondition where
+
+type family F a = r | a -> a

message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/index.md

@@ -0,0 +1,5 @@
+---
+title: Incorrect type variable on the LHS of injectivity condition
+---
+
+In the example, type family F is defined with an incorrect injectivity annotation. The left-hand side (LHS) of the injectivity condition should be the output type variable (r), but in the definition, it is the input type variable (a). This is what the error message is referring to.

message-index/messages/GHC-88333/index.md

@@ -0,0 +1,10 @@
+---
+title: Incorrect type variable on the LHS of injectivity condition
+summary: Injectivity annotations are used to constrain type families, so that for a given input type, there is exactly one output type.
+severity: error
+introduced: 9.6.1
+---
+
+This error is about the incorrect use of type variables in the injectivity condition of type families.
+
+Type families in Haskell are a way to define type-level functions. An injectivity annotation (| a -> r) is used to specify that for a given input type a, there is exactly one output type r that the type family can map to.