[Git][ghc/ghc][wip/T23543] Fix typechecking of promoted empty lists
Ryan Scott (@RyanGlScott)
gitlab at gitlab.haskell.org
Sun Jun 25 21:55:14 UTC 2023
Ryan Scott pushed to branch wip/T23543 at Glasgow Haskell Compiler / GHC
Commits:
005f5d34 by Ryan Scott at 2023-06-25T17:54:52-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.
- - - - -
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
=====================================
@@ -1003,6 +1003,13 @@ But, we want to make sure that our pattern-matches are complete. So,
we have a bunch of repetitive code just so that we get warnings if we're
missing any patterns.
+Note particularly (c.f. #23543):
+
+* `HsExplicitListTy` with an empty argument list is handled by
+ `tc_infer_hs_type`, because it can have a polymorphic kind
+ `forall k. k -> [k]`.
+* `HsExplicitListTy` with a non-empty argument list is handled by `tc_hs_type`,
+ because it can only have a monomorphic kind.
-}
------------------------------------------
@@ -1075,6 +1082,7 @@ tc_infer_hs_type _ (XHsType ty)
tc_infer_hs_type _ (HsExplicitListTy _ _ tys)
| null tys -- this is so that we can use visible kind application with '[]
-- e.g ... '[] @Bool
+ -- See Note [Future-proofing the type checker]
= return (mkTyConTy promotedNilDataCon,
mkSpecForAllTys [alphaTyVar] $ mkListTy alphaTy)
@@ -1253,6 +1261,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
=====================================
@@ -880,3 +880,4 @@ test('T22560b', normal, compile, [''])
test('T22560c', normal, compile, [''])
test('T22560d', extra_files(['T22560d.hs']), ghci_script, ['T22560d.script'])
test('T22560e', normal, compile, [''])
+test('T23543', 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/005f5d348d60413541c078ca2932f3d7d8e2b9de
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/005f5d348d60413541c078ca2932f3d7d8e2b9de
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/20230625/2e48d6e6/attachment-0001.html>
More information about the ghc-commits
mailing list