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

[GHC]

#13399: Location of `forall` matters with 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:                    |
-------------------------------------+-------------------------------------
Description changed by crockeea:

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

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

--

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