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..16512a7d --- /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: 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.