Opened 4 months ago

Closed 4 months ago

Last modified 4 months ago

#15545 closed bug (fixed)

Forced to enable TypeInType because of (i ~ i)

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.5
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #15195 Differential Rev(s):
Wiki Page:

Description

I don't know if this is a bug but i ~ i holds by reflexivity so I would not have expected it to require TypeInType

$ ghci -ignore-dot-ghci
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XPolyKinds -XGADTs
Prelude> import Data.Kind
Prelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a

<interactive>:3:45: error:
    • Data constructor ‘NP’ constrains the choice of kind parameter:
        i ~ i
      Use TypeInType to allow this
    • In the definition of data constructor ‘NP’
      In the data type declaration for ‘NP’
Prelude Data.Kind> 

I would rather expect the warning I get after enabling TypeInType

Prelude Data.Kind> :set -XTypeInType
Prelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a

<interactive>:8:28: error:
    • Couldn't match ‘k’ with ‘i’
    • In the data declaration for ‘NP’

ps making sure this is OK as well; it works after enabling -XTypeInType and quantifying with -XRankNTypes (is this using polymorphic recursion?)

Prelude Data.Kind> :set -XTypeInType -XRankNTypes
Prelude Data.Kind> data NP :: forall i k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
Prelude Data.Kind> :t NP
NP :: forall i (f :: i -> *) (a :: i). f a -> NP f a

it also works for

data NP :: forall k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
data NP :: forall i. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
data NP :: (k -> Type) -> forall i. (i -> Type) where NP :: f a -> NP f a

Change History (2)

comment:1 Changed 4 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: newclosed

This is a rather cheeky solution, but this problem simply doesn't exist on GHC 8.6, since TypeInType is now simply a synonym for DataKinds and PolyKinds, and PolyKinds now grants access to all of the features that used to be exclusive to TypeInType. See #15195.

comment:2 Changed 4 months ago by Iceland_jack

That is cheeky indeed :) cheers Ryan

Note: See TracTickets for help on using tickets.