Remove GADT self-reference check (#11554, #12081, #12174, fixes #15942)

Reverts 430f5c84dac1eab550110d543831a70516b5cac8

11 files changed, 68 insertions, 40 deletions

diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 8d4dbdb7fc..b37f36c735 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/dependent/should_fail/T12174.hs b/testsuite/tests/dependent/should_compile/T12174.hs
index 800759d690..800759d690 100644
--- a/testsuite/tests/dependent/should_fail/T12174.hs
+++ b/testsuite/tests/dependent/should_compile/T12174.hs
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index b89c1279cc..cf5c76d380 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/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, [''])
diff --git a/testsuite/tests/dependent/should_fail/T12081.stderr b/testsuite/tests/dependent/should_fail/T12081.stderr
index 77d5a40353..e8f25ba354 100644
--- a/testsuite/tests/dependent/should_fail/T12081.stderr
+++ b/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’
diff --git a/testsuite/tests/dependent/should_fail/T12174.stderr b/testsuite/tests/dependent/should_fail/T12174.stderr
deleted file mode 100644
index 868046137c..0000000000
--- a/testsuite/tests/dependent/should_fail/T12174.stderr
+++ /dev/null
@@ -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’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 38c7f45d55..af95d1b333 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/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, [''])
diff --git a/testsuite/tests/polykinds/T11554.hs b/testsuite/tests/polykinds/T11554.hs
index bca6b8277c..0f26bcf330 100644
--- a/testsuite/tests/polykinds/T11554.hs
+++ b/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
diff --git a/testsuite/tests/polykinds/T11554.stderr b/testsuite/tests/polykinds/T11554.stderr
deleted file mode 100644
index e3045c8366..0000000000
--- a/testsuite/tests/polykinds/T11554.stderr
+++ /dev/null
@@ -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’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 68bf260e64..1ff66e63ab 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/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, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T15942.hs b/testsuite/tests/typecheck/should_compile/T15942.hs
new file mode 100644
index 0000000000..60200466bf
--- /dev/null
+++ b/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))
+
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9e59160ccf..9e4e80dba8 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/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, [''])