From 6e044db19db65f824837bfdc15ba3def0315b6e4 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Fri, 23 Jun 2023 18:49:32 -0400
Subject: [PATCH] Fix typechecking of promoted empty lists
The `'[]` case in `tc_infer_hs_type` is smart enough to handle arity-0 uses of
`'[]` (see the newly added `T23543` test case for an example), but the `'[]`
case in `tc_hs_type` was not. We fix this by changing the `tc_hs_type` case to
invoke `tc_infer_hs_type`, as prescribed in `Note [Future-proofing the type
checker]`.
There are some benign changes to test cases' expected output due to the new
code path using `forall a. [a]` as the kind of `'[]` rather than `[k]`.
Fixes #23543.
(cherry picked from commit c335fb7c44a8447b3e73e7f18d9d0dcb18cea8dd)
---
compiler/GHC/Tc/Gen/HsType.hs | 6 ++++++
testsuite/tests/ghci/scripts/T15898.stderr | 2 +-
testsuite/tests/ghci/scripts/T6018ghcifail.stderr | 8 ++++----
testsuite/tests/ghci/scripts/T7939.stdout | 8 ++++----
testsuite/tests/typecheck/should_compile/T23543.hs | 9 +++++++++
testsuite/tests/typecheck/should_compile/all.T | 1 +
testsuite/tests/typecheck/should_fail/T6018fail.stderr | 8 ++++----
7 files changed, 29 insertions(+), 13 deletions(-)
create mode 100644 testsuite/tests/typecheck/should_compile/T23543.hs
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 95646b0057b..d47fd2168bb 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1253,6 +1253,12 @@ tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
--------- Promoted lists and tuples
tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
+ -- The '[] case is handled in tc_infer_hs_type.
+ -- See Note [Future-proofing the type checker].
+ | null tys
+ = tc_infer_hs_type_ek mode rn_ty exp_kind
+
+ | otherwise
= do { tks <- mapM (tc_infer_lhs_type mode) tys
; (taus', kind) <- unifyKinds tys tks
; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
diff --git a/testsuite/tests/ghci/scripts/T15898.stderr b/testsuite/tests/ghci/scripts/T15898.stderr
index 4fd99bbccc0..97b98bc882a 100644
--- a/testsuite/tests/ghci/scripts/T15898.stderr
+++ b/testsuite/tests/ghci/scripts/T15898.stderr
@@ -18,7 +18,7 @@
In an equation for ‘it’: it = undefined :: [(), ()]
<interactive>:6:14: error: [GHC-83865]
- • Expected a type, but ‘'( '[], '[])’ has kind ‘([k0], [k1])’
+ • Expected a type, but ‘'( '[], '[])’ has kind ‘([a0], [a1])’
• In an expression type signature: '( '[], '[])
In the expression: undefined :: '( '[], '[])
In an equation for ‘it’: it = undefined :: '( '[], '[])
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index 36398cc89a0..ea1cd3f6df0 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -41,18 +41,18 @@
<interactive>:55:41: error: [GHC-05175]
Type family equation violates the family's injectivity annotation.
- Type/kind variable ‘k1’
+ Type/kind variable ‘a1’
cannot be inferred from the right-hand side.
In the type family equation:
- PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2
+ PolyKindVarsF @{[a1]} @[a2] ('[] @a1) = '[] @a2
-- Defined at <interactive>:55:41
<interactive>:60:15: error: [GHC-05175]
Type family equation violates the family's injectivity annotation.
- Type/kind variable ‘k1’
+ Type/kind variable ‘a1’
cannot be inferred from the right-hand side.
In the type family equation:
- PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
+ PolyKindVars @[a1] @[a2] ('[] @a1) = '[] @a2
-- Defined at <interactive>:60:15
<interactive>:64:15: error: [GHC-05175]
diff --git a/testsuite/tests/ghci/scripts/T7939.stdout b/testsuite/tests/ghci/scripts/T7939.stdout
index 6f0ab389487..83445adc242 100644
--- a/testsuite/tests/ghci/scripts/T7939.stdout
+++ b/testsuite/tests/ghci/scripts/T7939.stdout
@@ -19,12 +19,12 @@ type family H a where
H False = True
-- Defined at T7939.hs:15:1
H :: Bool -> Bool
-type J :: forall {k}. [k] -> Bool
-type family J a where
+type J :: forall {a}. [a] -> Bool
+type family J a1 where
J '[] = False
- forall k (h :: k) (t :: [k]). J (h : t) = True
+ forall a (h :: a) (t :: [a]). J (h : t) = True
-- Defined at T7939.hs:18:1
-J :: [k] -> Bool
+J :: [a] -> Bool
type K :: forall {a}. [a] -> Maybe a
type family K a1 where
K '[] = Nothing
diff --git a/testsuite/tests/typecheck/should_compile/T23543.hs b/testsuite/tests/typecheck/should_compile/T23543.hs
new file mode 100644
index 00000000000..1689d023287
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T23543.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T23543 where
+
+type N :: forall a. Maybe a
+type N = ('Nothing :: forall a. Maybe a)
+
+type L :: forall a. [a]
+type L = ('[] :: forall a. [a])
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 505a2f44adb..013f44971a4 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -875,6 +875,7 @@ test('T23171', normal, compile, [''])
test('T23192', normal, compile, [''])
test('T23199', normal, compile, [''])
test('T23156', normal, compile, [''])
+test('T23543', normal, compile, [''])
test('T22560a', normal, compile, [''])
test('T22560b', normal, compile, [''])
test('T22560c', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 0c352199e1f..27afca2b94d 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -52,18 +52,18 @@ T6018fail.hs:53:15: error: [GHC-05175]
T6018fail.hs:61:10: error: [GHC-05175]
Type family equation violates the family's injectivity annotation.
- Type/kind variable ‘k1’
+ Type/kind variable ‘a1’
cannot be inferred from the right-hand side.
In the type family equation:
- PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2
+ PolyKindVarsF @{[a1]} @[a2] ('[] @a1) = '[] @a2
-- Defined at T6018fail.hs:61:10
T6018fail.hs:64:15: error: [GHC-05175]
Type family equation violates the family's injectivity annotation.
- Type/kind variable ‘k1’
+ Type/kind variable ‘a1’
cannot be inferred from the right-hand side.
In the type family equation:
- PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
+ PolyKindVars @[a1] @[a2] ('[] @a1) = '[] @a2
-- Defined at T6018fail.hs:64:15
T6018fail.hs:68:15: error: [GHC-05175]
--
GitLab