#14514: Higher-Rank Kinds work in ADT but not GADT -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: Replying to [comment:1 Iceland_jack]:

Please close is that is the case

You got it. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14514#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14514: Error messages: suggest annotating with higher-rank kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: invalid | Keywords: TypeInType, | TypeErrorMessages Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: => TypeInType, TypeErrorMessages Old description:

Following code from [https://github.com/goldfirere/triptych/blob/2e21a6be4419873c77a02c9a198379c7... Richard's 2016 Haskell Implementors' Workshop talk] (/ [https://arxiv.org/abs/1610.04799 Trees That Grow]) works just fine

{{{#!hs {-# Language RankNTypes, KindSignatures, DataKinds, TypeFamilyDependencies, TypeInType #-}

import Data.Kind

data TagTag = ETagTag | PTagTag data ETag = VarTag data PTag = VarPTag

type family Tag (ttag::TagTag) = (res :: Type) | res -> ttag where Tag ETagTag = ETag Tag PTagTag = PTag

type WithAnyTag = forall tag. Tag tag -> Type

-- data Exp (ext::WithAnyTag) where -- Var :: ext VarTag -> Exp ext data Exp (ext::WithAnyTag) = Var (ext VarTag) }}}

but replace `data Exp` with its commented-out GADT brethren and it stops working

{{{ $ ghci -ignore-dot-ghci Weird.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( Weird.hs, interpreted )

Weird.hs:17:28: error: • Expected kind ‘WithAnyTag’, but ‘ext1’ has kind ‘ETag -> *’ • In the first argument of ‘Exp’, namely ‘ext’ In the type ‘Exp ext’ In the definition of data constructor ‘Var’ | 17 | Var :: ext VarTag -> Exp ext | ^^^ Failed, 0 modules loaded. Prelude> }}}

The type synonym can be inlined, makes no difference.

New description: The ticket below was posted because of confusion around higher-rank kinds. comment:3 suggests an error-message improvement, which I (goldfire) think is feasible. ------------------------------------ Following code from [https://github.com/goldfirere/triptych/blob/2e21a6be4419873c77a02c9a198379c7... Richard's 2016 Haskell Implementors' Workshop talk] (/ [https://arxiv.org/abs/1610.04799 Trees That Grow]) works just fine {{{#!hs {-# Language RankNTypes, KindSignatures, DataKinds, TypeFamilyDependencies, TypeInType #-} import Data.Kind data TagTag = ETagTag | PTagTag data ETag = VarTag data PTag = VarPTag type family Tag (ttag::TagTag) = (res :: Type) | res -> ttag where Tag ETagTag = ETag Tag PTagTag = PTag type WithAnyTag = forall tag. Tag tag -> Type -- data Exp (ext::WithAnyTag) where -- Var :: ext VarTag -> Exp ext data Exp (ext::WithAnyTag) = Var (ext VarTag) }}} but replace `data Exp` with its commented-out GADT brethren and it stops working {{{ $ ghci -ignore-dot-ghci Weird.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( Weird.hs, interpreted ) Weird.hs:17:28: error: • Expected kind ‘WithAnyTag’, but ‘ext1’ has kind ‘ETag -> *’ • In the first argument of ‘Exp’, namely ‘ext’ In the type ‘Exp ext’ In the definition of data constructor ‘Var’ | 17 | Var :: ext VarTag -> Exp ext | ^^^ Failed, 0 modules loaded. Prelude> }}} The type synonym can be inlined, makes no difference. -- Comment: Yes, I suppose that wouldn't be too hard. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14514#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler