{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Morley.Util.Type
( IsEq
, type (==)
, If
, type (++)
, IsElem
, type (/)
, type (//)
, Guard
, FailWhen
, FailUnless
, failUnlessEvi
, failWhenEvi
, AllUnique
, RequireAllUnique
, ReifyList (..)
, PatternMatch
, PatternMatchL
, KnownList (..)
, KList (..)
, RSplit
, rsplit
, Some1 (..)
, recordToSomeList
, reifyTypeEquality
, ConcatListOfTypesAssociativity
, listOfTypesConcatAssociativityAxiom
, MockableConstraint (..)
, onFirst
, knownListFromSingI
) where
import Data.Constraint (Dict(..), (:-)(..), (\\))
import Data.Singletons (SingI(sing))
import Data.Type.Bool (If, Not, type (&&))
import Data.Type.Equality (type (==))
import Data.Vinyl.Core (Rec(..))
import Data.Vinyl.Functor qualified as Vinyl
import Data.Vinyl.Recursive (recordToList, rmap)
import Data.Vinyl.TypeLevel (type (++))
import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)
import Prelude.Singletons (SList(..))
import Unsafe.Coerce (unsafeCoerce)
class a ~ b => IsEq a b
instance a ~ b => IsEq a b
type family IsElem (a :: k) (l :: [k]) :: Bool where
IsElem _ '[] = 'False
IsElem a (a ': _) = 'True
IsElem a (_ ': as) = IsElem a as
type family (l :: [k]) / (a :: k) where
'[] / _ = '[]
(a ': xs) / a = xs / a
(b ': xs) / a = b ': (xs / a)
type family (l1 :: [k]) // (l2 :: [k]) :: [k] where
l // '[] = l
l // (x ': xs) = (l / x) // xs
type family Guard (cond :: Bool) (a :: k) :: Maybe k where
Guard 'False _ = 'Nothing
Guard 'True a = 'Just a
type family FailUnless (cond :: Bool) (msg :: ErrorMessage) :: Constraint where
FailUnless 'True _ = ()
FailUnless 'False msg = TypeError msg
type FailWhen cond msg = FailUnless (Not cond) msg
failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True)
failUnlessEvi :: forall (cond :: Bool) (msg :: ErrorMessage).
FailUnless cond msg :- (cond ~ 'True)
failUnlessEvi = (FailUnless cond msg => Dict (cond ~ 'True))
-> FailUnless cond msg :- (cond ~ 'True)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub FailUnless cond msg => Dict (cond ~ 'True)
forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint
failWhenEvi :: forall cond msg. FailWhen cond msg :- (cond ~ 'False)
failWhenEvi :: forall (cond :: Bool) (msg :: ErrorMessage).
FailWhen cond msg :- (cond ~ 'False)
failWhenEvi = (FailUnless (Not cond) msg => Dict (cond ~ 'False))
-> FailUnless (Not cond) msg :- (cond ~ 'False)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub FailUnless (Not cond) msg => Dict (cond ~ 'False)
forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint
type family AllUnique (l :: [k]) :: Bool where
AllUnique '[] = 'True
AllUnique (x : xs) = Not (IsElem x xs) && AllUnique xs
type RequireAllUnique desc l = RequireAllUnique' desc l l
type family RequireAllUnique' (desc :: Symbol) (l :: [k]) (origL ::[k]) :: Constraint where
RequireAllUnique' _ '[] _ = ()
RequireAllUnique' desc (x : xs) origL =
If (IsElem x xs)
(TypeError ('Text "Duplicated " ':<>: 'Text desc ':<>: 'Text ":" ':$$:
'ShowType x ':$$:
'Text "Full list: " ':<>:
'ShowType origL
)
)
(RequireAllUnique' desc xs origL)
type family PatternMatch (a :: Type) :: Constraint where
PatternMatch Int = ((), ())
PatternMatch _ = ()
type family PatternMatchL (l :: [k]) :: Constraint where
PatternMatchL '[] = ((), ())
PatternMatchL _ = ()
class ReifyList (c :: k -> Constraint) (l :: [k]) where
reifyList :: (forall a. c a => Proxy a -> r) -> [r]
instance ReifyList c '[] where
reifyList :: forall r. (forall (a :: k). c a => Proxy a -> r) -> [r]
reifyList forall (a :: k). c a => Proxy a -> r
_ = []
instance (c x, ReifyList c xs) => ReifyList c (x ': xs) where
reifyList :: forall r. (forall (a :: a). c a => Proxy a -> r) -> [r]
reifyList forall (a :: a). c a => Proxy a -> r
reifyElem = Proxy x -> r
forall (a :: a). c a => Proxy a -> r
reifyElem (forall {t :: a}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @x) r -> [r] -> [r]
forall a. a -> [a] -> [a]
: forall k (c :: k -> Constraint) (l :: [k]) r.
ReifyList c l =>
(forall (a :: k). c a => Proxy a -> r) -> [r]
reifyList @_ @c @xs forall (a :: a). c a => Proxy a -> r
reifyElem
reifyTypeEquality :: forall a b x. (a == b) ~ 'True => (a ~ b => x) -> x
reifyTypeEquality :: forall {k} (a :: k) (b :: k) x.
((a == b) ~ 'True) =>
((a ~ b) => x) -> x
reifyTypeEquality (a ~ b) => x
x = (a ~ b) => x
x ((a ~ b) => x) -> Dict (a ~ b) -> x
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @(a ~ b)
class KnownList l where
klist :: KList l
instance KnownList '[] where
klist :: KList '[]
klist = KList '[]
forall k. KList '[]
KNil
instance KnownList xs => KnownList (x ': xs) where
klist :: KList (x : xs)
klist = Proxy x -> Proxy xs -> KList (x : xs)
forall {k} (xs :: [k]) (x :: k).
KnownList xs =>
Proxy x -> Proxy xs -> KList (x : xs)
KCons Proxy x
forall {k} (t :: k). Proxy t
Proxy Proxy xs
forall {k} (t :: k). Proxy t
Proxy
knownListFromSingI :: forall xs. SingI xs => Dict (KnownList xs)
knownListFromSingI :: forall {k} (xs :: [k]). SingI xs => Dict (KnownList xs)
knownListFromSingI = SList xs -> Dict (KnownList xs)
forall {k} (ys :: [k]). SList ys -> Dict (KnownList ys)
go (forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @xs)
where
go :: forall ys. SList ys -> Dict (KnownList ys)
go :: forall {k} (ys :: [k]). SList ys -> Dict (KnownList ys)
go = \case
SList ys
SNil -> Dict (KnownList ys)
forall (a :: Constraint). a => Dict a
Dict
SCons Sing n1
_ Sing n2
ys -> KnownList n2 => Dict (KnownList ys)
forall (a :: Constraint). a => Dict a
Dict (KnownList n2 => Dict (KnownList ys))
-> Dict (KnownList n2) -> Dict (KnownList ys)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SList n2 -> Dict (KnownList n2)
forall {k} (ys :: [k]). SList ys -> Dict (KnownList ys)
go Sing n2
SList n2
ys
data KList (l :: [k]) where
KNil :: KList '[]
KCons :: KnownList xs => Proxy x -> Proxy xs -> KList (x ': xs)
type RSplit l r = KnownList l
rsplit
:: forall k (l :: [k]) (r :: [k]) f.
(RSplit l r)
=> Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit :: forall k (l :: [k]) (r :: [k]) (f :: k -> *).
RSplit l r =>
Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit = case forall (l :: [k]). KnownList l => KList l
forall {k} (l :: [k]). KnownList l => KList l
klist @l of
KList l
KNil -> (Rec f '[]
forall {u} (a :: u -> *). Rec a '[]
RNil, )
KCons{} -> \(f r
x :& Rec f rs
r) ->
let (Rec f xs
x1, Rec f r
r1) = Rec f (xs ++ r) -> (Rec f xs, Rec f r)
forall k (l :: [k]) (r :: [k]) (f :: k -> *).
RSplit l r =>
Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit Rec f rs
Rec f (xs ++ r)
r
in (f r
x f r -> Rec f xs -> Rec f (r : xs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f xs
x1, Rec f r
r1)
data Some1 (f :: k -> Type) =
forall a. Some1 (f a)
deriving stock instance (forall a. Show (f a)) => Show (Some1 f)
recordToSomeList :: Rec f l -> [Some1 f]
recordToSomeList :: forall {k} (f :: k -> *) (l :: [k]). Rec f l -> [Some1 f]
recordToSomeList = Rec (Const (Some1 f)) l -> [Some1 f]
forall {u} a (rs :: [u]). Rec (Const a) rs -> [a]
recordToList (Rec (Const (Some1 f)) l -> [Some1 f])
-> (Rec f l -> Rec (Const (Some1 f)) l) -> Rec f l -> [Some1 f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: k). f x -> Const (Some1 f) x)
-> Rec f l -> Rec (Const (Some1 f)) l
forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (Some1 f -> Const (Some1 f) x
forall k a (b :: k). a -> Const a b
Vinyl.Const (Some1 f -> Const (Some1 f) x)
-> (f x -> Some1 f) -> f x -> Const (Some1 f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> Some1 f
forall k (f :: k -> *) (a :: k). f a -> Some1 f
Some1)
type ConcatListOfTypesAssociativity a b c = ((a ++ b) ++ c) ~ (a ++ (b ++ c))
listOfTypesConcatAssociativityAxiom :: forall a b c . Dict (ConcatListOfTypesAssociativity a b c)
listOfTypesConcatAssociativityAxiom :: forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
Dict (ConcatListOfTypesAssociativity a b c)
listOfTypesConcatAssociativityAxiom = Dict (((a ++ b) ++ c) ~ (a ++ (b ++ c)))
forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint
class MockableConstraint (c :: Constraint) where
unsafeProvideConstraint :: Dict c
instance MockableConstraint (a ~ b) where
unsafeProvideConstraint :: Dict (a ~ b)
unsafeProvideConstraint = Dict (Int ~ Int) -> Dict (a ~ b)
forall a b. a -> b
unsafeCoerce (Dict (Int ~ Int) -> Dict (a ~ b))
-> Dict (Int ~ Int) -> Dict (a ~ b)
forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict @(Int ~ Int)
instance {-# OVERLAPPABLE #-} c a => MockableConstraint (c a) where
unsafeProvideConstraint :: Dict (c a)
unsafeProvideConstraint = Dict (c a)
forall (a :: Constraint). a => Dict a
Dict
instance ( MockableConstraint c1
, MockableConstraint c2
) => MockableConstraint (c1, c2) where
unsafeProvideConstraint :: Dict (c1, c2)
unsafeProvideConstraint = Identity (Dict (c1, c2)) -> Dict (c1, c2)
forall a. Identity a -> a
runIdentity (Identity (Dict (c1, c2)) -> Dict (c1, c2))
-> Identity (Dict (c1, c2)) -> Dict (c1, c2)
forall a b. (a -> b) -> a -> b
$ do
Dict c1
Dict <- Dict c1 -> Identity (Dict c1)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c1 -> Identity (Dict c1)) -> Dict c1 -> Identity (Dict c1)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c1
Dict c2
Dict <- Dict c2 -> Identity (Dict c2)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c2 -> Identity (Dict c2)) -> Dict c2 -> Identity (Dict c2)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c2
Dict (c1, c2) -> Identity (Dict (c1, c2))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (c1, c2)
forall (a :: Constraint). a => Dict a
Dict
{-# INLINE unsafeProvideConstraint #-}
instance ( MockableConstraint c1
, MockableConstraint c2
, MockableConstraint c3
) => MockableConstraint (c1, c2, c3) where
unsafeProvideConstraint :: Dict (c1, c2, c3)
unsafeProvideConstraint = Identity (Dict (c1, c2, c3)) -> Dict (c1, c2, c3)
forall a. Identity a -> a
runIdentity (Identity (Dict (c1, c2, c3)) -> Dict (c1, c2, c3))
-> Identity (Dict (c1, c2, c3)) -> Dict (c1, c2, c3)
forall a b. (a -> b) -> a -> b
$ do
Dict (c1, c2)
Dict <- Dict (c1, c2) -> Identity (Dict (c1, c2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict (c1, c2) -> Identity (Dict (c1, c2)))
-> Dict (c1, c2) -> Identity (Dict (c1, c2))
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @(c1, c2)
Dict c3
Dict <- Dict c3 -> Identity (Dict c3)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c3 -> Identity (Dict c3)) -> Dict c3 -> Identity (Dict c3)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c3
Dict (c1, c2, c3) -> Identity (Dict (c1, c2, c3))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (c1, c2, c3)
forall (a :: Constraint). a => Dict a
Dict
{-# INLINE unsafeProvideConstraint #-}
instance ( MockableConstraint c1
, MockableConstraint c2
, MockableConstraint c3
, MockableConstraint c4
) => MockableConstraint (c1, c2, c3, c4) where
unsafeProvideConstraint :: Dict (c1, c2, c3, c4)
unsafeProvideConstraint = Identity (Dict (c1, c2, c3, c4)) -> Dict (c1, c2, c3, c4)
forall a. Identity a -> a
runIdentity (Identity (Dict (c1, c2, c3, c4)) -> Dict (c1, c2, c3, c4))
-> Identity (Dict (c1, c2, c3, c4)) -> Dict (c1, c2, c3, c4)
forall a b. (a -> b) -> a -> b
$ do
Dict (c1, c2, c3)
Dict <- Dict (c1, c2, c3) -> Identity (Dict (c1, c2, c3))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict (c1, c2, c3) -> Identity (Dict (c1, c2, c3)))
-> Dict (c1, c2, c3) -> Identity (Dict (c1, c2, c3))
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @(c1, c2, c3)
Dict c4
Dict <- Dict c4 -> Identity (Dict c4)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c4 -> Identity (Dict c4)) -> Dict c4 -> Identity (Dict c4)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c4
Dict (c1, c2, c3, c4) -> Identity (Dict (c1, c2, c3, c4))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (c1, c2, c3, c4)
forall (a :: Constraint). a => Dict a
Dict
{-# INLINE unsafeProvideConstraint #-}
instance ( MockableConstraint c1
, MockableConstraint c2
, MockableConstraint c3
, MockableConstraint c4
, MockableConstraint c5
) => MockableConstraint (c1, c2, c3, c4, c5) where
unsafeProvideConstraint :: Dict (c1, c2, c3, c4, c5)
unsafeProvideConstraint = Identity (Dict (c1, c2, c3, c4, c5)) -> Dict (c1, c2, c3, c4, c5)
forall a. Identity a -> a
runIdentity (Identity (Dict (c1, c2, c3, c4, c5)) -> Dict (c1, c2, c3, c4, c5))
-> Identity (Dict (c1, c2, c3, c4, c5))
-> Dict (c1, c2, c3, c4, c5)
forall a b. (a -> b) -> a -> b
$ do
Dict (c1, c2, c3, c4)
Dict <- Dict (c1, c2, c3, c4) -> Identity (Dict (c1, c2, c3, c4))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict (c1, c2, c3, c4) -> Identity (Dict (c1, c2, c3, c4)))
-> Dict (c1, c2, c3, c4) -> Identity (Dict (c1, c2, c3, c4))
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @(c1, c2, c3, c4)
Dict c5
Dict <- Dict c5 -> Identity (Dict c5)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c5 -> Identity (Dict c5)) -> Dict c5 -> Identity (Dict c5)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c5
Dict (c1, c2, c3, c4, c5) -> Identity (Dict (c1, c2, c3, c4, c5))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (c1, c2, c3, c4, c5)
forall (a :: Constraint). a => Dict a
Dict
{-# INLINE unsafeProvideConstraint #-}
onFirst :: Bifunctor p => p a c -> (a -> b) -> p b c
onFirst :: forall (p :: * -> * -> *) a c b.
Bifunctor p =>
p a c -> (a -> b) -> p b c
onFirst = ((a -> b) -> p a c -> p b c) -> p a c -> (a -> b) -> p b c
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> b) -> p a c -> p b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first