Universally quantified constraints

UniversallyQuantifiedConstraints.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module ForallConstraints where
import Data.Monoid
import Data.Constraint
import Data.Constraint.Forall

data Box t where
  Box :: t a -> Box t

-- This doesn't typecheck
-- example :: forall t. (forall a. Monoid (t a)) => Box t -> Box t
-- example (Box x) = Box (x <> x)

-- Bake the constraint into the data type
data MonBox t where
  MonBox :: Monoid (t a) => t a -> MonBox t

example1 :: MonBox t -> MonBox t
example1 (MonBox x) = MonBox (x <> x)

-- Use the constraints package
example2 :: ForallF Monoid t => Box t -> Box t
example2 (Box (x :: t a)) = Box (x <> x)
  \\ (instF :: ForallF Monoid t :- Monoid (t a))