#11554 closed bug (fixed)

Self quantification in GADT data declarations

Reported by: Rafbill Owned by:
Priority: high Milestone: 8.0.2
Component: Compiler (Type checker) Version: 8.0.1-rc2
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

GHC hangs on this (it was panicking on the same code before : https://github.com/goldfirere/ghc/issues/56(https://github.com/goldfirere/ghc/issues/56) :

{-# LANGUAGE GADTs, TypeInType #-}
import Data.Kind
data A :: Type where
  B :: forall (a :: A). A

I guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.

Change History (14)

comment:1 Changed 22 months ago by bgamari

Component: CompilerCompiler (Type checker)
Keywords: TypeInType added
Milestone: 8.0.1
Priority: normalhigh
Type of failure: None/UnknownCompile-time crash

comment:2 Changed 20 months ago by bgamari

Cc: goldfire added

comment:3 Changed 20 months ago by bgamari

We're going to just mention this in the user's guide for now.

Last edited 20 months ago by bgamari (previous) (diff)

comment:4 Changed 20 months ago by Ben Gamari <ben@…>

In aa61174/ghc:

users-guide: Add references to various issues in bugs section

Test Plan: Read it

Reviewers: austin

Reviewed By: austin

Subscribers: thomie

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

GHC Trac Issues: #7411, #11197, #11554, #11715

comment:5 Changed 20 months ago by bgamari

Milestone: 8.0.18.0.2

comment:6 Changed 18 months ago by carlostome

This bug seems to be solved in ghc version 8.1.20160519 (commit 296b8f1baef2e6c88a418bbc5ac8b1ced111c745).

comment:7 Changed 18 months ago by Rafbill

The bug is still present in this slightly modified example :

{-# LANGUAGE GADTs, TypeInType, RankNTypes #-}
import Data.Kind
data P (x :: k) = Q
data A :: Type where
  B :: forall (a :: A). P a -> A

comment:8 Changed 18 months ago by alexvieth

I have a patch which will reject the example in comment:7 and give this 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’

The details:

  • ATcTyThing has a new variant ATcTyConUnpromoted TyCon meaning the TyCon can't be used as a kind.
  • tcTyVar will give a promotion error (TyConPE) whenever an ATcTyConUnpromoted is encountered and the TcTyMode is kind level.
  • When checking the constructors of a DataDecl, the name of the type is associated with an ATcTyConUnpromoted, rather than ATcTyCon as it is now.

Think this is a sane thing to do? If so I'll upload it to phab.

comment:9 Changed 18 months ago by goldfire

Won't ATcTyConUnpromoted and ATcTyCon be the same, always? That is, if (and only if) we're currently checking a mutually recursive group containing the tycon T, T will be registered as ATcTyCon. Isn't that the exact scenario where you're proposing to use ATcTyConUnpromoted? So my take would be to check in tcTyVar, just as you suggest, but use the existing ATcTyCon instead of creating something new.

Or what am I missing?

comment:10 Changed 18 months ago by alexvieth

Or what am I missing?

Nothing, you're right about this. The patch is now very small.

--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -881,7 +881,10 @@ 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 { 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]

comment:11 Changed 18 months ago by goldfire

I like it! :)

comment:12 Changed 17 months ago by Ben Gamari <ben@…>

In 430f5c8/ghc:

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

comment:13 Changed 17 months ago by bgamari

Status: newmerge

comment:14 Changed 17 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.