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

[GHC]

#10039: Make Const (Control.Applicative) kind polymorphic in its second argument
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                   Owner:  ekmett
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Core Libraries    |                 Version:  7.8.4
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

Old description:

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

New description:

 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 it
 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#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler