Trac #11554 fix loopy GADTs

Summary: Fixes T11554

Reviewers: goldfire, thomie, simonpj, austin, bgamari

Reviewed By: thomie, simonpj, bgamari

Subscribers: simonpj, goldfire, thomie

Differential Revision: https://phabricator.haskell.org/D2283

GHC Trac Issues: #11554

5 files changed, 43 insertions, 8 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 524e0b69cb..2d029b2fdc 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -907,7 +907,11 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
        ; case thing of
            ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
 
-           ATcTyCon tc_tc -> do { check_tc tc_tc
+           ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference]
+                                  unless
+                                    (isTypeLevel (mode_level mode))
+                                    (promotionErr name TyConPE)
+                                ; check_tc tc_tc
                                 ; tc <- get_loopy_tc name tc_tc
                                 ; handle_tyfams tc tc_tc }
                              -- mkNakedTyConApp: see Note [Type-checking inside the knot]
@@ -1029,6 +1033,26 @@ look at the TyCon or Class involved.
 This is horribly delicate.  I hate it.  A good example of how
 delicate it is can be seen in Trac #7903.
 
+Note [GADT kind self-reference]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A promoted type cannot be used in the body of that type's declaration.
+Trac #11554 shows this example, which made GHC loop:
+
+  import Data.Kind
+  data P (x :: k) = Q
+  data A :: Type where
+    B :: forall (a :: A). P a -> A
+
+In order to check the constructor B, we need 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.
+
+Trac #11962 proposes checking the head of a data declaration separately from
+its constructors. This would allow the example above to pass.
+
 Note [Body kind of a HsForAllTy]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The body of a forall is usually a type, but in principle
diff --git a/docs/users_guide/bugs.rst b/docs/users_guide/bugs.rst
index ff8372589e..5b710aa35d 100644
--- a/docs/users_guide/bugs.rst
+++ b/docs/users_guide/bugs.rst
@@ -479,13 +479,6 @@ Bugs in GHC
    in the compiler's internal representation and can be unified producing
    unexpected results. See :ghc-ticket:`11715` for one example.
 
--  :ghc-flag:`-XTypeInType` still has a few rough edges, especially where
-   it interacts with other advanced type-system features. For instance,
-   this definition causes the typechecker to loop (:ghc-ticket:`11559`), ::
-
-     data A :: Type where
-       B :: forall (a :: A). A
-
 .. _bugs-ghci:
 
 Bugs in GHCi (the interactive GHC)
diff --git a/testsuite/tests/polykinds/T11554.hs b/testsuite/tests/polykinds/T11554.hs
new file mode 100644
index 0000000000..e7a35bd9d8
--- /dev/null
+++ b/testsuite/tests/polykinds/T11554.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE GADTs, TypeInType, RankNTypes #-}
+
+module T11554 where
+
+import Data.Kind
+
+data P (x :: k) = Q
+
+data A :: Type where
+  B :: forall (a :: A). P a -> A
diff --git a/testsuite/tests/polykinds/T11554.stderr b/testsuite/tests/polykinds/T11554.stderr
new file mode 100644
index 0000000000..e3045c8366
--- /dev/null
+++ b/testsuite/tests/polykinds/T11554.stderr
@@ -0,0 +1,7 @@
+
+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 bcc8dc4f81..1c27dfd82e 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -148,5 +148,6 @@ test('T11648b', normal, compile_fail, [''])
 test('KindVType', normal, compile_fail, [''])
 test('T11821', normal, compile, [''])
 test('T11640', normal, compile, [''])
+test('T11554', normal, compile_fail, [''])
 test('T12055', normal, compile, [''])
 test('T12055a', normal, compile_fail, [''])