GitLab

The ticket below was posted because of confusion around higher-rank kinds. ticket:14514#comment:145571 suggests an error-message improvement, which I (goldfire) think is feasible.

---

Following code from Richard's 2016 Haskell Implementors' Workshop talk (/ Trees That Grow) works just fine

{-# 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.