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

[GHC]

#11498: GHC requires kind-polymorphic signatures on class head
-------------------------------------+-------------------------------------
           Reporter:  crockeea       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2-rc2
           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:
-------------------------------------+-------------------------------------
 I have the following compiling example:

 {{{
 {-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances,
 KindSignatures,
              MultiParamTypeClasses, PolyKinds, RankNTypes,
              ScopedTypeVariables, TypeFamilies, TypeOperators #-}

 import Data.Proxy
 import GHC.Prim

 type family CtxOf d (args :: k) :: Constraint

 class Run ctx (params :: [k]) where
   runAll :: Proxy params
             -> Proxy ctx
             -> (forall (args :: k) . (CtxOf ctx args) => Proxy args ->
 Bool)
             -> [Bool]

 data BasicCtxD
 type instance CtxOf BasicCtxD '(a,b) = (a ~ b)
 instance (Run BasicCtxD params, a ~ b)
   => Run BasicCtxD ( '(a,b) ': params) where
   runAll _ pctx f = (f (Proxy::Proxy '(a,b))) :
       (runAll (Proxy::Proxy params) pctx f)
 }}}

 But if I move the kind signature of `params` to its occurrence in the
 signature of `runAll`:
 {{{
 class Run ctx params where
   runAll :: Proxy (params :: [k])
             -> Proxy ctx
             -> (forall (args :: k) . (CtxOf ctx args) => Proxy args ->
 Bool)
             -> [Bool]
 }}}

 I get a couple of nasty (and confusing) compile errors.

 {{{
 Main.hs:20:25:
     Couldn't match kind ‘k1’ with ‘(,) k k’
       ‘k1’ is a rigid type variable bound by
            the type signature for
              runAll :: Proxy ('(a, b) : params)
                        -> Proxy BasicCtxD
                        -> (forall (args :: k1).
                            CtxOf BasicCtxD args =>
                            Proxy args -> Bool)
                        -> [Bool]
            at Main.hs:20:3
     Expected type: Proxy args0
       Actual type: Proxy '(a, b)
     Relevant bindings include
       f :: forall (args :: k1).
            CtxOf BasicCtxD args =>
            Proxy args -> Bool
         (bound at Main.hs:20:17)
       runAll :: Proxy ('(a, b) : params)
                 -> Proxy BasicCtxD
                 -> (forall (args :: k1).
                     CtxOf BasicCtxD args =>
                     Proxy args -> Bool)
                 -> [Bool]
         (bound at Main.hs:20:3)
     In the first argument of ‘f’, namely ‘(Proxy :: Proxy '(a, b))’
     In the first argument of ‘(:)’, namely
       ‘(f (Proxy :: Proxy '(a, b)))’
     In the expression:
       (f (Proxy :: Proxy '(a, b)))
       : (runAll (Proxy :: Proxy params) pctx f)

 Main.hs:21:42:
     Could not deduce (k1 ~ (,) k k)
     from the context (CtxOf BasicCtxD args)
       bound by a type expected by the context:
                  CtxOf BasicCtxD args => Proxy args -> Bool
       at Main.hs:21:8-42
       ‘k1’ is a rigid type variable bound by
            the type signature for
              runAll :: Proxy ('(a, b) : params)
                        -> Proxy BasicCtxD
                        -> (forall (args :: k1).
                            CtxOf BasicCtxD args =>
                            Proxy args -> Bool)
                        -> [Bool]
            at Main.hs:20:3
     Expected type: Proxy args -> Bool
       Actual type: Proxy args1 -> Bool
     Relevant bindings include
       f :: forall (args :: k1).
            CtxOf BasicCtxD args =>
            Proxy args -> Bool
         (bound at Main.hs:20:17)
       runAll :: Proxy ('(a, b) : params)
                 -> Proxy BasicCtxD
                 -> (forall (args :: k1).
                     CtxOf BasicCtxD args =>
                     Proxy args -> Bool)
                 -> [Bool]
         (bound at Main.hs:20:3)
     In the third argument of ‘runAll’, namely ‘f’
     In the second argument of ‘(:)’, namely
       ‘(runAll (Proxy :: Proxy params) pctx f)’
 }}}
 It seems to me that the two definitions of the class are equivalent, so it
 would be nice if they both compiled. It wasn't obvious to me that the kind
 signature had to go on the class parameter rather than somewhere else.

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