{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeInType          #-}
{-# LANGUAGE TypeOperators       #-}

-- |
-- Module      : Data.Type.Universe.Subset
-- Copyright   : (c) Justin Le 2018
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Represent a decidable subset of a type-level collection.
--
module Data.Type.Universe.Subset (
  -- * Subset
    Subset, WitSubset(..)
  , makeSubset
  -- ** Subset manipulation
  , intersection, union, symDiff, mergeSubset, imergeSubset
  , mapSubset, imapSubset
  -- ** Subset extraction
  , subsetToList
  -- ** Subset tests
  , subsetToAny, subsetToAll, subsetToNone
  -- ** Subset construction
  , emptySubset, fullSubset
  ) where

import           Control.Applicative
import           Data.Kind
import           Data.Monoid                        (Alt(..))
import           Data.Singletons
import           Data.Singletons.Decide
import           Data.Type.Functor.Product
import           Data.Type.Predicate
import           Data.Type.Predicate.Logic
import           Data.Type.Predicate.Quantification
import           Data.Type.Universe

-- | A @'WitSubset' f p @@ as@ describes a /decidable/ subset of type-level
-- collection @as@.
newtype WitSubset f p (as :: f k) = WitSubset
    { WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset :: forall a. Elem f as a -> Decision (p @@ a)
    }

-- | A @'Subset' f p@ is a predicate that some decidable subset of an input
-- @as@ is true.
data Subset f :: (k ~> Type) -> (f k ~> Type)
type instance Apply (Subset f p) as = WitSubset f p as

instance (Universe f, Decidable p) => Decidable (Subset f p)
instance (Universe f, Decidable p) => Provable (Subset f p) where
    prove :: Sing a -> Subset f p @@ a
prove = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Subset f p @@ a
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Subset f p @@ as
makeSubset @f @_ @p (\_ -> Decidable p => Decide p
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p)

-- | Create a 'Subset' from a predicate.
makeSubset
    :: forall f k p (as :: f k). Universe f
    => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
    -> Sing as
    -> Subset f p @@ as
makeSubset :: (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Subset f p @@ as
makeSubset f :: forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)
f xs :: Sing as
xs = (forall (a :: k). Elem f as a -> Decision (p @@ a))
-> Subset f p @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Decision (p @@ a))
-> WitSubset f p as
WitSubset ((forall (a :: k). Elem f as a -> Decision (p @@ a))
 -> Subset f p @@ as)
-> (forall (a :: k). Elem f as a -> Decision (p @@ a))
-> Subset f p @@ as
forall a b. (a -> b) -> a -> b
$ \i :: Elem f as a
i -> Elem f as a -> Sing a -> Decision (p @@ a)
forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)
f Elem f as a
i (Elem f as a -> Sing as -> Sing a
forall k (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f as a
i Sing as
xs)

-- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied
-- predicates.
--
-- List is meant to include no duplicates.
subsetToList
    :: forall f p t. (Universe f, Alternative t)
    => (Subset f p --># Any f p) t
subsetToList :: (-->#) (Subset f p) (Any f p) t
subsetToList xs :: Sing a
xs s :: Subset f p @@ a
s = Alt t (WitAny f p a) -> t (Apply (Any f p) a)
forall k (f :: k -> *) (a :: k). Alt f a -> f a
getAlt (Alt t (WitAny f p a) -> t (Apply (Any f p) a))
-> Alt t (WitAny f p a) -> t (Apply (Any f p) a)
forall a b. (a -> b) -> a -> b
$ ((forall (a :: k). Elem f a a -> Sing a -> Alt t (WitAny f p a))
-> Sing a -> Alt t (WitAny f p a)
forall (f :: * -> *) k (as :: f k) m.
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
`ifoldMapSing` Sing a
xs) ((forall (a :: k). Elem f a a -> Sing a -> Alt t (WitAny f p a))
 -> Alt t (WitAny f p a))
-> (forall (a :: k). Elem f a a -> Sing a -> Alt t (WitAny f p a))
-> Alt t (WitAny f p a)
forall a b. (a -> b) -> a -> b
$ \i :: Elem f a a
i _ -> t (WitAny f p a) -> Alt t (WitAny f p a)
forall k (f :: k -> *) (a :: k). f a -> Alt f a
Alt (t (WitAny f p a) -> Alt t (WitAny f p a))
-> t (WitAny f p a) -> Alt t (WitAny f p a)
forall a b. (a -> b) -> a -> b
$ case WitSubset f p a -> Elem f a a -> Decision (p @@ a)
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ a
WitSubset f p a
s Elem f a a
i of
    Proved p :: p @@ a
p    -> WitAny f p a -> t (WitAny f p a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WitAny f p a -> t (WitAny f p a))
-> WitAny f p a -> t (WitAny f p a)
forall a b. (a -> b) -> a -> b
$ Elem f a a -> (p @@ a) -> WitAny f p a
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i p @@ a
p
    Disproved _ -> t (WitAny f p a)
forall (f :: * -> *) a. Alternative f => f a
empty

-- | Restrict a 'Subset' to a single (arbitrary) member, or fail if none
-- exists.
subsetToAny
    :: forall f p. Universe f
    => Subset f p -?> Any f p
subsetToAny :: Subset f p -?> Any f p
subsetToAny xs :: Sing a
xs s :: Subset f p @@ a
s = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (Any f p) a)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
idecideAny (\i :: Elem f a a
i _ -> WitSubset f p a -> Elem f a a -> Decision (p @@ a)
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ a
WitSubset f p a
s Elem f a a
i) Sing a
xs

-- | Construct an empty subset.
emptySubset :: forall f as. (Universe f, SingI as) => Subset f Impossible @@ as
emptySubset :: Subset f Impossible @@ as
emptySubset = Sing as -> Subset f Impossible @@ as
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @(Subset f Impossible) Sing as
forall k (a :: k). SingI a => Sing a
sing

-- | Construct a full subset
fullSubset :: forall f as. (Universe f, SingI as) => Subset f Evident @@ as
fullSubset :: Subset f Evident @@ as
fullSubset = Sing as -> Subset f Evident @@ as
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @(Subset f Evident) Sing as
forall k (a :: k). SingI a => Sing a
sing

-- | Test if a subset is empty.
subsetToNone :: forall f p. Universe f => Subset f p -?> None f p
subsetToNone :: Subset f p -?> None f p
subsetToNone xs :: Sing a
xs s :: Subset f p @@ a
s = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (None f p) a)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (None f p @@ as)
idecideNone (\i :: Elem f a a
i _ -> WitSubset f p a -> Elem f a a -> Decision (p @@ a)
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ a
WitSubset f p a
s Elem f a a
i) Sing a
xs

-- | Combine two subsets based on a decision function
imergeSubset
    :: forall f k p q r (as :: f k). ()
    => (forall a. Elem f as a -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
    -> Subset f p @@ as
    -> Subset f q @@ as
    -> Subset f r @@ as
imergeSubset :: (forall (a :: k).
 Elem f as a
 -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset f :: forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
f ps :: Subset f p @@ as
ps qs :: Subset f q @@ as
qs = (forall (a :: k). Elem f as a -> Decision (r @@ a))
-> Subset f r @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Decision (p @@ a))
-> WitSubset f p as
WitSubset ((forall (a :: k). Elem f as a -> Decision (r @@ a))
 -> Subset f r @@ as)
-> (forall (a :: k). Elem f as a -> Decision (r @@ a))
-> Subset f r @@ as
forall a b. (a -> b) -> a -> b
$ \i :: Elem f as a
i ->
    Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
f Elem f as a
i (WitSubset f p as -> Elem f as a -> Decision (p @@ a)
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ as
WitSubset f p as
ps Elem f as a
i) (WitSubset f q as -> Elem f as a -> Decision (q @@ a)
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f q @@ as
WitSubset f q as
qs Elem f as a
i)

-- | Combine two subsets based on a decision function
mergeSubset
    :: forall f k p q r (as :: f k). ()
    => (forall a. Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
    -> Subset f p @@ as
    -> Subset f q @@ as
    -> Subset f r @@ as
mergeSubset :: (forall (a :: k).
 Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
mergeSubset f :: forall (a :: k).
Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
f = (forall (a :: k).
 Elem f as a
 -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
       (as :: f k).
(forall (a :: k).
 Elem f as a
 -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset (\(_ :: Elem f as a) p :: Decision (p @@ a)
p -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
forall (a :: k).
Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
f @a Decision (p @@ a)
p)

-- | Subset intersection
intersection
    :: forall f p q. ()
    => ((Subset f p &&& Subset f q) --> Subset f (p &&& q))
intersection :: Sing a
-> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p &&& q) @@ a
intersection _ = (WitSubset f p a -> WitSubset f q a -> WitSubset f (p &&& q) a)
-> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p &&& q) @@ a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((WitSubset f p a -> WitSubset f q a -> WitSubset f (p &&& q) a)
 -> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p &&& q) @@ a)
-> (WitSubset f p a -> WitSubset f q a -> WitSubset f (p &&& q) a)
-> ((Subset f p &&& Subset f q) @@ a)
-> Subset f (p &&& q) @@ a
forall a b. (a -> b) -> a -> b
$ (forall (a :: k).
 Elem f a a
 -> Decision (p @@ a)
 -> Decision (q @@ a)
 -> Decision ((p &&& q) @@ a))
-> WitSubset f p a -> WitSubset f q a -> WitSubset f (p &&& q) a
forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
       (as :: f k).
(forall (a :: k).
 Elem f as a
 -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset ((forall (a :: k).
  Elem f a a
  -> Decision (p @@ a)
  -> Decision (q @@ a)
  -> Decision ((p &&& q) @@ a))
 -> WitSubset f p a -> WitSubset f q a -> WitSubset f (p &&& q) a)
-> (forall (a :: k).
    Elem f a a
    -> Decision (p @@ a)
    -> Decision (q @@ a)
    -> Decision ((p &&& q) @@ a))
-> WitSubset f p a
-> WitSubset f q a
-> WitSubset f (p &&& q) a
forall a b. (a -> b) -> a -> b
$ \(_ :: Elem f as a) -> Decision (Apply p a)
-> Decision (Apply q a) -> Decision (Apply (p &&& q) a)
forall k1 (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
decideAnd @p @q @a

-- | Subset union (left-biased)
union
    :: forall f p q. ()
    => ((Subset f p &&& Subset f q) --> Subset f (p ||| q))
union :: Sing a
-> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ||| q) @@ a
union _ = (WitSubset f p a -> WitSubset f q a -> WitSubset f (p ||| q) a)
-> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ||| q) @@ a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((WitSubset f p a -> WitSubset f q a -> WitSubset f (p ||| q) a)
 -> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ||| q) @@ a)
-> (WitSubset f p a -> WitSubset f q a -> WitSubset f (p ||| q) a)
-> ((Subset f p &&& Subset f q) @@ a)
-> Subset f (p ||| q) @@ a
forall a b. (a -> b) -> a -> b
$ (forall (a :: k).
 Elem f a a
 -> Decision (p @@ a)
 -> Decision (q @@ a)
 -> Decision ((p ||| q) @@ a))
-> WitSubset f p a -> WitSubset f q a -> WitSubset f (p ||| q) a
forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
       (as :: f k).
(forall (a :: k).
 Elem f as a
 -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset ((forall (a :: k).
  Elem f a a
  -> Decision (p @@ a)
  -> Decision (q @@ a)
  -> Decision ((p ||| q) @@ a))
 -> WitSubset f p a -> WitSubset f q a -> WitSubset f (p ||| q) a)
-> (forall (a :: k).
    Elem f a a
    -> Decision (p @@ a)
    -> Decision (q @@ a)
    -> Decision ((p ||| q) @@ a))
-> WitSubset f p a
-> WitSubset f q a
-> WitSubset f (p ||| q) a
forall a b. (a -> b) -> a -> b
$ \(_ :: Elem f as a) -> Decision (Apply p a)
-> Decision (Apply q a) -> Decision (Apply (p ||| q) a)
forall k1 (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
decideOr @p @q @a

-- | Symmetric subset difference
symDiff
    :: forall f p q. ()
    => ((Subset f p &&& Subset f q) --> Subset f (p ^^^ q))
symDiff :: Sing a
-> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ^^^ q) @@ a
symDiff _ = (WitSubset f p a -> WitSubset f q a -> WitSubset f (p ^^^ q) a)
-> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ^^^ q) @@ a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((WitSubset f p a -> WitSubset f q a -> WitSubset f (p ^^^ q) a)
 -> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ^^^ q) @@ a)
-> (WitSubset f p a -> WitSubset f q a -> WitSubset f (p ^^^ q) a)
-> ((Subset f p &&& Subset f q) @@ a)
-> Subset f (p ^^^ q) @@ a
forall a b. (a -> b) -> a -> b
$ (forall (a :: k).
 Elem f a a
 -> Decision (p @@ a)
 -> Decision (q @@ a)
 -> Decision ((p ^^^ q) @@ a))
-> WitSubset f p a -> WitSubset f q a -> WitSubset f (p ^^^ q) a
forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
       (as :: f k).
(forall (a :: k).
 Elem f as a
 -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset ((forall (a :: k).
  Elem f a a
  -> Decision (p @@ a)
  -> Decision (q @@ a)
  -> Decision ((p ^^^ q) @@ a))
 -> WitSubset f p a -> WitSubset f q a -> WitSubset f (p ^^^ q) a)
-> (forall (a :: k).
    Elem f a a
    -> Decision (p @@ a)
    -> Decision (q @@ a)
    -> Decision ((p ^^^ q) @@ a))
-> WitSubset f p a
-> WitSubset f q a
-> WitSubset f (p ^^^ q) a
forall a b. (a -> b) -> a -> b
$ \(_ :: Elem f as a) -> Decision (Apply p a)
-> Decision (Apply q a) -> Decision (Apply (p ^^^ q) a)
forall k1 (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a)
decideXor @p @q @a

-- | Test if a subset is equal to the entire original collection
subsetToAll
    :: forall f p. Universe f
    => Subset f p -?> All f p
subsetToAll :: Subset f p -?> All f p
subsetToAll xs :: Sing a
xs s :: Subset f p @@ a
s = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (All f p) a)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll (\i :: Elem f a a
i _ -> WitSubset f p a -> Elem f a a -> Decision (p @@ a)
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ a
WitSubset f p a
s Elem f a a
i) Sing a
xs

-- | 'mapSubset', but providing an 'Elem'.
imapSubset
    :: (forall a. Elem f as a -> p @@ a -> q @@ a)
    -> (forall a. Elem f as a -> q @@ a -> p @@ a)
    -> Subset f p @@ as
    -> Subset f q @@ as
imapSubset :: (forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a)
-> (forall (a :: k). Elem f as a -> (q @@ a) -> p @@ a)
-> (Subset f p @@ as)
-> Subset f q @@ as
imapSubset f :: forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a
f g :: forall (a :: k). Elem f as a -> (q @@ a) -> p @@ a
g s :: Subset f p @@ as
s = (forall (a :: k). Elem f as a -> Decision (q @@ a))
-> Subset f q @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Decision (p @@ a))
-> WitSubset f p as
WitSubset ((forall (a :: k). Elem f as a -> Decision (q @@ a))
 -> Subset f q @@ as)
-> (forall (a :: k). Elem f as a -> Decision (q @@ a))
-> Subset f q @@ as
forall a b. (a -> b) -> a -> b
$ \i :: Elem f as a
i ->
    (Apply p a -> Apply q a)
-> (Apply q a -> Apply p a)
-> Decision (Apply p a)
-> Decision (Apply q a)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Elem f as a -> Apply p a -> Apply q a
forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a
f Elem f as a
i) (Elem f as a -> Apply q a -> Apply p a
forall (a :: k). Elem f as a -> (q @@ a) -> p @@ a
g Elem f as a
i) (WitSubset f p as -> Elem f as a -> Decision (Apply p a)
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ as
WitSubset f p as
s Elem f as a
i)

-- | Map a bidirectional implication over a subset described by that
-- implication.
--
-- Implication needs to be bidirectional, or otherwise we can't produce
-- a /decidable/ subset as a result.
mapSubset
    :: Universe f
    => (p --> q)
    -> (q --> p)
    -> (Subset f p --> Subset f q)
mapSubset :: (p --> q) -> (q --> p) -> Subset f p --> Subset f q
mapSubset f :: p --> q
f g :: q --> p
g xs :: Sing a
xs = Sing a
-> (SingI a => WitSubset f p a -> WitSubset f q a)
-> WitSubset f p a
-> WitSubset f q a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
xs ((SingI a => WitSubset f p a -> WitSubset f q a)
 -> Apply (Subset f p) a -> Apply (Subset f q) a)
-> (SingI a => WitSubset f p a -> WitSubset f q a)
-> Apply (Subset f p) a
-> Apply (Subset f q) a
forall a b. (a -> b) -> a -> b
$
    (forall (a :: k). Elem f a a -> (p @@ a) -> q @@ a)
-> (forall (a :: k). Elem f a a -> (q @@ a) -> p @@ a)
-> Apply (Subset f p) a
-> Apply (Subset f q) a
forall k (f :: * -> *) (as :: f k) (p :: k ~> *) (q :: k ~> *).
(forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a)
-> (forall (a :: k). Elem f as a -> (q @@ a) -> p @@ a)
-> (Subset f p @@ as)
-> Subset f q @@ as
imapSubset (\i :: Elem f a a
i -> Sing a -> (p @@ a) -> q @@ a
p --> q
f (Elem f a a -> Sing a -> Sing a
forall k (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs))
               (\i :: Elem f a a
i -> Sing a -> (q @@ a) -> p @@ a
q --> p
g (Elem f a a -> Sing a -> Sing a
forall k (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs))