{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE DataKinds #-}
module Data.Summer
(
Sum
, pattern Inj
, tag
, inject
, inspect
, consider
, considerFirst
, variant
, UnorderedMatch(unorderedMatch)
, Match(match, override, unmatch)
, Unmatch
, TagIn
, HasTagIn
, Delete
, HaveSameTagsIn
, Matcher
, Weaken(weaken)
, noOpWeaken
, inmap
, smap
, ApplyFunction(apply)
, type ForAll
) where
import Control.Exception (catch, SomeException)
import Unsafe.Coerce (unsafeCoerce)
import GHC.Exts (Any, Constraint)
import GHC.TypeLits (Nat, KnownNat, natVal, type (+))
import Data.Proxy (Proxy(Proxy))
import Data.Kind (Type)
import Control.Monad (unless)
import Generics.SOP (Generic(..))
import qualified Generics.SOP as SOP
import Data.Profunctor (Profunctor(dimap), Choice(..))
import Data.Typeable (typeRep, Typeable)
import Data.ForAll (type ForAll)
data Sum (xs :: [*]) = UnsafeInj {-# UNPACK #-} !Word Any
deriving (Typeable)
eject :: Sum '[x] -> x
eject :: forall x. Sum '[x] -> x
eject (UnsafeInj Word
_ Any
x) = forall a b. a -> b
unsafeCoerce Any
x
{-# INLINE CONLIKE eject #-}
variant :: forall a b xs p f. (a `HasTagIn` xs, Applicative f, Choice p) => p a (f b) -> p (Sum xs) (f (Sum (Replace a b xs)))
variant :: forall a b (xs :: [*]) (p :: * -> * -> *) (f :: * -> *).
(HasTagIn a xs, Applicative f, Choice p) =>
p a (f b) -> p (Sum xs) (f (Sum (Replace a b xs)))
variant p a (f b)
p = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Sum xs -> Either a (Sum (Replace a b xs))
try Either (f b) (Sum (Replace a b xs)) -> f (Sum (Replace a b xs))
replace (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' p a (f b)
p) where
try :: Sum xs -> Either a (Sum (Replace a b xs))
try :: Sum xs -> Either a (Sum (Replace a b xs))
try (UnsafeInj Word
t Any
x) = if Word
t forall a. Eq a => a -> a -> Bool
== forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @a @xs then forall a b. a -> Either a b
Left (forall a b. a -> b
unsafeCoerce Any
x) else forall a b. b -> Either a b
Right (forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
t Any
x)
replace :: Either (f b) (Sum (Replace a b xs)) -> f (Sum (Replace a b xs))
replace :: Either (f b) (Sum (Replace a b xs)) -> f (Sum (Replace a b xs))
replace = \case
Left f b
fb -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @a @xs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b
unsafeCoerce) f b
fb
Right Sum (Replace a b xs)
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Sum (Replace a b xs)
s
{-# INLINE CONLIKE variant #-}
type family Replace x y xs where
Replace x y (x ': xs) = y ': xs
Replace x y (z ': xs) = z ': Replace x y xs
Replace x y '[] = '[]
instance Generic (Sum '[]) where
type Code (Sum '[]) = '[]
from :: Sum '[] -> Rep (Sum '[])
from Sum '[]
a = forall a. HasCallStack => [Char] -> a
error [Char]
"Generics.SOP.from: Impossible to create an empty sum"
to :: Rep (Sum '[]) -> Sum '[]
to Rep (Sum '[])
a = forall a. HasCallStack => [Char] -> a
error [Char]
"Generics.SOP.to: Impossible to create an empty sum"
instance Generic (Sum xs) => Generic (Sum (x ': xs)) where
type Code (Sum (x ': xs)) = '[x] ': Code (Sum xs)
from :: Sum (x : xs) -> Rep (Sum (x : xs))
from (UnsafeInj Word
0 Any
x) = forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP (forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
SOP.Z (forall a. a -> I a
SOP.I (forall a b. a -> b
unsafeCoerce Any
x) forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
SOP.:* forall {k} (a :: k -> *). NP a '[]
SOP.Nil))
from Sum (x : xs)
xs = forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP (forall {k} (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
SOP.S NS (NP I) (Code (Sum xs))
ns) where
SOP.SOP NS (NP I) (Code (Sum xs))
ns = forall a. Generic a => a -> Rep a
from (forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
xs)
to :: Rep (Sum (x : xs)) -> Sum (x : xs)
to (SOP.SOP NS (NP I) (Code (Sum (x : xs)))
ns) = case NS (NP I) (Code (Sum (x : xs)))
ns of
SOP.Z (SOP.I x
x SOP.:* NP I xs
SOP.Nil) -> forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
0 (forall a b. a -> b
unsafeCoerce x
x)
SOP.S NS (NP I) xs
s -> Sum xs -> Sum (x : xs)
recall (forall a. Generic a => Rep a -> a
to (forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP NS (NP I) xs
s))
where
recall :: Sum xs -> Sum (x ': xs)
recall :: Sum xs -> Sum (x : xs)
recall (UnsafeInj Word
i Any
a) = forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
i forall a. Num a => a -> a -> a
+ Word
1) Any
a
type role Sum representational
pattern Inj :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
pattern $bInj :: forall x (xs :: [*]). HasTagIn x xs => x -> Sum xs
$mInj :: forall {r} {x} {xs :: [*]}.
HasTagIn x xs =>
Sum xs -> (x -> r) -> ((# #) -> r) -> r
Inj x <- (inspect -> Just x)
where
Inj x
x = forall x (xs :: [*]). HasTagIn x xs => x -> Sum xs
inject x
x
type family TagIn (x :: k) (xs :: [k]) where
TagIn x (x ': xs) = 0
TagIn x (y ': xs) = 1 + TagIn x xs
class KnownNat (x `TagIn` xs) => x `HasTagIn` xs
instance KnownNat (x `TagIn` xs) => x `HasTagIn` xs
tag :: forall x xs. x `HasTagIn` xs => Word
tag :: forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @(TagIn x xs))
{-# INLINE CONLIKE tag #-}
inject :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
inject :: forall x (xs :: [*]). HasTagIn x xs => x -> Sum xs
inject x
x = forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs) (forall a b. a -> b
unsafeCoerce x
x)
{-# INLINE CONLIKE inject #-}
inspect :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Maybe x
inspect :: forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Maybe x
inspect (UnsafeInj Word
tag' Any
x) = if forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs forall a. Eq a => a -> a -> Bool
== Word
tag' then forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce Any
x) else forall a. Maybe a
Nothing
{-# INLINE CONLIKE inspect #-}
type family Delete (x :: k) (xs :: [k]) :: [k] where
Delete x (x ': xs) = xs
Delete x (y ': xs) = y ': Delete x xs
Delete x '[] = '[]
consider :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Either (Sum (Delete x xs)) x
consider :: forall x (xs :: [*]).
HasTagIn x xs =>
Sum xs -> Either (Sum (Delete x xs)) x
consider (UnsafeInj Word
tag' Any
x) =
if Word
tag' forall a. Eq a => a -> a -> Bool
== forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs
then forall a b. b -> Either a b
Right (forall a b. a -> b
unsafeCoerce Any
x)
else forall a b. a -> Either a b
Left (forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (if Word
tag' forall a. Ord a => a -> a -> Bool
>= forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word
tag' forall a. Num a => a -> a -> a
- Word
1 else Word
tag') Any
x)
{-# INLINE CONLIKE consider #-}
considerFirst :: forall x xs. Sum (x ': xs) -> Either (Sum xs) x
considerFirst :: forall x (xs :: [*]). Sum (x : xs) -> Either (Sum xs) x
considerFirst = forall x (xs :: [*]).
HasTagIn x xs =>
Sum xs -> Either (Sum (Delete x xs)) x
consider
{-# INLINE CONLIKE considerFirst #-}
inmap :: forall x y xs. (x `HasTagIn` xs, y `HasTagIn` xs) => (x -> y) -> Sum xs -> Sum xs
inmap :: forall x y (xs :: [*]).
(HasTagIn x xs, HasTagIn y xs) =>
(x -> y) -> Sum xs -> Sum xs
inmap x -> y
f uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) = if Word
tag' forall a. Eq a => a -> a -> Bool
== forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @xs) (forall a b. a -> b
unsafeCoerce (x -> y
f (forall a b. a -> b
unsafeCoerce Any
x))) else Sum xs
uv
{-# INLINE CONLIKE inmap #-}
smap :: forall x y xs ys. (Weaken (Delete x xs) ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys
smap :: forall x y (xs :: [*]) (ys :: [*]).
(Weaken (Delete x xs) ys, HasTagIn x xs, HasTagIn y ys) =>
(x -> y) -> Sum xs -> Sum ys
smap x -> y
f uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) = if Word
tag' forall a. Eq a => a -> a -> Bool
== forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @ys) (forall a b. a -> b
unsafeCoerce (x -> y
f (forall a b. a -> b
unsafeCoerce Any
x))) else forall (xs :: [*]) (ys :: [*]). Weaken xs ys => Sum xs -> Sum ys
weaken (forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Sum (Delete x xs)
unsafeForget @x Sum xs
uv)
{-# INLINE CONLIKE smap #-}
class HaveSameTagsIn xs ys
instance {-# OVERLAPPABLE #-} HaveSameTagsIn '[] ys
instance {-# OVERLAPPABLE #-} HaveSameTagsIn xs ys => HaveSameTagsIn (x ': xs) (x ': ys)
noOpWeaken :: forall xs ys. (xs `HaveSameTagsIn` ys) => Sum xs -> Sum ys
noOpWeaken :: forall (xs :: [*]) (ys :: [*]).
HaveSameTagsIn xs ys =>
Sum xs -> Sum ys
noOpWeaken = forall a b. a -> b
unsafeCoerce
{-# INLINE CONLIKE noOpWeaken #-}
unsafeForget :: forall x xs. x `HasTagIn` xs => Sum xs -> Sum (Delete x xs)
unsafeForget :: forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Sum (Delete x xs)
unsafeForget (UnsafeInj Word
tag' Any
x) = if Word
tag' forall a. Ord a => a -> a -> Bool
< forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
tag' Any
x
else if Word
tag' forall a. Eq a => a -> a -> Bool
== forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then forall a. HasCallStack => [Char] -> a
error [Char]
"unsafeForget: you can't forget the truth"
else forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
tag' forall a. Num a => a -> a -> a
- Word
1) Any
x
{-# INLINE CONLIKE unsafeForget #-}
unsafeForgetFirst :: Sum (x ': xs) -> Sum xs
unsafeForgetFirst :: forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst (UnsafeInj Word
tag' Any
x) = forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
tag' forall a. Num a => a -> a -> a
- Word
1) Any
x
{-# INLINE CONLIKE unsafeForgetFirst #-}
instance (Eq (Sum xs), Eq x) => Eq (Sum (x ': xs)) where
uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x) == :: Sum (x : xs) -> Sum (x : xs) -> Bool
== uv' :: Sum (x : xs)
uv'@(UnsafeInj Word
tag'' Any
x')
| Word
tag' forall a. Eq a => a -> a -> Bool
== Word
tag'' =
if Word
tag' forall a. Eq a => a -> a -> Bool
== Word
0
then forall a b. a -> b
unsafeCoerce @_ @x Any
x forall a. Eq a => a -> a -> Bool
== forall a b. a -> b
unsafeCoerce @_ @x Any
x'
else forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv forall a. Eq a => a -> a -> Bool
== forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv'
| Bool
otherwise = Bool
False
{-# INLINE CONLIKE (==) #-}
instance Eq (Sum '[]) where
== :: Sum '[] -> Sum '[] -> Bool
(==) = forall a. HasCallStack => [Char] -> a
error [Char]
"(==) base case: impossible by construction"
{-# INLINE CONLIKE (==) #-}
class (Show x, Typeable x) => ShowTypeable x
instance (Show x, Typeable x) => ShowTypeable x
instance ApplyFunction ShowTypeable xs => Show (Sum xs) where
showsPrec :: Int -> Sum xs -> ShowS
showsPrec Int
d Sum xs
v = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
[Char] -> ShowS
showString [Char]
"Inj @"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> Constraint) (xs :: [*]) y.
ApplyFunction c xs =>
(forall a. c a => a -> y) -> Sum xs -> y
apply @ShowTypeable (\(a
x :: x) ->
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
d forall a. Num a => a -> a -> a
+ Int
1) (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
" "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ShowS -> ShowS
showParen Bool
True (forall a. Show a => Int -> a -> ShowS
showsPrec (Int
d forall a. Num a => a -> a -> a
+ Int
1) a
x)
) Sum xs
v
class Weaken xs ys where
weaken :: Sum xs -> Sum ys
instance (Weaken xs ys, x `HasTagIn` ys) => Weaken (x ': xs) ys where
weaken :: Sum (x : xs) -> Sum ys
weaken uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x) =
if Word
tag' forall a. Eq a => a -> a -> Bool
== Word
0
then forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @ys) Any
x
else let UnsafeInj Word
tag'' Any
_ = forall (xs :: [*]) (ys :: [*]). Weaken xs ys => Sum xs -> Sum ys
weaken @xs @ys (forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv) in forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
tag'' Any
x
{-# INLINE CONLIKE weaken #-}
instance Weaken '[] ys where
weaken :: Sum '[] -> Sum ys
weaken = forall a. HasCallStack => [Char] -> a
error [Char]
"weaken base case: impossible by construction"
{-# INLINE CONLIKE weaken #-}
class UnorderedMatch xs matcher where
unorderedMatch :: Sum xs -> matcher
instance UnorderedMatch '[] r where
unorderedMatch :: Sum '[] -> r
unorderedMatch = forall a. HasCallStack => [Char] -> a
error [Char]
"unordered match base case: impossible by construction"
instance
( Result matcher ~ r
, Match (Unmatcher matcher r)
, Matcher (Unmatcher matcher r) r ~ matcher
, y `HasTagIn` xs
, UnorderedMatch (Delete y xs) matcher
) => UnorderedMatch xs ((y -> r) -> matcher) where
unorderedMatch :: Sum xs -> (y -> r) -> matcher
unorderedMatch :: Sum xs -> (y -> r) -> matcher
unorderedMatch uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) y -> r
f =
if Word
tag' forall a. Eq a => a -> a -> Bool
== forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @xs
then forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @(Unmatcher matcher r) @r (y -> r
f (forall a b. a -> b
unsafeCoerce Any
x)) forall a b. (a -> b) -> a -> b
$ forall (xs :: [*]) matcher.
UnorderedMatch xs matcher =>
Sum xs -> matcher
unorderedMatch @(Delete y xs) @matcher (forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Sum (Delete x xs)
unsafeForget @y Sum xs
uv)
else forall (xs :: [*]) matcher.
UnorderedMatch xs matcher =>
Sum xs -> matcher
unorderedMatch @(Delete y xs) @matcher (forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Sum (Delete x xs)
unsafeForget @y Sum xs
uv)
type family Result matcher :: Type where
Result ((x -> r) -> matcher) = r
Result r = r
type family Unmatcher matcher r :: [Type] where
Unmatcher r r = '[]
Unmatcher ((x -> r) -> matcher) r = x ': Unmatcher matcher r
type family Matcher xs r :: Type where
Matcher '[] r = r
Matcher (x ': xs) r = (x -> r) -> Matcher xs r
class Match xs where
match :: forall r. Sum xs -> Matcher xs r
unmatch :: (forall r. Matcher xs r) -> Sum xs
override :: forall r. r -> Matcher xs r -> Matcher xs r
instance Match '[] where
match :: forall r. Sum '[] -> Matcher '[] r
match = forall a. HasCallStack => [Char] -> a
error [Char]
"match base case: impossible by construction"
{-# INLINE CONLIKE match #-}
unmatch :: (forall r. Matcher '[] r) -> Sum '[]
unmatch forall r. Matcher '[] r
r = forall r. Matcher '[] r
r
{-# INLINE CONLIKE unmatch #-}
override :: forall r. r -> Matcher '[] r -> Matcher '[] r
override = forall a b. a -> b -> a
const
{-# INLINE CONLIKE override #-}
instance (Unmatch xs (x ': xs), Match xs) => Match (x ': xs) where
match :: forall r. Sum (x ': xs) -> (x -> r) -> Matcher xs r
match :: forall r. Sum (x : xs) -> (x -> r) -> Matcher xs r
match uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x) x -> r
f =
if Word
tag' forall a. Eq a => a -> a -> Bool
== Word
0
then forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @xs @r (x -> r
f (forall a b. a -> b
unsafeCoerce Any
x)) forall a b. (a -> b) -> a -> b
$ forall (xs :: [*]) r. Match xs => Sum xs -> Matcher xs r
match @xs @r (forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv)
else forall (xs :: [*]) r. Match xs => Sum xs -> Matcher xs r
match @xs @r (forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv)
{-# INLINE CONLIKE match #-}
unmatch :: (forall r. (x -> r) -> Matcher xs r) -> Sum (x ': xs)
unmatch :: (forall r. (x -> r) -> Matcher xs r) -> Sum (x : xs)
unmatch forall r. (x -> r) -> Matcher xs r
g = forall (xs :: [*]) (ys :: [*]).
Unmatch xs ys =>
Matcher xs (Sum ys) -> Sum ys
unmatchGo @xs forall a b. (a -> b) -> a -> b
$ forall r. (x -> r) -> Matcher xs r
g @(Sum (x ': xs)) (forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b
unsafeCoerce @x)
{-# INLINE CONLIKE unmatch #-}
override :: forall r. r -> Matcher (x : xs) r -> Matcher (x : xs) r
override r
r Matcher (x : xs) r
m = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @xs r
r) Matcher (x : xs) r
m
{-# INLINE CONLIKE override #-}
class Unmatch xs ys where
unmatchGo :: Matcher xs (Sum ys) -> Sum ys
instance Unmatch '[] ys where
unmatchGo :: Matcher '[] (Sum ys) -> Sum ys
unmatchGo = forall a. a -> a
id
{-# INLINE CONLIKE unmatchGo #-}
instance (Unmatch xs ys, x `HasTagIn` ys) => Unmatch (x ': xs) ys where
unmatchGo :: Matcher (x : xs) (Sum ys) -> Sum ys
unmatchGo Matcher (x : xs) (Sum ys)
f = forall (xs :: [*]) (ys :: [*]).
Unmatch xs ys =>
Matcher xs (Sum ys) -> Sum ys
unmatchGo @xs (Matcher (x : xs) (Sum ys)
f (forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (forall {k} (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @ys) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b
unsafeCoerce @x))
{-# INLINE CONLIKE unmatchGo #-}
class ForAll c xs => ApplyFunction c xs where
apply :: (forall a. c a => a -> y) -> Sum xs -> y
instance ApplyFunction c '[] where
apply :: forall y. (forall a. c a => a -> y) -> Sum '[] -> y
apply forall a. c a => a -> y
_f Sum '[]
x = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: empty sum"
{-# INLINE CONLIKE apply #-}
instance (c x, ApplyFunction c xs) => ApplyFunction c (x ': xs) where
apply :: forall y. (forall a. c a => a -> y) -> Sum (x : xs) -> y
apply forall a. c a => a -> y
f Sum (x : xs)
x = case forall x (xs :: [*]). Sum (x : xs) -> Either (Sum xs) x
considerFirst Sum (x : xs)
x of
Right x
x' -> forall a. c a => a -> y
f x
x'
Left Sum xs
xs -> forall (c :: * -> Constraint) (xs :: [*]) y.
ApplyFunction c xs =>
(forall a. c a => a -> y) -> Sum xs -> y
apply @c forall a. c a => a -> y
f Sum xs
xs
{-# INLINE CONLIKE apply #-}