Trac #11554 fix loopy GADTs
authorAlexander Vieth <alexander.vieth@mail.mcgill.ca>
Mon, 20 Jun 2016 07:22:18 +0000 (09:22 +0200)
committerBen Gamari <ben@smart-cactus.org>
Mon, 25 Jul 2016 15:06:05 +0000 (17:06 +0200)
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

(cherry picked from commit 430f5c84dac1eab550110d543831a70516b5cac8)

compiler/typecheck/TcHsType.hs
docs/users_guide/bugs.rst
testsuite/tests/polykinds/T11554.hs [new file with mode: 0644]
testsuite/tests/polykinds/T11554.stderr [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index c533399..ea6a292 100644 (file)
@@ -881,7 +881,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]
@@ -1003,6 +1007,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
index c4ac9ce..a1ec885 100644 (file)
@@ -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
-
 -  There is known to be maleficent interactions between weak references and
    laziness. Particularly, it has been observed that placing a thunk containing
    a reference to a weak reference inside of another weak reference may cause
diff --git a/testsuite/tests/polykinds/T11554.hs b/testsuite/tests/polykinds/T11554.hs
new file mode 100644 (file)
index 0000000..e7a35bd
--- /dev/null
@@ -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 (file)
index 0000000..e3045c8
--- /dev/null
@@ -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’
index 522ae43..b2e1c7b 100644 (file)
@@ -145,3 +145,4 @@ test('T11611', normal, compile_fail, [''])
 test('T11648', normal, compile, [''])
 test('T11648b', normal, compile_fail, [''])
 test('KindVType', normal, compile_fail, [''])
+test('T11554', normal, compile_fail, [''])