Constrain.hs

{-# LANGUAGE ConstraintKinds, DataKinds, GADTs, PolyKinds, RankNTypes,
TemplateHaskell, TypeFamilies, TypeOperators, FlexibleInstances, ScopedTypeVariables, TypeApplications, AllowAmbiguousTypes #-}

import Data.Kind

data HList vv where
  HNil :: HList '[]
  HCons :: v -> HList vv -> HList (v ': vv)

type family ConstrainList (cc :: [Constraint]) :: Constraint where
  ConstrainList '[] = ()
  ConstrainList (c ': cc) = (c, ConstrainList cc)

-- From the singletons package
-- Too lazy to install singletons for proper defunctionalization.
type family Fmap (c :: k -> h) (xs :: [k]) :: [h] where
  Fmap c '[] = '[]
  Fmap c (x ': xs) = c x ': Fmap c xs

class Null a
instance Null a

-- From the constraints package
data Dict (c :: Constraint) where
  Dict :: c => Dict c

withNullC
  :: forall vv r
   . HList vv
  -> (ConstrainList (Fmap Null vv) => r)
  -> r
withNullC HNil           f = f
withNullC (HCons v tail) f = withNullC tail f

toNullC :: HList vv -> HList (Fmap Dict (Fmap Null vv))
toNullC HNil = HNil
toNullC (HCons _ tail) = HCons Dict (toNullC tail)

-- Using toNullC, we can define withNullC as a special case of this more general combinator:

withDictList
  :: forall c vv r
   . HList vv
  -> HList (Fmap Dict (Fmap c vv))
  -> (ConstrainList (Fmap c vv) => r)
  -> r
withDictList HNil HNil f = f
withDictList (HCons _ tv) (HCons Dict tc) f = withDictList @c tv tc f

-- Alternative implementation of withNullC using toNullC and withDictList
withNullC'
  :: forall vv r
   . HList vv
  -> (ConstrainList (Fmap Null vv) => r)
  -> r
withNullC' h = withDictList @Null h (toNullC h)

-- Conversely, using withNullC, we can define toNullC as a special case of:

toDictList :: forall c vv. ConstrainList (Fmap c vv) => HList vv -> HList (Fmap Dict (Fmap c vv))
toDictList HNil = HNil
toDictList (HCons _ xs) = HCons Dict (toDictList @c xs)

toNullC' :: HList vv -> HList (Fmap Dict (Fmap Null vv))
toNullC' h = withNullC h (toDictList @Null h)