diff --git a/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/after/Test.hs b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/after/Test.hs
new file mode 100644
index 00000000..43560757
--- /dev/null
+++ b/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
diff --git a/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/before/Test.hs b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/before/Test.hs
new file mode 100644
index 00000000..5894d4c5
--- /dev/null
+++ b/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
diff --git a/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/index.md b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/index.md
new file mode 100644
index 00000000..925e4804
--- /dev/null
+++ b/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.
diff --git a/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/after/Test.hs b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/after/Test.hs
new file mode 100644
index 00000000..9090bb07
--- /dev/null
+++ b/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
diff --git a/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/before/Test.hs b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/before/Test.hs
new file mode 100644
index 00000000..e7da0dcd
--- /dev/null
+++ b/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
diff --git a/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/index.md b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/index.md
new file mode 100644
index 00000000..5c2f2866
--- /dev/null
+++ b/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.
diff --git a/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/after/Test.hs b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/after/Test.hs
new file mode 100644
index 00000000..9739c836
--- /dev/null
+++ b/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
diff --git a/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/before/Test.hs b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/before/Test.hs
new file mode 100644
index 00000000..f4db1602
--- /dev/null
+++ b/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
diff --git a/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/index.md b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/index.md
new file mode 100644
index 00000000..6fb402fb
--- /dev/null
+++ b/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.
diff --git a/message-index/messages/GHC-88333/index.md b/message-index/messages/GHC-88333/index.md
new file mode 100644
index 00000000..ff258ee1
--- /dev/null
+++ b/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.