#15545: Forced to enable TypeInType because of (i ~ i) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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 {{{#!hs 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15545 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler