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

8 Mar 2017

      #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
           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:
-------------------------------------+-------------------------------------
 The following code fails to compile, but probably should:

 {{{
 {-# LANGUAGE RankNTypes, TypeInType #-}

 import Data.Kind

 data Foo :: forall k . (* -> *) -> k -> * -- Decl 1

 class C (a :: forall k . k -> *)

 instance C (Foo a) -- error on this line
 }}}

 with the error

 {{{
 • Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’
 • In the first argument of ‘C’, namely ‘Foo a’
   In the instance declaration for ‘C (Foo a)’
 }}}

 Similarly, the following declarations of `Foo` also cause a similar error
 at the instance declaration:

 Decl 2: `data Foo :: (* -> *) -> k -> *`

 Decl 3: `data Foo (a :: * -> *) (b :: k)`

 However, if I move the `forall` to a point ''after'' the first type
 parameter (which is where the instance is partially applied) thusly:

 Decl 4: `data Foo :: (* -> *) -> forall k . k -> *`

 then GHC happily accepts the instance of `C`.

 From my (admittedly negligible) knowledge of type theory, the signatures
 for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated
 to the front of Decl 4. GHC should accept any of the four versions of
 `Foo`, since they are all equivalent.

 As a side note, I was surprised to discover that the syntax for Decl 4 is
 even allowed. What is the point of allowing a "global"/rank-1 forall
 anywhere but at the left edge of the signature (other than as a convenient
 workaround for this bug)?

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