Re: [GHC] #11498: GHC requires kind-polymorphic signatures on class head

26 May 2018

      #11498: GHC requires kind-polymorphic signatures on class head
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.2-rc2
  checker)                           |
      Resolution:                    |             Keywords:
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 RyanGlScott):

 This is rather strange. Here is a slightly more compact example:

 {{{#!hs
 {-# LANGUAGE PolyKinds #-}
 module Prog1 where

 import Data.Proxy

 class C (a :: k) where
   c :: Proxy a -> Proxy (b :: k)
 }}}

 Let's see what GHCi thinks the type of `c` is:

 {{{
 λ> :i C
 class C (a :: k) where
   c :: forall (b :: k). Proxy a -> Proxy b
 }}}

 So far, so good. But if you move the kind signature:

 {{{#!hs
 {-# LANGUAGE PolyKinds #-}
 module Prog2 where

 import Data.Proxy

 class C a where
   c :: Proxy (a :: k) -> Proxy (b :: k)
 }}}

 Then the type changes!

 {{{
 λ> :i C
 class C (a :: k) where
   c :: forall k1 (b :: k1). Proxy a -> Proxy b
 }}}

 All of a sudden, the kinds of `a` and `b` have become entirely different.

 To add to the strangeness, `Prog2` doesn't compile at all on GHC HEAD:

 {{{
 $ /opt/ghc/head/bin/ghci Prog2.hs
 GHCi, version 8.5.20180501: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Prog2            ( Prog2.hs, interpreted )

 Prog2.hs:7:15: error:
     • Expected kind ‘k’, but ‘a’ has kind ‘k0’
     • In the first argument of ‘Proxy’, namely ‘(a :: k)’
       In the type signature: c :: Proxy (a :: k) -> Proxy (b :: k)
       In the class declaration for ‘C’
   |
 7 |   c :: Proxy (a :: k) -> Proxy (b :: k)
   |               ^
 }}}

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