From a16464f2cde2ead95100718b56c9c62b0c7cd86b Mon Sep 17 00:00:00 2001 From: Mauricio Date: Fri, 7 Jun 2024 11:26:00 +0200 Subject: [PATCH 1/3] Documented GHC-88333: Incorrect type variable on the LHS of infectivity condition --- .../after/Test.hs | 7 +++++++ .../before/Test.hs | 4 ++++ .../index.md | 5 +++++ .../after/Test.hs | 7 +++++++ .../before/Test.hs | 4 ++++ .../index.md | 5 +++++ .../after/Test.hs | 12 ++++++++++++ .../before/Test.hs | 3 +++ .../index.md | 5 +++++ message-index/messages/GHC-88333/index.md | 10 ++++++++++ 10 files changed, 62 insertions(+) create mode 100644 message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/after/Test.hs create mode 100644 message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/before/Test.hs create mode 100644 message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-associated-type-family/index.md create mode 100644 message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/after/Test.hs create mode 100644 message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/before/Test.hs create mode 100644 message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family-where/index.md create mode 100644 message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/after/Test.hs create mode 100644 message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/before/Test.hs create mode 100644 message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/index.md create mode 100644 message-index/messages/GHC-88333/index.md 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..a74c43a3 --- /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 \ No newline at end of file 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..840ae70d --- /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 \ No newline at end of file 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..7363fb09 --- /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 \ No newline at end of file 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..fb136938 --- /dev/null +++ b/message-index/messages/GHC-88333/incorrect-type-var-injectivity-condition-type-family/after/Test.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilyDependencies #-} + +module IncorrectTypeVarLHSInjectivityCondition where + +type family F a = r | r -> a + +-- Given input type a, there is exactly one output type r that the type family can map to +-- So, the uncommenting the lines below would be incorrect because it violates the injectivity condition +-- since the type family F would map both Char and Int to Double +-- type instance F Char = Double +-- type instance F Int = Double \ No newline at end of file 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..bc1f92ff --- /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 \ No newline at end of file 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. From 8dbe4a8d2ce96293c6f355235629cb4b3dcc6144 Mon Sep 17 00:00:00 2001 From: Mauricio Date: Fri, 7 Jun 2024 11:31:18 +0200 Subject: [PATCH 2/3] Documented GHC-88333: Incorrect type variable on the LHS of infectivity condition --- .../after/Test.hs | 8 +------- .../index.md | 2 +- 2 files changed, 2 insertions(+), 8 deletions(-) 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 index fb136938..b9f772e7 100644 --- 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 @@ -3,10 +3,4 @@ module IncorrectTypeVarLHSInjectivityCondition where -type family F a = r | r -> a - --- Given input type a, there is exactly one output type r that the type family can map to --- So, the uncommenting the lines below would be incorrect because it violates the injectivity condition --- since the type family F would map both Char and Int to Double --- type instance F Char = Double --- type instance F Int = Double \ No newline at end of file +type family F a = r | r -> a \ No newline at end of file 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 index 6fb402fb..d45c8d6d 100644 --- 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 @@ -2,4 +2,4 @@ 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. +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. \ No newline at end of file From 9cdea357db868dd1c6306ee54787cb44b45379cf Mon Sep 17 00:00:00 2001 From: Mauricio Date: Sun, 9 Jun 2024 13:22:23 +0200 Subject: [PATCH 3/3] AST: Remove Assert from GHC --- .../after/Test.hs | 2 +- .../before/Test.hs | 2 +- .../after/Test.hs | 2 +- .../after/Test.hs | 2 +- .../before/Test.hs | 2 +- .../index.md | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) 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 index a74c43a3..43560757 100644 --- 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 @@ -4,4 +4,4 @@ module IncorrectTypeVarLHSInjectivityCondition where class Fcl a where - type Ft a = r | r -> a \ No newline at end of file + 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 index 840ae70d..5894d4c5 100644 --- 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 @@ -1,4 +1,4 @@ module IncorrectTypeVarLHSInjectivityCondition where class Fcl a where - type Ft a = r | a -> a \ No newline at end of file + type Ft a = r | a -> a 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 index 7363fb09..9090bb07 100644 --- 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 @@ -4,4 +4,4 @@ module IncorrectTypeVarLHSInjectivityCondition where type family Fc a = r | r -> a where - Fc a = a \ No newline at end of file + Fc a = a 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 index b9f772e7..9739c836 100644 --- 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 @@ -3,4 +3,4 @@ module IncorrectTypeVarLHSInjectivityCondition where -type family F a = r | r -> a \ No newline at end of file +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 index bc1f92ff..f4db1602 100644 --- 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 @@ -1,3 +1,3 @@ module IncorrectTypeVarLHSInjectivityCondition where -type family F a = r | a -> a \ No newline at end of file +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 index d45c8d6d..6fb402fb 100644 --- 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 @@ -2,4 +2,4 @@ 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. \ No newline at end of file +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.