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: An injectivity annotation must put the type family's result variable on the left-hand side.
+severity: error
+introduced: 9.6.1
+---
+
+This error occurs when the variable on the left-hand side of an injectivity annotation is not the type family's result variable.
+
+Type families in Haskell define type-level functions. In `type family F a = r | r -> a`, the injectivity annotation `| r -> a` states that the result type `r` uniquely determines the input type `a`: equal results imply equal inputs. The left-hand side must be the result variable `r` named after `=`, and the right-hand side lists the input variables determined by that result.