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