[Git][ghc/ghc][master] Remove GADT self-reference check (#11554, #12081, #12174, fixes #15942)
Marge Bot
gitlab at gitlab.haskell.org
Sat Sep 19 19:52:31 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
760307cf by Artyom Kuznetsov at 2020-09-19T15:52:21-04:00
Remove GADT self-reference check (#11554, #12081, #12174, fixes #15942)
Reverts 430f5c84dac1eab550110d543831a70516b5cac8
- - - - -
11 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- testsuite/tests/dependent/should_fail/T12174.hs → testsuite/tests/dependent/should_compile/T12174.hs
- testsuite/tests/dependent/should_compile/all.T
- testsuite/tests/dependent/should_fail/T12081.stderr
- − testsuite/tests/dependent/should_fail/T12174.stderr
- testsuite/tests/dependent/should_fail/all.T
- testsuite/tests/polykinds/T11554.hs
- − testsuite/tests/polykinds/T11554.stderr
- testsuite/tests/polykinds/all.T
- + testsuite/tests/typecheck/should_compile/T15942.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1798,11 +1798,9 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
; case thing of
ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
+ -- See Note [Recursion through the kinds]
ATcTyCon tc_tc
- -> do { -- See Note [GADT kind self-reference]
- unless (isTypeLevel (mode_tyki mode))
- (promotionErr name TyConPE)
- ; check_tc tc_tc
+ -> do { check_tc tc_tc
; return (mkTyConTy tc_tc, tyConKind tc_tc) }
AGlobal (ATyCon tc)
@@ -1843,25 +1841,34 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
dc_theta_illegal_constraint = find (not . isEqPred)
{-
-Note [GADT kind self-reference]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-A promoted type cannot be used in the body of that type's declaration.
-#11554 shows this example, which made GHC loop:
+Note [Recursion through the kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider these examples
- import Data.Kind
+#11554:
data P (x :: k) = Q
data A :: Type where
- B :: forall (a :: A). P a -> A
+ MkA :: forall (a :: A). P a -> A
+
+#12174
+ data V a
+ data T = forall (a :: T). MkT (V a)
+
+The type is recursive (which is fine) but it is recursive /through the
+kinds/. In earlier versions of GHC this caused a loop in the compiler
+(to do with knot-tying) but there is nothing fundamentally wrong with
+the code (kinds are types, and the recursive declarations are OK). But
+it's hard to distinguish "recursion through the kinds" from "recursion
+through the types". Consider this (also #11554):
+
+ data PB k (x :: k) = Q
+ data B :: Type where
+ MkB :: P B a -> B
-In order to check the constructor B, we need to have the promoted type A, but in
-order to get that promoted type, B must first be checked. To prevent looping, a
-TyConPE promotion error is given when tcTyVar checks an ATcTyCon in kind mode.
-Any ATcTyCon is a TyCon being defined in the current recursive group (see data
-type decl for TcTyThing), and all such TyCons are illegal in kinds.
+Here the occurrence of B is not obviously in a kind position.
-#11962 proposes checking the head of a data declaration separately from
-its constructors. This would allow the example above to pass.
+So now GHC allows all these programs. #12081 and #15942 are other
+examples.
Note [Body kind of a HsForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
testsuite/tests/dependent/should_fail/T12174.hs → testsuite/tests/dependent/should_compile/T12174.hs
=====================================
=====================================
testsuite/tests/dependent/should_compile/all.T
=====================================
@@ -67,3 +67,4 @@ test('T16391a', normal, compile, [''])
test('T16344b', normal, compile, [''])
test('T16347', normal, compile, [''])
test('T18660', normal, compile, [''])
+test('T12174', normal, compile, [''])
=====================================
testsuite/tests/dependent/should_fail/T12081.stderr
=====================================
@@ -1,7 +1,6 @@
T12081.hs:9:14: error:
- • Type constructor ‘T’ cannot be used here
- (it is defined and used in the same recursive group)
+ • Expected a type, but ‘T n’ has kind ‘Nat’
• In the kind ‘T n’
In the type signature: f :: (a :: T n)
In the class declaration for ‘C’
=====================================
testsuite/tests/dependent/should_fail/T12174.stderr deleted
=====================================
@@ -1,7 +0,0 @@
-
-T12174.hs:9:23: error:
- • Type constructor ‘T’ cannot be used here
- (it is defined and used in the same recursive group)
- • In the kind ‘T’
- In the definition of data constructor ‘MkS’
- In the data declaration for ‘S’
=====================================
testsuite/tests/dependent/should_fail/all.T
=====================================
@@ -13,7 +13,6 @@ test('T11407', normal, compile_fail, [''])
test('T11334b', normal, compile_fail, [''])
test('T11473', normal, compile_fail, [''])
test('T11471', normal, compile_fail, [''])
-test('T12174', normal, compile_fail, [''])
test('T12081', normal, compile_fail, [''])
test('T13135', normal, compile_fail, [''])
test('T13601', normal, compile_fail, [''])
=====================================
testsuite/tests/polykinds/T11554.hs
=====================================
@@ -1,10 +1,17 @@
-{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
+{-# LANGUAGE GADTs, PolyKinds, RankNTypes, TypeApplications, DataKinds #-}
module T11554 where
import Data.Kind
-data P (x :: k) = Q
+data P1 (x :: k) = Q1
+data A1 :: Type where
+ B1 :: forall (a :: A1). P1 a -> A1
-data A :: Type where
- B :: forall (a :: A). P a -> A
+data P2 k (x :: k) = Q2
+data A2 :: Type where
+ B2 :: P2 A2 a -> A2
+
+data P3 (x :: k) = Q3
+data A3 :: Type where
+ B3 :: P3 @A3 a -> A3
=====================================
testsuite/tests/polykinds/T11554.stderr deleted
=====================================
@@ -1,7 +0,0 @@
-
-T11554.hs:10:21: error:
- • Type constructor ‘A’ cannot be used here
- (it is defined and used in the same recursive group)
- • In the kind ‘A’
- In the definition of data constructor ‘B’
- In the data declaration for ‘A’
=====================================
testsuite/tests/polykinds/all.T
=====================================
@@ -148,7 +148,7 @@ test('KindVType', normal, compile_fail, [''])
test('T11821', normal, compile, [''])
test('T11821a', normal, compile_fail, [''])
test('T11640', normal, compile, [''])
-test('T11554', normal, compile_fail, [''])
+test('T11554', normal, compile, [''])
test('T12055', normal, compile, [''])
test('T12055a', normal, compile_fail, [''])
test('T12593', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_compile/T15942.hs
=====================================
@@ -0,0 +1,28 @@
+{-# Language DataKinds #-}
+{-# Language RankNTypes #-}
+{-# Language TypeApplications #-}
+{-# Language PolyKinds #-}
+{-# Language KindSignatures #-}
+{-# Language TypeFamilies #-}
+{-# Language AllowAmbiguousTypes #-}
+module T15942 where
+
+import Data.Kind
+import Data.Proxy
+
+type G1 = forall (b :: Bool). Type
+
+data Fun1 :: G1
+
+class F1 (bool :: Bool) where
+ type Not1 bool :: Bool
+ foo1 :: Fun1 @(Not1 bool)
+
+type G2 = Bool -> Type
+
+data Fun2 :: G2
+
+class F2 (bool :: Bool) where
+ type Not2 bool :: Bool
+ foo2 :: Proxy (x :: Proxy (Not2 bool))
+
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -722,4 +722,5 @@ test('T18412', normal, compile, [''])
test('T18470', normal, compile, [''])
test('T18323', normal, compile, [''])
test('T18585', normal, compile, [''])
+test('T15942', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/760307cf5511d970dfddf7fa4b502b4e3394b197
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/760307cf5511d970dfddf7fa4b502b4e3394b197
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/20200919/f1a50e3a/attachment-0001.html>
More information about the ghc-commits
mailing list