Opened 4 years ago

Closed 2 years ago

Last modified 2 years ago

#11963 closed bug (fixed)

GHC introduces kind equality without TypeInType

Reported by: ezyang Owned by: johnleo
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.0.1-rc2
Keywords: TypeInType Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T11963
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


The following program is accepted by GHC 8.0 rc2

{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
data Typ k t  where
    Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t

This probably shouldn't be accepted, because this is a circuitous way of saying:

{-# LANGUAGE TypeInType #-}
data Typ k (t :: k) = Typ

which does not work without TypeInType. Or perhaps both should be accepted without TypeInType?

Printing with explicit kinds makes it clear why the obvious check didn't fire:

ezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds
GHCi, version  :? for help
[1 of 1] Compiling Main             ( B.hs, interpreted )
Ok, modules loaded: Main.
*Main> :info Typ
type role Typ nominal nominal nominal
data Typ k k1 (t :: k) where
  Typ :: forall k (t :: k).
         (forall (a :: k -> *). a t -> a t) -> Typ k k t
  	-- Defined at B.hs:2:1

Change History (8)

comment:1 Changed 4 years ago by goldfire

Keywords: TypeInType added

As it says in the user's guide, identifying the necessity for -XTypeInType is done on a best-effort basis. That said, I'm surprised this one is missed, because k is clearly used as both a kind and a type in the type of the data constructor.

comment:2 Changed 4 years ago by RyanGlScott

Cc: RyanGlScott added

comment:3 Changed 3 years ago by johnleo

Owner: changed from goldfire to johnleo

comment:4 Changed 2 years ago by Richard Eisenberg <rae@…>

In 10d13b6/ghc:

Fix #11963 by checking for more mixed type/kinds

This is a straightforward fix -- there were just some omitted

test case: typecheck/should_fail/T11963

comment:5 Changed 2 years ago by goldfire

Milestone: 8.2.2
Status: newmerge
Test Case: typecheck/should_fail/T11963

This seems easy enough to merge, but it's far from critical.

comment:6 Changed 2 years ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:7 Changed 2 years ago by bgamari

Reverted from ghc-8.2 in 5e2d3e6d06a051dd30c0ce1919cd2d3d0ece087b as it causes a few programs from Hackage to be rejected, which we'd like to avoid in a point release.

comment:8 Changed 2 years ago by bgamari

Note: See TracTickets for help on using tickets.