{-# 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
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
  , UnorderedMatch(unorderedMatch)
  , 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.Typeable (typeRep, Typeable)
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
  deriving (Typeable)

-- | Deconstruct a 'Sum' with only one variant
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 #-}

-- | 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 :: 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 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 = 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

-- | 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 :: 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

-- | 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 :: 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 #-}

-- | Injects a type into the extensible sum.
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 #-}

-- | Inspects an extensible sum for a particular type.
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 #-}

-- | 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 :: 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 #-}

-- | 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 :: 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 #-}

-- | 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 :: 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 #-}

-- | 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 :: 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 #-}

-- | 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 :: 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 #-}

-- | 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' 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

-- | Showing extensible sums.
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

-- | 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' 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)

-- | Returns the result type of the Scott encoding for the particular Sum's elements.
type family Result matcher :: Type where
  Result ((x -> r) -> matcher) = r
  Result r = r

-- | What types does this Scott encoding have in its Sum?
type family Unmatcher matcher r :: [Type] where
  Unmatcher r r = '[]
  Unmatcher ((x -> r) -> matcher) r = x ': Unmatcher matcher r

-- | 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 :: 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 #-}

-- | 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 = 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 #-}

-- | 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 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 #-}