[GHC] #10039: Make Const (Control.Applicative) kind polymorphic in its second argument

28 Jan 2015

      #10039: Make Const (Control.Applicative) kind polymorphic in its second argument
-------------------------------------+-------------------------------------
              Reporter:              |             Owner:
  Iceland_jack                       |            Status:  new
                  Type:  feature     |         Milestone:
  request                            |           Version:  7.8.4
              Priority:  normal      |  Operating System:  Unknown/Multiple
             Component:              |   Type of failure:  None/Unknown
  libraries/base                     |        Blocked By:
              Keywords:              |   Related Tickets:
          Architecture:              |
  Unknown/Multiple                   |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Is there any reason why `Const` isn't kind polymorphic?

 {{{#!hs
 newtype Const a (b :: k) = Const { getConst :: a }
   deriving (Generic, Generic1)
 }}}

 An example where I need it is for
 [[http://wiki.ocharles.org.uk/Name%20Binding%20in%20EDSLs|interpreting
 typed PHOAS]], the following fails to compile complaining that `The first
 argument of ‘PTerm’ should have kind ‘Ty -> *’, but ‘Const Char’ has kind
 ‘* -> *’`:

 {{{#!hs
 {-# LANGUAGE DataKinds, KindSignatures, GADTs, RankNTypes, PolyKinds #-}

 import Control.Applicative

 data Ty = TyBool | TyArr Ty Ty

 data PTerm :: (Ty -> *) -> Ty -> * where
   Var :: v t -> PTerm v t
   Tru :: PTerm v 'TyBool
   Fals :: PTerm v 'TyBool
   App :: PTerm v ('TyArr t1 t2) -> PTerm v t1 -> PTerm v t2
   Abs :: (v t1 -> PTerm v t2) -> PTerm v ('TyArr t1 t2)

 newtype Term t = Term (forall v. PTerm v t)

 showT :: Term t -> String
 showT (Term pterm) = show' 'a' pterm
   where
     show' :: Char -> PTerm (Const Char) t -> String
     show' _ (Var (Const c)) = [c]
     show' _ Tru = "True"
     show' _ Fals = "False"
     show' s (App x y) = "(" ++ show' s x ++ ") " ++ show' s y
     show' s (Abs f) = [s] ++ ". " ++ show' (succ s) (f (Const s))
 }}}

 but it compiles if one defines a bespoke form of `Const` with kind `* ->
 Ty -> *` (or the more general suggestion at the beginning of the ticket),
 I implemented all the related instances from `Control.Applicative` and the
 compiled without a hitch. Relevant discussion: a
 [[http://stackoverflow.com/questions/2023052/haskell-specifying-kind-in-
 data-declaration|question on StackOverflow]] that predates the `PolyKinds`
 extension effectively wants to define `type Const' (a :: * -> *) = Const
 Integer a` which would be possible if it were kind polymorphic.

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