GitLab

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

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture