Commit 430f5c84 authored by Alexander Vieth's avatar Alexander Vieth Committed by Ben Gamari

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:

GHC Trac Issues: #11554
parent 0701db12
......@@ -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]
(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
......@@ -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)
{-# 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
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’
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment