1{-# LANGUAGE Rank2Types, TypeFamilies, TypeOperators, ConstraintKinds, PolyKinds, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, FlexibleContexts, UndecidableInstances, CPP #-} 2module Constraints where 3 4import Control.Newtype -- from newtype 5import Data.Constraint -- from constraints 6import Data.Constraint.Unsafe -- from constraints 7import Data.Proxy -- from tagged 8import Data.Reflection -- from reflection 9#if !(MIN_VERSION_base(4,11,0)) 10import Data.Semigroup -- from semigroups 11#endif 12 13-- | Values in our dynamically constructed monoid over 'a' 14newtype Lift (p :: * -> Constraint) (a :: *) (s :: *) = Lift { lower :: a } 15 16class ReifiableConstraint p where 17 data Def (p :: * -> Constraint) (a :: *) 18 reifiedIns :: Reifies s (Def p a) :- p (Lift p a s) 19 20instance Newtype (Lift p a s) a where 21 pack = Lift 22 unpack = lower 23 24-- > ghci> with (Monoid (+) 0) $ mempty <> Lift 2 25-- > 2 26with :: Def p a -> (forall s. Reifies s (Def p a) => Lift p a s) -> a 27with d v = reify d $ lower . asProxyOf v 28 29reifyInstance :: Def p a -> (forall (s :: *). Reifies s (Def p a) => Proxy s -> r) -> r 30reifyInstance = reify 31 32asProxyOf :: f s -> Proxy s -> f s 33asProxyOf a _ = a 34 35-- > using (Monoid (+) 0) $ mappend mempty 12 36-- > 12 37using :: forall p a. ReifiableConstraint p => Def p a -> (p a => a) -> a 38using d m = reify d $ \(_ :: Proxy s) -> m \\ trans (unsafeCoerceConstraint :: (p (Lift p a s) :- p a)) reifiedIns 39 40usingT :: forall p f a. ReifiableConstraint p => Def p a -> (p a => f a) -> f a 41usingT d m = reify d $ \(_ :: Proxy s) -> m \\ trans (unsafeCoerceConstraint :: (p (Lift p a s) :- p a)) reifiedIns 42 43instance ReifiableConstraint Monoid where 44 data Def Monoid a = Monoid { mappend_ :: a -> a -> a, mempty_ :: a } 45 reifiedIns = Sub Dict 46 47instance Reifies s (Def Monoid a) => Semigroup (Lift Monoid a s) where 48 a <> b = Lift $ mappend_ (reflect a) (lower a) (lower b) 49 50instance Reifies s (Def Monoid a) => Monoid (Lift Monoid a s) where 51 mappend = (<>) 52 mempty = a where a = Lift $ mempty_ (reflect a) 53 54data ClassProxy (p :: * -> Constraint) = ClassProxy 55 56given :: ClassProxy c -> p s -> a -> Lift c a s 57given _ _ = Lift 58 59eq :: ClassProxy Eq 60eq = ClassProxy 61 62ord :: ClassProxy Ord 63ord = ClassProxy 64 65monoid :: ClassProxy Monoid 66monoid = ClassProxy 67 68instance ReifiableConstraint Eq where 69 data Def Eq a = Eq { eq_ :: a -> a -> Bool } 70 reifiedIns = Sub Dict 71 72instance Reifies s (Def Eq a) => Eq (Lift Eq a s) where 73 a == b = eq_ (reflect a) (lower a) (lower b) 74 75instance ReifiableConstraint Ord where 76 data Def Ord a = Ord { compare_ :: a -> a -> Ordering } 77 reifiedIns = Sub Dict 78 79instance Reifies s (Def Ord a) => Eq (Lift Ord a s) where 80 a == b = compare a b == EQ 81 82instance Reifies s (Def Ord a) => Ord (Lift Ord a s) where 83 compare a b = compare_ (reflect a) (lower a) (lower b) 84 85