[GHC] #14514: Higher-Rank Kinds work in ADT but not GADT

23 Nov 2017

      #14514: Higher-Rank Kinds work in ADT but not GADT
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14514
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler