Opened 7 months ago

Last modified 5 days ago

#13391 patch 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): Phab:D3859
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 (8)

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

Keywords: TypeInType added

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

Keywords: newcomer removed

comment:6 Changed 6 weeks ago by goldfire

Differential Rev(s): Phab:D3859
Status: newpatch

comment:7 Changed 9 days ago by bgamari

One non-obvious implication of this change is that program like the KindEqualities test from the testsuite will now require that users enable TypeInType and consequently will manually need to quantify over the kind variables of their tycon's signature. For instance, currently KindEqualities has,

data TyRep :: k -> * where
  TyInt :: TyRep Int
  -- etc.

This needs to become,

data TyRep :: forall k. k -> * where
  TyInt :: TyRep Int
  -- etc.

This is documented in Phab:D3966.

comment:8 Changed 5 days ago by Ben Gamari <ben@…>

In bbb8cb92/ghc:

users-guide: Mention changes necessary due to #13391

Some variant of this should also be added to the migration guide.

[skip ci]

Test Plan: Read it

Reviewers: goldfire, austin

Reviewed By: goldfire

Subscribers: rwbarton, thomie

GHC Trac Issues: #13391

Differential Revision: https://phabricator.haskell.org/D3966
Note: See TracTickets for help on using tickets.