[GHC] #14514: Error messages: suggest annotating with higher-rank kind (was: Higher-Rank Kinds work in ADT but not GADT)

[GHC]

#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/2e21a6be4419873c77a02c9a198379c76947b94c/extensibility/Extensible6.hs
> 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/2e21a6be4419873c77a02c9a198379c76947b94c/extensibility/Extensible6.hs
 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