Opened 5 months ago

Last modified 5 months ago

#13391 new bug

PolyKinds is more permissive in GHC 8

Reported by: crockeea Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.2
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The docs claim that the definition in section 9.11.10

data G (a :: k) where
  GInt   :: G Int
  GMaybe :: G Maybe

"requires that -XTypeInType be in effect", but this isn't the case.

The following compiles with GHC-8.0.2:

{-# LANGUAGE PolyKinds, GADTs #-}

data G (a :: k) where
  GInt   :: G Int
  GMaybe :: G Maybe

The example does *not* compile with 7.10.3, so this seems to be a case where -XPolyKinds has become more permissive in GHC 8 (as outlined in section 9.11.1).

Change History (5)

comment:1 Changed 5 months ago by RyanGlScott

Keywords: newcomer added

Good catch. I suspect fixing this wouldn't be too challenging. If you look at the commitdiff for 6746549772c5cc0ac66c0fce562f297f4d4b80a2 (Add kind equalities to GHC), searching for badGadtKindCon will give you the check that used to be in place for catching datatypes that are GADT-like in their kind arguments. Fixing this issue should hopefully be a matter of reinstating that check, but guarded behind a check for the presence of -XTypeInType.

comment:2 Changed 5 months ago by RyanGlScott

Keywords: TypeInType added

comment:3 Changed 5 months ago by goldfire

I don't think this is quite so easy. The old check needed to tell the difference between types and kinds. We can't do that anymore!

It is a shame that this happens though. If no one gets there first, I'll fix this in my TypeInType bug sweep this summer.

comment:4 in reply to:  3 Changed 5 months ago by RyanGlScott

Replying to goldfire:

I don't think this is quite so easy. The old check needed to tell the difference between types and kinds. We can't do that anymore!

Ah, good point. I'll remove the "newcomer" label so that we don't accidentally lead a new GHC contributor down a rabbit hole they can't climb back out of (something which has happened to me more times than I care to admit).

comment:5 Changed 5 months ago by RyanGlScott

Keywords: newcomer removed
Note: See TracTickets for help on using tickets.