{-# LANGUAGE AllowAmbiguousTypes, BangPatterns, CPP, ConstraintKinds,
             DataKinds, EmptyCase, FlexibleContexts,
             FlexibleInstances, GADTs, KindSignatures,
             MultiParamTypeClasses, PolyKinds, RankNTypes,
             ScopedTypeVariables, TypeApplications, TypeOperators,
             UndecidableInstances #-}
-- | Co-records: open sum types.
--
-- Consider a record with three fields @A@, @B@, and @C@. A record is
-- a product of its fields; that is, it contains all of them: @A@,
-- @B@, /and/ @C@. If we want to talk about a value whose type is one
-- of those three types, it is /any one/ of type @A@, @B@, /or/
-- @C@. The type @CoRec '[A,B,C]@ corresponds to this sum type.
module Data.Vinyl.CoRec where
import Data.Maybe(fromJust)
import Data.Vinyl.Core
import Data.Vinyl.Lens (RElem, rget, rput, type (∈))
import Data.Vinyl.Functor (Compose(..), (:.), Identity(..), Const(..))
import Data.Vinyl.TypeLevel
import Data.Vinyl.Derived (FieldType, (:::))
import GHC.TypeLits (Symbol, KnownSymbol)
import GHC.Types (type Type)

import Unsafe.Coerce (unsafeCoerce)

-- | Generalize algebraic sum types.
data CoRec :: (k -> *) -> [k] -> * where
  CoRec :: RElem a ts (RIndex a ts) => !(f a) -> CoRec f ts

-- | A 'CoRec' constructor with better inference. If you have a label
-- that should pick out a type from the list of types that index a
-- 'CoRec', this function will help you more so than the raw 'CoRec'
-- data constructor.
corec :: forall (l :: Symbol)
                (ts :: [(Symbol,Type)])
                (f :: (Symbol,Type) -> Type).
         (KnownSymbol l, (l ::: FieldType l ts) ∈ ts)
      => f (l ::: FieldType l ts) -> CoRec f ts
corec :: f (l ::: FieldType l ts) -> CoRec f ts
corec f (l ::: FieldType l ts)
x = f (l ::: FieldType l ts) -> CoRec f ts
forall k (a :: k) (ts :: [k]) (f :: k -> *).
RElem a ts (RIndex a ts) =>
f a -> CoRec f ts
CoRec f (l ::: FieldType l ts)
x

-- | Apply a function to a 'CoRec' value. The function must accept
-- /any/ variant.
foldCoRec :: (forall a. RElem a ts (RIndex a ts) => f a -> b) -> CoRec f ts -> b
foldCoRec :: (forall (a :: k). RElem a ts (RIndex a ts) => f a -> b)
-> CoRec f ts -> b
foldCoRec forall (a :: k). RElem a ts (RIndex a ts) => f a -> b
f (CoRec f a
x) = f a -> b
forall (a :: k). RElem a ts (RIndex a ts) => f a -> b
f f a
x

-- | A Field of a 'Rec' 'Identity' is a 'CoRec' 'Identity'.
type Field = CoRec Identity

-- | A function type constructor that takes its arguments in the
-- reverse order.
newtype Op b a = Op { Op b a -> a -> b
runOp :: a -> b }

-- | Helper for writing a 'Show' instance for 'CoRec'. This lets us
-- ask for a 'Show' constraint on the type formed by applying a type
-- constructor to a type index.
class ShowF f a where
  showf :: f a -> String

instance Show (f a) => ShowF f a where
  showf :: f a -> String
showf = f a -> String
forall a. Show a => a -> String
show

instance forall f ts. RPureConstrained (ShowF f) ts => Show (CoRec f ts) where
  show :: CoRec f ts -> String
show CoRec f ts
x = String
"{|" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (forall (a :: k). (a ∈ ts, ShowF f a) => f a -> String)
-> CoRec f ts -> String
forall k k (c :: k -> Constraint) (f :: k -> *) (ts :: [k])
       (b :: k) (g :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). (a ∈ ts, c a) => f a -> g b) -> CoRec f ts -> g b
onCoRec @(ShowF f) forall (a :: k). (a ∈ ts, ShowF f a) => f a -> String
forall k (f :: k -> *) (a :: k). ShowF f a => f a -> String
showf CoRec f ts
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|}"

instance forall ts. (RecApplicative ts, RecordToList ts,
                     RApply ts, ReifyConstraint Eq Maybe ts, RMap ts)
  => Eq (CoRec Identity ts) where
  CoRec Identity ts
crA == :: CoRec Identity ts -> CoRec Identity ts -> Bool
== CoRec Identity ts
crB = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> (Rec (Const Bool) ts -> [Bool]) -> Rec (Const Bool) ts -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Const Bool) ts -> [Bool]
forall u (rs :: [u]) a. RecordToList rs => Rec (Const a) rs -> [a]
recordToList
             (Rec (Const Bool) ts -> Bool) -> Rec (Const Bool) ts -> Bool
forall a b. (a -> b) -> a -> b
$ (forall x. (:.) (Dict Eq) Maybe x -> Maybe x -> Const Bool x)
-> Rec (Dict Eq :. Maybe) ts -> Rec Maybe ts -> Rec (Const Bool) ts
forall u (xs :: [u]) (f :: u -> *) (g :: u -> *) (h :: u -> *).
(RMap xs, RApply xs) =>
(forall (x :: u). f x -> g x -> h x)
-> Rec f xs -> Rec g xs -> Rec h xs
rzipWith forall x. (:.) (Dict Eq) Maybe x -> Maybe x -> Const Bool x
f (CoRec Identity ts -> Rec (Dict Eq :. Maybe) ts
toRec CoRec Identity ts
crA) (CoRec Identity ts -> Rec Maybe ts
forall (ts :: [*]).
(RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Rec Maybe ts
coRecToRec' CoRec Identity ts
crB)
    where
      f :: forall a. (Dict Eq :. Maybe) a -> Maybe a -> Const Bool a
      f :: (:.) (Dict Eq) Maybe a -> Maybe a -> Const Bool a
f (Compose (Dict Maybe a
a)) Maybe a
b = Bool -> Const Bool a
forall k a (b :: k). a -> Const a b
Const (Bool -> Const Bool a) -> Bool -> Const Bool a
forall a b. (a -> b) -> a -> b
$ Maybe a
a Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe a
b
      toRec :: CoRec Identity ts -> Rec (Dict Eq :. Maybe) ts
toRec = forall u (c :: * -> Constraint) (f :: u -> *) (rs :: [u]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
forall (f :: * -> *) (rs :: [*]).
ReifyConstraint Eq f rs =>
Rec f rs -> Rec (Dict Eq :. f) rs
reifyConstraint @Eq (Rec Maybe ts -> Rec (Dict Eq :. Maybe) ts)
-> (CoRec Identity ts -> Rec Maybe ts)
-> CoRec Identity ts
-> Rec (Dict Eq :. Maybe) ts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoRec Identity ts -> Rec Maybe ts
forall (ts :: [*]).
(RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Rec Maybe ts
coRecToRec'

-- | We can inject a a 'CoRec' into a 'Rec' where every field of the
-- 'Rec' is 'Nothing' except for the one whose type corresponds to the
-- type of the given 'CoRec' variant.
coRecToRec :: forall f ts. RecApplicative ts
           => CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec :: CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec (CoRec f a
x) = Compose Maybe f a -> Rec (Maybe :. f) ts -> Rec (Maybe :. f) ts
forall k (r :: k) (rs :: [k]) (record :: (k -> *) -> [k] -> *)
       (f :: k -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
f r -> record f rs -> record f rs
rput (Maybe (f a) -> Compose Maybe f a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (f a -> Maybe (f a)
forall a. a -> Maybe a
Just f a
x)) ((forall (x :: u). Compose Maybe f x) -> Rec (Maybe :. f) ts
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure (Maybe (f x) -> Compose Maybe f x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose Maybe (f x)
forall a. Maybe a
Nothing))

-- | Shorthand for applying 'coRecToRec' with common functors.
coRecToRec' :: (RecApplicative ts, RMap ts)
            => CoRec Identity ts -> Rec Maybe ts
coRecToRec' :: CoRec Identity ts -> Rec Maybe ts
coRecToRec' = (forall x. (:.) Maybe Identity x -> Maybe x)
-> Rec (Maybe :. Identity) ts -> Rec Maybe ts
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap ((Identity x -> x) -> Maybe (Identity x) -> Maybe x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Identity x -> x
forall a. Identity a -> a
getIdentity (Maybe (Identity x) -> Maybe x)
-> (Compose Maybe Identity x -> Maybe (Identity x))
-> Compose Maybe Identity x
-> Maybe x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose Maybe Identity x -> Maybe (Identity x)
forall l (f :: l -> *) k (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose) (Rec (Maybe :. Identity) ts -> Rec Maybe ts)
-> (CoRec Identity ts -> Rec (Maybe :. Identity) ts)
-> CoRec Identity ts
-> Rec Maybe ts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoRec Identity ts -> Rec (Maybe :. Identity) ts
forall u (f :: u -> *) (ts :: [u]).
RecApplicative ts =>
CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec

-- | Fold a field selection function over a 'Rec'.
class FoldRec ss ts where
  foldRec :: (CoRec f ss -> CoRec f ss -> CoRec f ss)
          -> CoRec f ss
          -> Rec f ts
          -> CoRec f ss

instance FoldRec ss '[] where foldRec :: (CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f '[] -> CoRec f ss
foldRec CoRec f ss -> CoRec f ss -> CoRec f ss
_ CoRec f ss
z Rec f '[]
_ = CoRec f ss
z

instance (t ∈ ss, FoldRec ss ts) => FoldRec ss (t ': ts) where
  foldRec :: (CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f (t : ts) -> CoRec f ss
foldRec CoRec f ss -> CoRec f ss -> CoRec f ss
f CoRec f ss
z (f r
x :& Rec f rs
xs) = (CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f rs -> CoRec f ss
forall k (ss :: [k]) (ts :: [k]) (f :: k -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec CoRec f ss -> CoRec f ss -> CoRec f ss
f (CoRec f ss -> CoRec f ss -> CoRec f ss
f CoRec f ss
z (f r -> CoRec f ss
forall k (a :: k) (ts :: [k]) (f :: k -> *).
RElem a ts (RIndex a ts) =>
f a -> CoRec f ts
CoRec f r
x)) Rec f rs
xs

-- | Apply a natural transformation to a variant.
coRecMap :: (forall x. f x -> g x) -> CoRec f ts -> CoRec g ts
coRecMap :: (forall (x :: k). f x -> g x) -> CoRec f ts -> CoRec g ts
coRecMap forall (x :: k). f x -> g x
nt (CoRec f a
x) = g a -> CoRec g ts
forall k (a :: k) (ts :: [k]) (f :: k -> *).
RElem a ts (RIndex a ts) =>
f a -> CoRec f ts
CoRec (f a -> g a
forall (x :: k). f x -> g x
nt f a
x)

-- | Get a 'DictOnly' from an 'RPureConstrained' instance.
getDict :: forall c ts a proxy. (a ∈ ts, RPureConstrained c ts)
        => proxy a -> DictOnly c a
getDict :: proxy a -> DictOnly c a
getDict proxy a
_ = Rec (DictOnly c) ts -> DictOnly c a
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget @a ((forall (a :: k). c a => DictOnly c a) -> Rec (DictOnly c) ts
forall u (c :: u -> Constraint) (ts :: [u]) (f :: u -> *).
RPureConstrained c ts =>
(forall (a :: u). c a => f a) -> Rec f ts
rpureConstrained @c @ts forall (a :: k). c a => DictOnly c a
forall k (c :: k -> Constraint) (a :: k). c a => DictOnly c a
DictOnly)

-- | Like 'coRecMap', but the function mapped over the 'CoRec' can
-- have a constraint.
coRecMapC :: forall c ts f g.
             (RPureConstrained c ts)
          => (forall x. (x ∈ ts, c x) => f x -> g x)
          -> CoRec f ts
          -> CoRec g ts
coRecMapC :: (forall (x :: k). (x ∈ ts, c x) => f x -> g x)
-> CoRec f ts -> CoRec g ts
coRecMapC forall (x :: k). (x ∈ ts, c x) => f x -> g x
nt (CoRec f a
x) = case f a -> DictOnly c a
forall k (c :: k -> Constraint) (ts :: [k]) (a :: k)
       (proxy :: k -> *).
(a ∈ ts, RPureConstrained c ts) =>
proxy a -> DictOnly c a
getDict @c @ts f a
x of
                           DictOnly c a
DictOnly -> g a -> CoRec g ts
forall k (a :: k) (ts :: [k]) (f :: k -> *).
RElem a ts (RIndex a ts) =>
f a -> CoRec f ts
CoRec (f a -> g a
forall (x :: k). (x ∈ ts, c x) => f x -> g x
nt f a
x)

-- | This can be used to pull effects out of a 'CoRec'.
coRecTraverse :: Functor h
              => (forall x. f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)
coRecTraverse :: (forall (x :: k). f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)
coRecTraverse forall (x :: k). f x -> h (g x)
f (CoRec f a
x) = (g a -> CoRec g ts) -> h (g a) -> h (CoRec g ts)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g a -> CoRec g ts
forall k (a :: k) (ts :: [k]) (f :: k -> *).
RElem a ts (RIndex a ts) =>
f a -> CoRec f ts
CoRec (f a -> h (g a)
forall (x :: k). f x -> h (g x)
f f a
x)

-- | Fold a field selection function over a non-empty 'Rec'.
foldRec1 :: FoldRec (t ': ts) ts
         => (CoRec f (t ': ts) -> CoRec f (t ': ts) -> CoRec f (t ': ts))
         -> Rec f (t ': ts)
         -> CoRec f (t ': ts)
foldRec1 :: (CoRec f (t : ts) -> CoRec f (t : ts) -> CoRec f (t : ts))
-> Rec f (t : ts) -> CoRec f (t : ts)
foldRec1 CoRec f (t : ts) -> CoRec f (t : ts) -> CoRec f (t : ts)
f (f r
x :& Rec f rs
xs) = (CoRec f (t : ts) -> CoRec f (t : ts) -> CoRec f (t : ts))
-> CoRec f (t : ts) -> Rec f rs -> CoRec f (t : ts)
forall k (ss :: [k]) (ts :: [k]) (f :: k -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec CoRec f (t : ts) -> CoRec f (t : ts) -> CoRec f (t : ts)
f (f r -> CoRec f (t : ts)
forall k (a :: k) (ts :: [k]) (f :: k -> *).
RElem a ts (RIndex a ts) =>
f a -> CoRec f ts
CoRec f r
x) Rec f rs
xs

-- | Similar to 'Data.Monoid.First': find the first field that is not
-- 'Nothing'.
firstField :: FoldRec ts ts
           => Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField :: Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField Rec (Maybe :. f) ts
RNil = Maybe (CoRec f ts)
forall a. Maybe a
Nothing
firstField v :: Rec (Maybe :. f) ts
v@((:.) Maybe f r
x :& Rec (Maybe :. f) rs
_) = (forall (x :: k). (:.) Maybe f x -> Maybe (f x))
-> CoRec (Maybe :. f) (r : rs) -> Maybe (CoRec f (r : rs))
forall k (h :: * -> *) (f :: k -> *) (g :: k -> *) (ts :: [k]).
Functor h =>
(forall (x :: k). f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)
coRecTraverse forall (x :: k). (:.) Maybe f x -> Maybe (f x)
forall l (f :: l -> *) k (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose (CoRec (Maybe :. f) (r : rs) -> Maybe (CoRec f (r : rs)))
-> CoRec (Maybe :. f) (r : rs) -> Maybe (CoRec f (r : rs))
forall a b. (a -> b) -> a -> b
$ (CoRec (Maybe :. f) (r : rs)
 -> CoRec (Maybe :. f) (r : rs) -> CoRec (Maybe :. f) (r : rs))
-> CoRec (Maybe :. f) (r : rs)
-> Rec (Maybe :. f) ts
-> CoRec (Maybe :. f) (r : rs)
forall k (ss :: [k]) (ts :: [k]) (f :: k -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec CoRec (Maybe :. f) (r : rs)
-> CoRec (Maybe :. f) (r : rs) -> CoRec (Maybe :. f) (r : rs)
forall a (f :: a -> *) (t :: a) (ts :: [a]).
CoRec (Maybe :. f) (t : ts)
-> CoRec (Maybe :. f) (t : ts) -> CoRec (Maybe :. f) (t : ts)
aux ((:.) Maybe f r -> CoRec (Maybe :. f) (r : rs)
forall k (a :: k) (ts :: [k]) (f :: k -> *).
RElem a ts (RIndex a ts) =>
f a -> CoRec f ts
CoRec (:.) Maybe f r
x) Rec (Maybe :. f) ts
v
  where aux :: CoRec (Maybe :. f) (t ': ts)
            -> CoRec (Maybe :. f) (t ': ts)
            -> CoRec (Maybe :. f) (t ': ts)
        aux :: CoRec (Maybe :. f) (t : ts)
-> CoRec (Maybe :. f) (t : ts) -> CoRec (Maybe :. f) (t : ts)
aux c :: CoRec (Maybe :. f) (t : ts)
c@(CoRec (Compose (Just f a
_))) CoRec (Maybe :. f) (t : ts)
_ =  CoRec (Maybe :. f) (t : ts)
c
        aux CoRec (Maybe :. f) (t : ts)
_ CoRec (Maybe :. f) (t : ts)
c = CoRec (Maybe :. f) (t : ts)
c

-- | Similar to 'Data.Monoid.Last': find the last field that is not
-- 'Nothing'.
lastField :: FoldRec ts ts
          => Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
lastField :: Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
lastField Rec (Maybe :. f) ts
RNil = Maybe (CoRec f ts)
forall a. Maybe a
Nothing
lastField v :: Rec (Maybe :. f) ts
v@((:.) Maybe f r
x :& Rec (Maybe :. f) rs
_) = (forall (x :: k). (:.) Maybe f x -> Maybe (f x))
-> CoRec (Maybe :. f) (r : rs) -> Maybe (CoRec f (r : rs))
forall k (h :: * -> *) (f :: k -> *) (g :: k -> *) (ts :: [k]).
Functor h =>
(forall (x :: k). f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)
coRecTraverse forall (x :: k). (:.) Maybe f x -> Maybe (f x)
forall l (f :: l -> *) k (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose (CoRec (Maybe :. f) (r : rs) -> Maybe (CoRec f (r : rs)))
-> CoRec (Maybe :. f) (r : rs) -> Maybe (CoRec f (r : rs))
forall a b. (a -> b) -> a -> b
$ (CoRec (Maybe :. f) (r : rs)
 -> CoRec (Maybe :. f) (r : rs) -> CoRec (Maybe :. f) (r : rs))
-> CoRec (Maybe :. f) (r : rs)
-> Rec (Maybe :. f) ts
-> CoRec (Maybe :. f) (r : rs)
forall k (ss :: [k]) (ts :: [k]) (f :: k -> *).
FoldRec ss ts =>
(CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss -> Rec f ts -> CoRec f ss
foldRec CoRec (Maybe :. f) (r : rs)
-> CoRec (Maybe :. f) (r : rs) -> CoRec (Maybe :. f) (r : rs)
forall a (f :: a -> *) (t :: a) (ts :: [a]).
CoRec (Maybe :. f) (t : ts)
-> CoRec (Maybe :. f) (t : ts) -> CoRec (Maybe :. f) (t : ts)
aux ((:.) Maybe f r -> CoRec (Maybe :. f) (r : rs)
forall k (a :: k) (ts :: [k]) (f :: k -> *).
RElem a ts (RIndex a ts) =>
f a -> CoRec f ts
CoRec (:.) Maybe f r
x) Rec (Maybe :. f) ts
v
  where aux :: CoRec (Maybe :. f) (t ': ts)
            -> CoRec (Maybe :. f) (t ': ts)
            -> CoRec (Maybe :. f) (t ': ts)
        aux :: CoRec (Maybe :. f) (t : ts)
-> CoRec (Maybe :. f) (t : ts) -> CoRec (Maybe :. f) (t : ts)
aux CoRec (Maybe :. f) (t : ts)
_ c :: CoRec (Maybe :. f) (t : ts)
c@(CoRec (Compose (Just f a
_))) = CoRec (Maybe :. f) (t : ts)
c
        aux CoRec (Maybe :. f) (t : ts)
c CoRec (Maybe :. f) (t : ts)
_ = CoRec (Maybe :. f) (t : ts)
c

-- | Apply methods from a type class to a 'CoRec'. Intended for use
-- with @TypeApplications@, e.g. @onCoRec \@Show show r@
onCoRec :: forall c f ts b g. (RPureConstrained c ts)
        => (forall a. (a ∈ ts, c a) => f a -> g b)
        -> CoRec f ts -> g b
onCoRec :: (forall (a :: k). (a ∈ ts, c a) => f a -> g b) -> CoRec f ts -> g b
onCoRec forall (a :: k). (a ∈ ts, c a) => f a -> g b
f (CoRec f a
x) = case f a -> DictOnly c a
forall k (c :: k -> Constraint) (ts :: [k]) (a :: k)
       (proxy :: k -> *).
(a ∈ ts, RPureConstrained c ts) =>
proxy a -> DictOnly c a
getDict @c @ts f a
x of
                        DictOnly c a
DictOnly -> f a -> g b
forall (a :: k). (a ∈ ts, c a) => f a -> g b
f f a
x
{-# INLINE onCoRec #-}

-- | Apply a type class method to a 'Field'. Intended for use with
-- @TypeApplications@, e.g. @onField \@Show show r@.
onField :: forall c ts b. (RPureConstrained c ts)
        => (forall a. (a ∈ ts, c a) => a -> b)
        -> Field ts -> b
onField :: (forall a. (a ∈ ts, c a) => a -> b) -> Field ts -> b
onField forall a. (a ∈ ts, c a) => a -> b
f Field ts
x = Identity b -> b
forall a. Identity a -> a
getIdentity ((forall a. (a ∈ ts, c a) => Identity a -> Identity b)
-> Field ts -> Identity b
forall k k (c :: k -> Constraint) (f :: k -> *) (ts :: [k])
       (b :: k) (g :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). (a ∈ ts, c a) => f a -> g b) -> CoRec f ts -> g b
onCoRec @c ((a -> b) -> Identity a -> Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
forall a. (a ∈ ts, c a) => a -> b
f) Field ts
x)
{-# INLINE onField #-}

-- * Extracting values from a CoRec/Pattern matching on a CoRec

-- | Compute a runtime 'Int' index identifying the position of the
-- variant held by a @CoRec f ts@ in the type-level list @ts@.
variantIndexOf :: forall f ts. CoRec f ts -> Int
variantIndexOf :: CoRec f ts -> Int
variantIndexOf (CoRec f a
x) = f a -> Int
forall (a :: k). NatToInt (RIndex a ts) => f a -> Int
aux f a
x
  where aux :: forall a. NatToInt (RIndex a ts) => f a -> Int
        aux :: f a -> Int
aux f a
_ = NatToInt (RIndex a ts) => Int
forall (n :: Nat). NatToInt n => Int
natToInt @(RIndex a ts)
{-# INLINE variantIndexOf #-}

-- [NOTE: asA] We want to say that if @NatToInt (RIndex a ts) ~
-- NatToInt (RIndex b ts)@ then @a ~ b@ by relying on an injectivity
-- property of 'RIndex'. However, we are checking the variant index of
-- the argument at runtime, so we do not statically know that
-- extracting the variant at a particular type is safe at compile
-- time.

-- | If a 'CoRec' is a variant of the requested type, return 'Just'
-- that value; otherwise return 'Nothing'.
asA :: NatToInt (RIndex t ts) => CoRec Identity ts -> Maybe t
asA :: CoRec Identity ts -> Maybe t
asA = (Identity t -> t) -> Maybe (Identity t) -> Maybe t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Identity t -> t
forall a. Identity a -> a
getIdentity (Maybe (Identity t) -> Maybe t)
-> (CoRec Identity ts -> Maybe (Identity t))
-> CoRec Identity ts
-> Maybe t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoRec Identity ts -> Maybe (Identity t)
forall k (t :: k) (ts :: [k]) (f :: k -> *).
NatToInt (RIndex t ts) =>
CoRec f ts -> Maybe (f t)
asA'
{-# INLINE asA #-}

-- | Like 'asA', but for any interpretation functor.
asA' :: forall t ts f. (NatToInt (RIndex t ts))
     => CoRec f ts -> Maybe (f t)
asA' :: CoRec f ts -> Maybe (f t)
asA' f :: CoRec f ts
f@(CoRec f a
x)
  | CoRec f ts -> Int
forall k (f :: k -> *) (ts :: [k]). CoRec f ts -> Int
variantIndexOf CoRec f ts
f Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== NatToInt (RIndex t ts) => Int
forall (n :: Nat). NatToInt n => Int
natToInt @(RIndex t ts) = f t -> Maybe (f t)
forall a. a -> Maybe a
Just (f a -> f t
forall a b. a -> b
unsafeCoerce f a
x)
  | Bool
otherwise = Maybe (f t)
forall a. Maybe a
Nothing
{-# INLINE asA' #-}

-- | Pattern match on a CoRec by specifying handlers for each case. Note that
-- the order of the Handlers has to match the type level list (t:ts).
--
-- >>> :{
-- let testCoRec = Col (Identity False) :: CoRec Identity [Int, String, Bool] in
-- match testCoRec $
--       (H $ \i -> "my Int is the successor of " ++ show (i - 1))
--    :& (H $ \s -> "my String is: " ++ s)
--    :& (H $ \b -> "my Bool is not: " ++ show (not b) ++ " thus it is " ++ show b)
--    :& RNil
-- :}
-- "my Bool is not: True thus it is False"
match :: forall ts b. CoRec Identity ts -> Handlers ts b -> b
match :: CoRec Identity ts -> Handlers ts b -> b
match (CoRec (Identity a
t)) Handlers ts b
hs = a -> b
forall a. RElem a ts (RIndex a ts) => a -> b
aux a
t
  where aux :: forall a. RElem a ts (RIndex a ts) => a -> b
        aux :: a -> b
aux a
x = case Handlers ts b -> Handler b a
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget @a Handlers ts b
hs of
                  H a -> b
f -> a -> b
f a
x

-- | Helper for handling a variant of a 'CoRec': either the function
-- is applied to the variant or the type of the 'CoRec' is refined to
-- reflect the fact that the variant is /not/ compatible with the type
-- of the would-be handler.
class RIndex t ts ~ i => Match1 t ts i where
  match1' :: Handler r t -> Rec Maybe ts -> Either r (Rec Maybe (RDelete t ts))

instance Match1 t (t ': ts) 'Z where
  match1' :: Handler r t
-> Rec Maybe (t : ts) -> Either r (Rec Maybe (RDelete t (t : ts)))
match1' Handler r t
_ (Maybe r
Nothing :& Rec Maybe rs
xs) = Rec Maybe rs -> Either r (Rec Maybe rs)
forall a b. b -> Either a b
Right Rec Maybe rs
xs
  match1' (H t -> r
h) (Just r
x :& Rec Maybe rs
_) = r -> Either r (Rec Maybe ts)
forall a b. a -> Either a b
Left (t -> r
h t
r
x)

instance (Match1 t ts i, RIndex t (s ': ts) ~ 'S i,
          RDelete t (s ': ts) ~ (s ': RDelete t ts))
         => Match1 t (s ': ts) ('S i) where
  match1' :: Handler r t
-> Rec Maybe (s : ts) -> Either r (Rec Maybe (RDelete t (s : ts)))
match1' Handler r t
h (Maybe r
x :& Rec Maybe rs
xs) = (Maybe r
x Maybe r -> Rec Maybe (RDelete t ts) -> Rec Maybe (r : RDelete t ts)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:&) (Rec Maybe (RDelete t ts) -> Rec Maybe (r : RDelete t ts))
-> Either r (Rec Maybe (RDelete t ts))
-> Either r (Rec Maybe (r : RDelete t ts))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Handler r t -> Rec Maybe rs -> Either r (Rec Maybe (RDelete t rs))
forall t (ts :: [*]) (i :: Nat) r.
Match1 t ts i =>
Handler r t -> Rec Maybe ts -> Either r (Rec Maybe (RDelete t ts))
match1' Handler r t
h Rec Maybe rs
xs

-- | Handle a single variant of a 'CoRec': either the function is
-- applied to the variant or the type of the 'CoRec' is refined to
-- reflect the fact that the variant is /not/ compatible with the type
-- of the would-be handler
match1 :: (Match1 t ts (RIndex t ts),
           RecApplicative ts,
           RMap ts, RMap (RDelete t ts),
           FoldRec (RDelete t ts) (RDelete t ts))
       => Handler r t
       -> CoRec Identity ts
       -> Either r (CoRec Identity (RDelete t ts))
match1 :: Handler r t
-> CoRec Identity ts -> Either r (CoRec Identity (RDelete t ts))
match1 Handler r t
h = (Rec Maybe (RDelete t ts) -> CoRec Identity (RDelete t ts))
-> Either r (Rec Maybe (RDelete t ts))
-> Either r (CoRec Identity (RDelete t ts))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Maybe (CoRec Identity (RDelete t ts))
-> CoRec Identity (RDelete t ts)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (CoRec Identity (RDelete t ts))
 -> CoRec Identity (RDelete t ts))
-> (Rec Maybe (RDelete t ts)
    -> Maybe (CoRec Identity (RDelete t ts)))
-> Rec Maybe (RDelete t ts)
-> CoRec Identity (RDelete t ts)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Maybe :. Identity) (RDelete t ts)
-> Maybe (CoRec Identity (RDelete t ts))
forall k (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField (Rec (Maybe :. Identity) (RDelete t ts)
 -> Maybe (CoRec Identity (RDelete t ts)))
-> (Rec Maybe (RDelete t ts)
    -> Rec (Maybe :. Identity) (RDelete t ts))
-> Rec Maybe (RDelete t ts)
-> Maybe (CoRec Identity (RDelete t ts))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. Maybe x -> (:.) Maybe Identity x)
-> Rec Maybe (RDelete t ts)
-> Rec (Maybe :. Identity) (RDelete t ts)
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (Maybe (Identity x) -> Compose Maybe Identity x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (Maybe (Identity x) -> Compose Maybe Identity x)
-> (Maybe x -> Maybe (Identity x))
-> Maybe x
-> Compose Maybe Identity x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> Identity x) -> Maybe x -> Maybe (Identity x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> Identity x
forall a. a -> Identity a
Identity))
         (Either r (Rec Maybe (RDelete t ts))
 -> Either r (CoRec Identity (RDelete t ts)))
-> (CoRec Identity ts -> Either r (Rec Maybe (RDelete t ts)))
-> CoRec Identity ts
-> Either r (CoRec Identity (RDelete t ts))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handler r t -> Rec Maybe ts -> Either r (Rec Maybe (RDelete t ts))
forall t (ts :: [*]) (i :: Nat) r.
Match1 t ts i =>
Handler r t -> Rec Maybe ts -> Either r (Rec Maybe (RDelete t ts))
match1' Handler r t
h
         (Rec Maybe ts -> Either r (Rec Maybe (RDelete t ts)))
-> (CoRec Identity ts -> Rec Maybe ts)
-> CoRec Identity ts
-> Either r (Rec Maybe (RDelete t ts))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoRec Identity ts -> Rec Maybe ts
forall (ts :: [*]).
(RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Rec Maybe ts
coRecToRec'

matchNil :: CoRec f '[] -> r
matchNil :: CoRec f '[] -> r
matchNil (CoRec f a
x) = case f a
x of f a
_ -> String -> r
forall a. HasCallStack => String -> a
error String
"matchNil: impossible"

-- | Newtype around functions for a to b
newtype Handler b a = H (a -> b)

-- | 'Handlers ts b', is essentially a list of functions, one for each type in
-- ts. All functions produce a value of type 'b'. Hence, 'Handlers ts b' would
-- represent something like the type-level list: [t -> b | t \in ts ]
type Handlers ts b = Rec (Handler b) ts

-- | A 'CoRec' is either the first possible variant indicated by its
-- type, or a 'CoRec' that must be one of the remaining types.
restrictCoRec :: forall t ts f. (RecApplicative ts, FoldRec ts ts)
              => CoRec f (t ': ts) -> Either (f t) (CoRec f ts)
restrictCoRec :: CoRec f (t : ts) -> Either (f t) (CoRec f ts)
restrictCoRec CoRec f (t : ts)
r = Either (f t) (CoRec f ts)
-> (f t -> Either (f t) (CoRec f ts))
-> Maybe (f t)
-> Either (f t) (CoRec f ts)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (CoRec f ts -> Either (f t) (CoRec f ts)
forall a b. b -> Either a b
Right (CoRec f (t : ts) -> CoRec f ts
forall a b. a -> b
unsafeCoerce CoRec f (t : ts)
r)) f t -> Either (f t) (CoRec f ts)
forall a b. a -> Either a b
Left (CoRec f (t : ts) -> Maybe (f t)
forall k (t :: k) (ts :: [k]) (f :: k -> *).
NatToInt (RIndex t ts) =>
CoRec f ts -> Maybe (f t)
asA' @t CoRec f (t : ts)
r)
{-# INLINE restrictCoRec #-}

-- | A 'CoRec' whose possible types are @ts@ may be used at a type of
-- 'CoRec' whose possible types are @t:ts@.
weakenCoRec :: (RecApplicative ts, FoldRec (t ': ts) (t ': ts))
            => CoRec f ts -> CoRec f (t ': ts)
weakenCoRec :: CoRec f ts -> CoRec f (t : ts)
weakenCoRec = Maybe (CoRec f (t : ts)) -> CoRec f (t : ts)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (CoRec f (t : ts)) -> CoRec f (t : ts))
-> (CoRec f ts -> Maybe (CoRec f (t : ts)))
-> CoRec f ts
-> CoRec f (t : ts)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Maybe :. f) (t : ts) -> Maybe (CoRec f (t : ts))
forall k (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField (Rec (Maybe :. f) (t : ts) -> Maybe (CoRec f (t : ts)))
-> (CoRec f ts -> Rec (Maybe :. f) (t : ts))
-> CoRec f ts
-> Maybe (CoRec f (t : ts))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (f t) -> Compose Maybe f t
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose Maybe (f t)
forall a. Maybe a
Nothing Compose Maybe f t
-> Rec (Maybe :. f) ts -> Rec (Maybe :. f) (t : ts)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:&) (Rec (Maybe :. f) ts -> Rec (Maybe :. f) (t : ts))
-> (CoRec f ts -> Rec (Maybe :. f) ts)
-> CoRec f ts
-> Rec (Maybe :. f) (t : ts)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoRec f ts -> Rec (Maybe :. f) ts
forall u (f :: u -> *) (ts :: [u]).
RecApplicative ts =>
CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec

-- * Safe Variants

-- | A 'CoRec' is either the first possible variant indicated by its
-- type, or a 'CoRec' that must be one of the remaining types. The
-- safety is related to that of 'asASafe'.
restrictCoRecSafe :: forall t ts f. (RecApplicative ts, FoldRec ts ts)
                  => CoRec f (t ': ts) -> Either (f t) (CoRec f ts)
restrictCoRecSafe :: CoRec f (t : ts) -> Either (f t) (CoRec f ts)
restrictCoRecSafe = Rec (Maybe :. f) (t : ts) -> Either (f t) (CoRec f ts)
go (Rec (Maybe :. f) (t : ts) -> Either (f t) (CoRec f ts))
-> (CoRec f (t : ts) -> Rec (Maybe :. f) (t : ts))
-> CoRec f (t : ts)
-> Either (f t) (CoRec f ts)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoRec f (t : ts) -> Rec (Maybe :. f) (t : ts)
forall u (f :: u -> *) (ts :: [u]).
RecApplicative ts =>
CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec
  where go :: Rec (Maybe :. f) (t ': ts) -> Either (f t) (CoRec f ts)
        go :: Rec (Maybe :. f) (t : ts) -> Either (f t) (CoRec f ts)
go (Compose Maybe (f r)
Nothing :& Rec (Maybe :. f) rs
xs) = CoRec f rs -> Either (f t) (CoRec f rs)
forall a b. b -> Either a b
Right (Maybe (CoRec f rs) -> CoRec f rs
forall a. HasCallStack => Maybe a -> a
fromJust (Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
forall k (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField Rec (Maybe :. f) rs
xs))
        go (Compose (Just f r
x) :& Rec (Maybe :. f) rs
_) = f r -> Either (f r) (CoRec f ts)
forall a b. a -> Either a b
Left f r
x

-- | Like 'asA', but implemented more safely and typically slower.
asASafe :: (t ∈ ts, RecApplicative ts, RMap ts)
        => CoRec Identity ts -> Maybe t
asASafe :: CoRec Identity ts -> Maybe t
asASafe c :: CoRec Identity ts
c@(CoRec Identity a
_) = Rec Maybe ts -> Maybe t
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget (Rec Maybe ts -> Maybe t) -> Rec Maybe ts -> Maybe t
forall a b. (a -> b) -> a -> b
$ CoRec Identity ts -> Rec Maybe ts
forall (ts :: [*]).
(RecApplicative ts, RMap ts) =>
CoRec Identity ts -> Rec Maybe ts
coRecToRec' CoRec Identity ts
c

-- | Like 'asASafe', but for any interpretation functor.
asA'Safe :: (t ∈ ts, RecApplicative ts, RMap ts)
         => CoRec f ts -> (Maybe :. f) t
asA'Safe :: CoRec f ts -> (:.) Maybe f t
asA'Safe c :: CoRec f ts
c@(CoRec f a
_) = Rec (Maybe :. f) ts -> (:.) Maybe f t
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget (Rec (Maybe :. f) ts -> (:.) Maybe f t)
-> Rec (Maybe :. f) ts -> (:.) Maybe f t
forall a b. (a -> b) -> a -> b
$ CoRec f ts -> Rec (Maybe :. f) ts
forall u (f :: u -> *) (ts :: [u]).
RecApplicative ts =>
CoRec f ts -> Rec (Maybe :. f) ts
coRecToRec CoRec f ts
c