[Git][ghc/ghc][master] Fix typechecking of promoted empty lists

[Marge Bot (@marge-bot)]

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
c335fb7c by Ryan Scott at 2023-06-28T21:10:44-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
=====================================
@@ -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/c335fb7c44a8447b3e73e7f18d9d0dcb18cea8dd

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c335fb7c44a8447b3e73e7f18d9d0dcb18cea8dd
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/20230628/cf88a891/attachment-0001.html>