{-# 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
Copyright: (c) Samuel Schlesinger 2020
License: MIT
Maintainer: sgschlesinger@gmail.com
Stability: experimental
Portability: non-portable
Description: Extensible sums
-}
module Data.Summer
  ( -- * The extensible sum type and its associated pattern for convenience
    Sum
  , pattern Inj
  , tag
  -- * Construction and Deconstruction
  , inject
  , inspect
  , consider
  , considerFirst
  , variant
  , Match(match, override, unmatch)
  , Unmatch
  -- * Type families
  , TagIn
  , HasTagIn
  , Delete
  , HaveSameTagsIn
  , Matcher
  -- * Weakening extensible sums
  , Weaken(weaken)
  , noOpWeaken
  -- * Transforming extensible sums
  , inmap
  , smap
  -- * Applying Polymorphic Functions
  , 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.ForAll (type ForAll)

-- | The extensible sum type, allowing inhabitants to be of any of the
-- types in the given type list.
data Sum (xs :: [*]) = UnsafeInj {-# UNPACK #-} !Word Any

-- | A prism which operates on a chosen variant of a 'Sum'
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 :: p a (f b) -> p (Sum xs) (f (Sum (Replace a b xs)))
variant p a (f b)
p = (Sum xs -> Either a (Sum (Replace a b xs)))
-> (Either (f b) (Sum (Replace a b xs))
    -> f (Sum (Replace a b xs)))
-> p (Either a (Sum (Replace a b xs)))
     (Either (f b) (Sum (Replace a b xs)))
-> p (Sum xs) (f (Sum (Replace a b xs)))
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 (p a (f b)
-> p (Either a (Sum (Replace a b xs)))
     (Either (f b) (Sum (Replace a b xs)))
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 Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn a xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @a @xs then a -> Either a (Sum (Replace a b xs))
forall a b. a -> Either a b
Left (Any -> a
forall a b. a -> b
unsafeCoerce Any
x) else Sum (Replace a b xs) -> Either a (Sum (Replace a b xs))
forall a b. b -> Either a b
Right (Word -> Any -> Sum (Replace a b xs)
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 -> (b -> Sum (Replace a b xs)) -> f b -> f (Sum (Replace a b xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Word -> Any -> Sum (Replace a b xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn a xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @a @xs) (Any -> Sum (Replace a b xs))
-> (b -> Any) -> b -> Sum (Replace a b xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Any
forall a b. a -> b
unsafeCoerce) f b
fb
    Right Sum (Replace a b xs)
s -> Sum (Replace a b xs) -> f (Sum (Replace a b xs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sum (Replace a b xs)
s

-- | Type family for replacing one type in a type level list with another
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 = [Char] -> SOP I '[]
forall a. HasCallStack => [Char] -> a
error [Char]
"Generics.SOP.from: Impossible to create an empty sum"
  to :: Rep (Sum '[]) -> Sum '[]
to Rep (Sum '[])
a = [Char] -> Sum '[]
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) = NS (NP I) ('[x] : Code (Sum xs)) -> SOP I ('[x] : Code (Sum xs))
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP (NP I '[x] -> NS (NP I) ('[x] : Code (Sum xs))
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
SOP.Z (x -> I x
forall a. a -> I a
SOP.I (Any -> x
forall a b. a -> b
unsafeCoerce Any
x) I x -> NP I '[] -> NP I '[x]
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
SOP.:* NP I '[]
forall k (a :: k -> *). NP a '[]
SOP.Nil))
  from Sum (x : xs)
xs = NS (NP I) ('[x] : Code (Sum xs)) -> SOP I ('[x] : Code (Sum xs))
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP (NS (NP I) (Code (Sum xs)) -> NS (NP I) ('[x] : Code (Sum xs))
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 = Sum xs -> SOP I (Code (Sum xs))
forall a. Generic a => a -> Rep a
from (Sum (x : xs) -> Sum xs
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) -> Word -> Any -> Sum (x : xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
0 (x -> Any
forall a b. a -> b
unsafeCoerce x
x)
    SOP.S NS (NP I) xs
s -> Sum xs -> Sum (x : xs)
recall (SOP I (Code (Sum xs)) -> Sum xs
forall a. Generic a => Rep a -> a
to (NS (NP I) xs -> SOP I xs
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) = Word -> Any -> Sum (x : xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
i Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Any
a

type role Sum representational

-- | A pattern to match on for convenience. Without this, the user facing
-- interface is rather baroque.
pattern Inj :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
pattern $bInj :: x -> Sum xs
$mInj :: forall r x (xs :: [*]).
HasTagIn x xs =>
Sum xs -> (x -> r) -> (Void# -> r) -> r
Inj x <- (inspect -> Just x)
  where
    Inj x
x = x -> Sum xs
forall x (xs :: [*]). HasTagIn x xs => x -> Sum xs
inject x
x

-- | A type family for computing the tag of a given type in an extensible
-- sum. In practice, this means computing the first index of the given type in
-- the list.
type family TagIn (x :: k) (xs :: [k]) where
  TagIn x (x ': xs) = 0
  TagIn x (y ': xs) = 1 + TagIn x xs

-- | A class that is used for convenience in order to make certain
-- type signatures read more clearly.
class KnownNat (x `TagIn` xs) => x `HasTagIn` xs
instance KnownNat (x `TagIn` xs) => x `HasTagIn` xs

-- | Computes the tag of the given type in the given type level list.
tag :: forall x xs. x `HasTagIn` xs => Word
tag :: Word
tag = Integer -> Word
forall a. Num a => Integer -> a
fromInteger (Integer -> Word) -> Integer -> Word
forall a b. (a -> b) -> a -> b
$ Proxy (TagIn x xs) -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (TagIn x xs)
forall k (t :: k). Proxy t
Proxy @(TagIn x xs))
{-# INLINE CONLIKE tag #-}

-- | Injects a type into the extensible sum.
inject :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
inject :: x -> Sum xs
inject x
x = Word -> Any -> Sum xs
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs) (x -> Any
forall a b. a -> b
unsafeCoerce x
x)
{-# INLINE CONLIKE inject #-}

-- | Inspects an extensible sum for a particular type.
inspect :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Maybe x
inspect :: Sum xs -> Maybe x
inspect (UnsafeInj Word
tag' Any
x) = if HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
tag' then x -> Maybe x
forall a. a -> Maybe a
Just (Any -> x
forall a b. a -> b
unsafeCoerce Any
x) else Maybe x
forall a. Maybe a
Nothing
{-# INLINE CONLIKE inspect #-}

-- | A type family for deleting the given type from a list
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 a certain type, discarding it as an option if it is not the
-- correct one.
consider :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Either (Sum (Delete x xs)) x
consider :: Sum xs -> Either (Sum (Delete x xs)) x
consider (UnsafeInj Word
tag' Any
x) =
  if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs
    then x -> Either (Sum (Delete x xs)) x
forall a b. b -> Either a b
Right (Any -> x
forall a b. a -> b
unsafeCoerce Any
x)
    else Sum (Delete x xs) -> Either (Sum (Delete x xs)) x
forall a b. a -> Either a b
Left (Word -> Any -> Sum (Delete x xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (if Word
tag' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
>= HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word
tag' Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1 else Word
tag') Any
x)
{-# INLINE CONLIKE consider #-}

-- | Consider the first type in the list of possibilities, a useful
-- specialization for type inference.
considerFirst :: forall x xs. Sum (x ': xs) -> Either (Sum xs) x
considerFirst :: Sum (x : xs) -> Either (Sum xs) x
considerFirst = Sum (x : xs) -> Either (Sum xs) x
forall x (xs :: [*]).
HasTagIn x xs =>
Sum xs -> Either (Sum (Delete x xs)) x
consider
{-# INLINE CONLIKE considerFirst #-}

-- | Transforms one type in the sum into another.
inmap :: forall x y xs. (x `HasTagIn` xs, y `HasTagIn` xs) => (x -> y) -> Sum xs -> Sum xs
inmap :: (x -> y) -> Sum xs -> Sum xs
inmap x -> y
f uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) = if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word -> Any -> Sum xs
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn y xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @xs) (y -> Any
forall a b. a -> b
unsafeCoerce (x -> y
f (Any -> x
forall a b. a -> b
unsafeCoerce Any
x))) else Sum xs
uv
{-# INLINE CONLIKE inmap #-}

-- | Transform one type in one sum into another type in another sum.
smap :: forall x y xs ys. (Weaken (Delete x xs) ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys
smap :: (x -> y) -> Sum xs -> Sum ys
smap x -> y
f uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) = if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn y ys => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @ys) (y -> Any
forall a b. a -> b
unsafeCoerce (x -> y
f (Any -> x
forall a b. a -> b
unsafeCoerce Any
x))) else Sum (Delete x xs) -> Sum ys
forall (xs :: [*]) (ys :: [*]). Weaken xs ys => Sum xs -> Sum ys
weaken (Sum xs -> Sum (Delete x xs)
forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Sum (Delete x xs)
unsafeForget @x Sum xs
uv)
{-# INLINE CONLIKE smap #-}

-- | A class which checks that every type has the same tag in the first
-- list as the second. In other words, checks if the first list is a prefix
-- of the other.
class HaveSameTagsIn xs ys
instance {-# OVERLAPPABLE #-} HaveSameTagsIn '[] ys
instance {-# OVERLAPPABLE #-} HaveSameTagsIn xs ys => HaveSameTagsIn (x ': xs) (x ': ys)

-- | A free version of weakening, where all you're doing is adding
-- more possibilities at exclusively higher tags.
noOpWeaken :: forall xs ys. (xs `HaveSameTagsIn` ys) => Sum xs -> Sum ys
noOpWeaken :: Sum xs -> Sum ys
noOpWeaken = Sum xs -> Sum ys
forall a b. a -> b
unsafeCoerce
{-# INLINE CONLIKE noOpWeaken #-}

unsafeForget :: forall x xs. x `HasTagIn` xs => Sum xs -> Sum (Delete x xs)
unsafeForget :: Sum xs -> Sum (Delete x xs)
unsafeForget (UnsafeInj Word
tag' Any
x) = if Word
tag' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word -> Any -> Sum (Delete x xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
tag' Any
x
                             else if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then [Char] -> Sum (Delete x xs)
forall a. HasCallStack => [Char] -> a
error [Char]
"unsafeForget: you can't forget the truth"
                             else Word -> Any -> Sum (Delete x xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
tag' Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Any
x


unsafeForgetFirst :: Sum (x ': xs) -> Sum xs
unsafeForgetFirst :: Sum (x : xs) -> Sum xs
unsafeForgetFirst (UnsafeInj Word
tag' Any
x) = Word -> Any -> Sum xs
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
tag' Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Any
x
{-# INLINE CONLIKE unsafeForget #-}

-- | Testing extensible sums for equality.
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' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
tag'' =
        if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
          then Any -> x
forall a b. a -> b
unsafeCoerce @_ @x Any
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== Any -> x
forall a b. a -> b
unsafeCoerce @_ @x Any
x'
          else Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv Sum xs -> Sum xs -> Bool
forall a. Eq a => a -> a -> Bool
== Sum (x : xs) -> Sum xs
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
(==) = [Char] -> Sum '[] -> Sum '[] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"(==) base case: impossible by construction"

-- | Transforming one sum into a sum which contains all of the same types
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' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
      then Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn x ys => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @ys) Any
x
      else let UnsafeInj Word
tag'' Any
_ = Sum xs -> Sum ys
forall (xs :: [*]) (ys :: [*]). Weaken xs ys => Sum xs -> Sum ys
weaken @xs @ys (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv) in Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
tag'' Any
x
  {-# INLINE CONLIKE weaken #-}
instance Weaken '[] ys where
  weaken :: Sum '[] -> Sum ys
weaken = [Char] -> Sum '[] -> Sum ys
forall a. HasCallStack => [Char] -> a
error [Char]
"weaken base case: impossible by construction"
  {-# INLINE CONLIKE weaken #-}

-- | The scott encoding of an extensible sum
type family Matcher xs r :: Type where
  Matcher '[] r = r
  Matcher (x ': xs) r = (x -> r) -> Matcher xs r

-- | A typeclass for scott encoding extensible sums
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 :: Sum '[] -> Matcher '[] r
match = [Char] -> Sum '[] -> r
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 = Sum '[]
forall r. Matcher '[] r
r
  {-# INLINE CONLIKE unmatch #-}
  override :: r -> Matcher '[] r -> Matcher '[] r
override = r -> Matcher '[] r -> Matcher '[] r
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 :: 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' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
      then r -> Matcher xs r -> Matcher xs r
forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @xs @r (x -> r
f (Any -> x
forall a b. a -> b
unsafeCoerce Any
x)) (Matcher xs r -> Matcher xs r) -> Matcher xs r -> Matcher xs r
forall a b. (a -> b) -> a -> b
$ Sum xs -> Matcher xs r
forall (xs :: [*]) r. Match xs => Sum xs -> Matcher xs r
match @xs @r (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv)
      else Sum xs -> Matcher xs r
forall (xs :: [*]) r. Match xs => Sum xs -> Matcher xs r
match @xs @r (Sum (x : xs) -> Sum xs
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 (ys :: [*]). Unmatch xs ys => Matcher xs (Sum ys) -> Sum ys
forall (xs :: [*]) (ys :: [*]).
Unmatch xs ys =>
Matcher xs (Sum ys) -> Sum ys
unmatchGo @xs (Matcher xs (Sum (x : xs)) -> Sum (x : xs))
-> Matcher xs (Sum (x : xs)) -> Sum (x : xs)
forall a b. (a -> b) -> a -> b
$ (x -> Sum (x : xs)) -> Matcher xs (Sum (x : xs))
forall r. (x -> r) -> Matcher xs r
g @(Sum (x ': xs)) (Word -> Any -> Sum (x : xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
0 (Any -> Sum (x : xs)) -> (x -> Any) -> x -> Sum (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. x -> b
forall a b. a -> b
unsafeCoerce @x)
  {-# INLINE CONLIKE unmatch #-}
  override :: r -> Matcher (x : xs) r -> Matcher (x : xs) r
override r
r Matcher (x : xs) r
m = (Matcher xs r -> Matcher xs r)
-> ((x -> r) -> Matcher xs r) -> (x -> r) -> Matcher xs r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (r -> Matcher xs r -> Matcher xs r
forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @xs r
r) Matcher (x : xs) r
(x -> r) -> Matcher xs r
m
  {-# INLINE CONLIKE override #-}

-- | A utility typeclass which makes the implementation of 'Match' cleaner.
class Unmatch xs ys where
  unmatchGo :: Matcher xs (Sum ys) -> Sum ys
instance Unmatch '[] ys where
  unmatchGo :: Matcher '[] (Sum ys) -> Sum ys
unmatchGo = Matcher '[] (Sum ys) -> Sum ys
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 = Matcher xs (Sum ys) -> Sum ys
forall (xs :: [*]) (ys :: [*]).
Unmatch xs ys =>
Matcher xs (Sum ys) -> Sum ys
unmatchGo @xs (Matcher (x : xs) (Sum ys)
(x -> Sum ys) -> Matcher xs (Sum ys)
f (Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn x ys => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @ys) (Any -> Sum ys) -> (x -> Any) -> x -> Sum ys
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. x -> b
forall a b. a -> b
unsafeCoerce @x))
  {-# INLINE CONLIKE unmatchGo #-}

-- | Using functions which only require constraints which are satisfied by
-- all members of the sum.
class ForAll c xs => ApplyFunction c xs where
  apply :: (forall a. c a => a -> y) -> Sum xs -> y

instance ApplyFunction c '[] where
  apply :: (forall a. c a => a -> y) -> Sum '[] -> y
apply forall a. c a => a -> y
_f Sum '[]
x = [Char] -> y
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: empty sum"

instance (c x, ApplyFunction c xs) => ApplyFunction c (x ': xs) where
  apply :: (forall a. c a => a -> y) -> Sum (x : xs) -> y
apply forall a. c a => a -> y
f Sum (x : xs)
x = case Sum (x : xs) -> Either (Sum xs) x
forall x (xs :: [*]). Sum (x : xs) -> Either (Sum xs) x
considerFirst Sum (x : xs)
x of
    Right x
x' -> x -> y
forall a. c a => a -> y
f x
x'
    Left Sum xs
xs -> (forall a. c a => a -> y) -> Sum xs -> y
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