Opened 15 months ago

Last modified 11 months ago

#11963 new bug

GHC introduces kind equality without TypeInType

Reported by: ezyang Owned by: johnleo
Priority: normal Milestone:
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:
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 (3)

comment:1 Changed 15 months 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 15 months ago by RyanGlScott

Cc: RyanGlScott added

comment:3 Changed 11 months ago by johnleo

Owner: changed from goldfire to johnleo
Note: See TracTickets for help on using tickets.