[Git][ghc/ghc][wip/ghc-9.8] Fix typechecking of promoted empty lists
Ben Gamari (@bgamari)
gitlab at gitlab.haskell.org
Thu Jul 20 19:26:16 UTC 2023
Ben Gamari pushed to branch wip/ghc-9.8 at Glasgow Haskell Compiler / GHC
Commits:
6e044db1 by Ryan Scott at 2023-07-20T15:24:43-04:00
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)
- - - - -
7 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- testsuite/tests/ghci/scripts/T15898.stderr
- testsuite/tests/ghci/scripts/T6018ghcifail.stderr
- testsuite/tests/ghci/scripts/T7939.stdout
- + testsuite/tests/typecheck/should_compile/T23543.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T6018fail.stderr
Changes:
=====================================
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')
=====================================
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 :: '( '[], '[])
=====================================
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]
=====================================
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
=====================================
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])
=====================================
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, [''])
=====================================
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]
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6e044db19db65f824837bfdc15ba3def0315b6e4
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6e044db19db65f824837bfdc15ba3def0315b6e4
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230720/4d43fb65/attachment-0001.html>
More information about the ghc-commits
mailing list