Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,399
    • Issues 5,399
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 592
    • Merge requests 592
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #10039
Closed
Open
Issue created Jan 28, 2015 by Icelandjack@IcelandjackReporter

Make Const (Control.Applicative) kind polymorphic in its second argument

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.

Edited Mar 10, 2019 by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking