[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:  closed
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler          |              Version:  8.0.2
      Resolution:  fixed             |             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):  Phab:D3860
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by bgamari):

 * status:  patch => closed
 * resolution:   => fixed
 * milestone:   => 8.4.1


Old description:

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

New description:

 The following code fails to compile, but probably should:

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

--

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