GitLab

Is there any reason why Const isn't kind polymorphic?

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

An example where I need it is for interpreting typed PHOAS, the following fails to compile complaining that The first argument of ‘PTerm’ should have kind ‘Ty -> *’, but ‘Const Char’ has kind ‘* -> *’:

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