HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

Moduleconstraints-extras-0.4.0.2Haskell2010

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

  • 2 types
  • 2 classes
  • 5 values

The Has typeclass

3 declarations
classclass Has (c :: k -> Constraint) (f :: k -> Type) where
#

The constraint Has c f means that given any value of type f a, we can determine that there is an instance of c a. For example, Has Show Tag means that given any x :: Tag a, we can conclude Show a. Most commonly, the type f will be a GADT, where we can enumerate all the possible index types through pattern matching, and discover that there is an appropriate instance in each case. In this sort of situation, the c can be left entirely polymorphic in the instance for Has, and this is the sort of instance that the provided Template Haskell code writes.

Methods

  • has :: f a -> (c a => r) -> r

    Use the f a to show that there is an instance of c a, and bring it into scope.

    The order of type variables is chosen to work with -XTypeApplications.

    -- Hold a value of type 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
  • argDict :: f a -> Dict (c a)

    Use an f a to obtain a dictionary for c a

    argDict @Show I :: Dict (Show Int)
Instances2Has
  • (Has c f, Has c g) => Has c (Sum f g)Defined in constraints-extras-0.4.0.2 · Data.Constraint.Extras
  • (Has c f, Has c g) => Has c (f :+: g)Defined in constraints-extras-0.4.0.2 · Data.Constraint.Extras
valueargDict' :: Has' c f g => f a -> Dict (c (g a))
#

Get a dictionary for c (g a), using a value of type f a.

argDict' @Show @Identity B :: Dict (Show (Identity Bool))
valueargDictV :: HasV c f g => f v -> Dict (c (v g))
#

Get a dictionary for c (v g), using a value of type f v.

Bringing instances into scope

5 declarations
typetype Has' (c :: k -> Constraint) (f :: k' -> Type) (g :: k' -> k) = Has (ComposeC c g) f
#

The constraint Has' c f g means that given a value of type f a, we can satisfy the constraint c (g a).

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
typetype HasV (c :: k2 -> Constraint) (f :: (k' -> k2) -> Type) (g :: k') = Has (FlipC (ComposeC c) g) f
#

The constraint HasV c f g means that given a value of type f v, we can satisfy the constraint c (v g).

valuehasV :: HasV c f g => f v -> (c (v g) => r) -> r
#

Similar to has, but given a value of type f v, we get a c (v g) instance brought into scope instead.

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