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

Reverts 430f5c84dac1eab550110d543831a70516b5cac8

1 files changed, 25 insertions, 18 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~