Forced to enable TypeInType because of (i ~ i)
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 |