HORIZON HASKELLDocslts/ghc-9.14.x45dd5372026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 45dd537 · 2026-10-11

Moduleconstraints-extras-0.3.2.1Haskell2010

Data.Constraint.Extras

Throughout this module, we use the following GADT and ArgDict instance in our examples:

{-# LANGUAGE StandaloneDeriving #-}

data Tag a where
  I :: Tag Int
  B :: Tag Bool
deriving instance Show (Tag a)

$(deriveArgDict ''Tag)

The constructors of Tag mean that a type variable a in Tag a must come from the set { Int, Bool }. We call this the "set of types a that could be applied to Tag".

  • 6 types
  • 2 classes
  • 6 values

The ArgDict typeclass

5 declarations
classclass ArgDict (c :: k -> Constraint) (f :: k -> Type) where
#

Morally, this class is for GADTs whose indices can be finitely enumerated. An ArgDict c f instance allows us to do two things:

  1. ConstraintsFor requests the set of constraints c a for all possible types a that could be applied to f.

  2. argDict selects a specific c a given a value of type f a.

Use deriveArgDict to derive instances of this class.

Associated types

Methods

  • argDict :: ConstraintsFor f c => f a -> Dict (c a)

    Use an f a to select a specific dictionary from ConstraintsFor f c.

    argDict I :: Dict (Show Int)
Instances2ArgDict
typetype ConstraintsFor' (f :: k' -> Type) (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g)
#

"Primed" variants (ConstraintsFor', argDict', Has', has', &c.) use the ArgDict instance on f to apply constraints on g a instead of just a. This is often useful when you have data structures parameterised by something of kind (x -> Type) -> Type, like in the dependent-sum and dependent-map libraries.

ConstraintsFor' Tag Show Identity = (Show (Identity Int), Show (Identity Bool))
valueargDict' :: Has' c f g => f a -> Dict (c (g a))
#

Get a dictionary for a specific g a, using a value of type f a.

argDict' B :: Dict (Show (Identity Bool))

Bringing instances into scope

7 declarations
typetype Has (c :: k -> Constraint) (f :: k -> Type) = (ArgDict c f, ConstraintsFor f c)
#

Has c f is a constraint which means that for every type a that could be applied to f, we have c a.

Has Show Tag = (ArgDict Show Tag, Show Int, Show Bool)
valuehas :: Has c f => f a -> (c a => r) -> r
#

Use the a from f a to select a specific c a constraint, and bring it into scope. The order of type variables is chosen to work with -XTypeApplications.

-- Hold an a, along with a tag identifying the a.
data SomeTagged tag where
  SomeTagged :: a -> tag a -> SomeTagged tag

-- Use the stored tag to identify the thing we have, allowing us to call 'show'. Note that we
-- have no knowledge of the tag type.
showSomeTagged :: Has Show tag => SomeTagged tag -> String
showSomeTagged (SomeTagged a tag) = has @Show tag $ show a
typetype Has' (c :: k -> Constraint) (f :: k' -> Type) (g :: k' -> k) = (ArgDict (ComposeC c g) f, ConstraintsFor' f c g)
#

Has' c f g is a constraint which means that for every type a that could be applied to f, we have c (g a).

Has' Show Tag Identity = (ArgDict (Show . Identity) Tag, Show (Identity Int), Show (Identity Bool))
valuehas' :: Has' c f g => f a -> (c (g a) => r) -> r
#

Like has, but we get a c (g a) instance brought into scope instead. Use -XTypeApplications to specify c and g.

-- From dependent-sum:Data.Dependent.Sum
data DSum tag f = forall a. !(tag a) :=> f a

-- Show the value from a dependent sum. (We'll need 'whichever', discussed later, to show the key.)
showDSumVal :: forall tag f . Has' Show tag f => DSum tag f -> String
showDSumVal (tag :=> fa) = has' @Show @f tag $ show fa
valuehasV :: HasV c f g => f v -> (c (v g) => r) -> r
#
valuewhichever :: ForallF c t => (c (t a) => r) -> r
#

Given "forall a. c (t a)" (the ForallF c t constraint), select a specific a, and bring c (t a) into scope. Use -XTypeApplications to specify c, t and a.

-- Show the tag of a dependent sum, even though we don't know the tag type.
showDSumKey :: forall tag f . ForallF Show tag => DSum tag f -> String
showDSumKey ((tag :: tag a) :=> fa) = whichever @Show @tag @a $ show tag

Misc

1 declaration

Deprecated

1 declaration