[GHC] #13399: Location of `forall` matters with higher-rank kind polymorphism

[GHC]

#13399: Location of `forall` matters with higher-rank kind polymorphism
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.2
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by crockeea):

 **Use case:**

 I'm working on a HOAS for a [http://okmij.org/ftp/tagless-final/ tagless
 final] DSL. That approach uses GADTs for "interpreters" of various
 languages (classes). The class `C` in my example comes from the language
 for lambda abstractions in our depth-indexed language. Namely,

 {{{
 class LambdaD (expr :: forall k . k -> * -> *) where
   lamD :: (expr da a -> expr db b) -> expr '(da,db) (a -> b)
   appD :: expr '(da,db) (a -> b) -> expr da a -> expr db b
 }}}

 where `expr` is one of the GADT interpreters. We need to remember the
 depth of the input and output of the function, so we change the ''kind''
 of the "depth" to a pair.

 **Back to this ticket:**

 However, I just realized you don't actually need higher-rank polymorphism
 to see this bug. You can do the following in GHCi:

 {{{
 > :set -XTypeInType
 > :set -XRankNTypes
 > :set -fprint-explicit-foralls
 > data Bar :: forall k. (* -> *) -> k -> *
 > :kind! Bar
 Bar :: forall k. (* -> *) -> k -> *              -- precisely what I
 wrote, no surprise here
 > :kind! (Bar Maybe :: forall k. k -> *)
 <interactive>:1:2: error:
   • Expected kind ‘forall k. k -> *’,
       but ‘Bar Maybe’ has kind ‘k0 -> *’
   • In the type ‘(Bar Maybe :: forall k. k -> *)’
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13399#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler