{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Predicate.Auto (
Auto (..),
autoTC,
AutoNot,
autoNot,
autoAny,
autoNotAll,
AutoProvable,
AutoElem (..),
AutoAll (..),
) where
import Data.Functor.Identity
import Data.List.NonEmpty (NonEmpty (..))
import Data.Singletons
import Data.Singletons.Sigma
import Data.Type.Equality
import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Type.Predicate.Param
import Data.Type.Predicate.Quantification
import Data.Type.Universe
class Auto (p :: Predicate k) (a :: k) where
auto :: p @@ a
autoTC :: forall t a. Auto (TyPred t) a => t a
autoTC :: forall {k} (t :: k -> *) (a :: k). Auto (TyPred t) a => t a
autoTC = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(TyPred t) @a
instance SingI a => Auto Evident a where
auto :: Evident @@ a
auto = Sing a
Evident @@ a
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI a => Auto (Not Impossible) a where
auto :: Not Impossible @@ a
auto = ((Sing a -> Void) -> Sing a -> Void
forall a b. (a -> b) -> a -> b
$ Sing a
forall {k} (a :: k). SingI a => Sing a
sing)
instance Auto (EqualTo a) a where
auto :: EqualTo a @@ a
auto = a :~: a
EqualTo a @@ a
forall {k} (a :: k). a :~: a
Refl
instance (Auto p a, Auto q a) => Auto (p &&& q) a where
auto :: (p &&& q) @@ a
auto = (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a, forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @q @a)
instance Auto q a => Auto (p ==> q) a where
auto :: (p ==> q) @@ a
auto Apply p a
_ = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @q @a
data AutoProvable :: Predicate k -> Predicate k
type instance Apply (AutoProvable p) a = p @@ a
instance (Provable p, SingI a) => Auto (AutoProvable p) a where
auto :: AutoProvable p @@ a
auto = forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k ~> *). Provable p => Prove p
prove @p @a Sing a
forall {k} (a :: k). SingI a => Sing a
sing
class AutoElem f (as :: f k) (a :: k) where
autoElem :: Elem f as a
instance {-# OVERLAPPING #-} AutoElem [] (a ': as) a where
autoElem :: Elem [] (a : as) a
autoElem = Index (a : as) a
Elem [] (a : as) a
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
instance {-# OVERLAPPING #-} AutoElem [] as a => AutoElem [] (b ': as) a where
autoElem :: Elem [] (b : as) a
autoElem = Index as a -> Index (b : as) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Index as a
Elem [] as a
forall k (f :: * -> *) (as :: f k) (a :: k).
AutoElem f as a =>
Elem f as a
autoElem
instance AutoElem Maybe ('Just a) a where
autoElem :: Elem Maybe ('Just a) a
autoElem = IJust ('Just a) a
Elem Maybe ('Just a) a
forall {k} (b :: k). IJust ('Just b) b
IJust
instance AutoElem (Either j) ('Right a) a where
autoElem :: Elem (Either j) ('Right a) a
autoElem = IRight ('Right a) a
Elem (Either j) ('Right a) a
forall {k} {j} (b :: k). IRight ('Right b) b
IRight
instance AutoElem NonEmpty (a ':| as) a where
autoElem :: Elem NonEmpty (a ':| as) a
autoElem = NEIndex (a ':| as) a
Elem NonEmpty (a ':| as) a
forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead
instance AutoElem [] as a => AutoElem NonEmpty (b ':| as) a where
autoElem :: Elem NonEmpty (b ':| as) a
autoElem = Index as a -> NEIndex (b ':| as) a
forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail Index as a
Elem [] as a
forall k (f :: * -> *) (as :: f k) (a :: k).
AutoElem f as a =>
Elem f as a
autoElem
instance AutoElem ((,) j) '(w, a) a where
autoElem :: Elem ((,) j) '(w, a) a
autoElem = ISnd '(w, a) a
Elem ((,) j) '(w, a) a
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd
instance AutoElem Identity ('Identity a) a where
autoElem :: Elem Identity ('Identity a) a
autoElem = IIdentity ('Identity a) a
Elem Identity ('Identity a) a
forall {k} (b :: k). IIdentity ('Identity b) b
IId
instance AutoElem f as a => Auto (In f as) a where
auto :: In f as @@ a
auto = forall k (f :: * -> *) (as :: f k) (a :: k).
AutoElem f as a =>
Elem f as a
autoElem @_ @f @as @a
class AutoAll f (p :: Predicate k) (as :: f k) where
autoAll :: All f p @@ as
instance AutoAll [] p '[] where
autoAll :: All [] p @@ '[]
autoAll = (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[]
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[])
-> (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[]
forall a b. (a -> b) -> a -> b
$ \case {}
instance (Auto p a, AutoAll [] p as) => AutoAll [] p (a ': as) where
autoAll :: All [] p @@ (a : as)
autoAll = (forall (a :: a). Elem [] (a : as) a -> p @@ a)
-> WitAll [] p (a : as)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: a). Elem [] (a : as) a -> p @@ a)
-> WitAll [] p (a : as))
-> (forall (a :: a). Elem [] (a : as) a -> p @@ a)
-> WitAll [] p (a : as)
forall a b. (a -> b) -> a -> b
$ \case
Index (a : as) a
Elem [] (a : as) a
IZ -> forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
IS Index bs a
i -> WitAll [] p as -> forall (a :: a). Elem [] as a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll (forall k (f :: * -> *) (p :: Predicate k) (as :: f k).
AutoAll f p as =>
All f p @@ as
autoAll @_ @[] @p @as) Index bs a
Elem [] as a
i
instance AutoAll Maybe p 'Nothing where
autoAll :: All Maybe p @@ 'Nothing
autoAll = (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing)
-> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing
forall a b. (a -> b) -> a -> b
$ \case {}
instance Auto p a => AutoAll Maybe p ('Just a) where
autoAll :: All Maybe p @@ 'Just a
autoAll = (forall (a :: a). Elem Maybe ('Just a) a -> p @@ a)
-> WitAll Maybe p ('Just a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: a). Elem Maybe ('Just a) a -> p @@ a)
-> WitAll Maybe p ('Just a))
-> (forall (a :: a). Elem Maybe ('Just a) a -> p @@ a)
-> WitAll Maybe p ('Just a)
forall a b. (a -> b) -> a -> b
$ \case IJust ('Just a) a
Elem Maybe ('Just a) a
IJust -> forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
instance AutoAll (Either j) p ('Left e) where
autoAll :: All (Either j) p @@ 'Left e
autoAll = (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> WitAll (Either j) p ('Left e)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> WitAll (Either j) p ('Left e))
-> (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> WitAll (Either j) p ('Left e)
forall a b. (a -> b) -> a -> b
$ \case {}
instance Auto p a => AutoAll (Either j) p ('Right a) where
autoAll :: All (Either j) p @@ 'Right a
autoAll = (forall (a :: b). Elem (Either j) ('Right a) a -> p @@ a)
-> WitAll (Either j) p ('Right a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: b). Elem (Either j) ('Right a) a -> p @@ a)
-> WitAll (Either j) p ('Right a))
-> (forall (a :: b). Elem (Either j) ('Right a) a -> p @@ a)
-> WitAll (Either j) p ('Right a)
forall a b. (a -> b) -> a -> b
$ \case IRight ('Right a) a
Elem (Either j) ('Right a) a
IRight -> forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
instance (Auto p a, AutoAll [] p as) => AutoAll NonEmpty p (a ':| as) where
autoAll :: All NonEmpty p @@ (a ':| as)
autoAll = (forall (a :: a). Elem NonEmpty (a ':| as) a -> p @@ a)
-> WitAll NonEmpty p (a ':| as)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: a). Elem NonEmpty (a ':| as) a -> p @@ a)
-> WitAll NonEmpty p (a ':| as))
-> (forall (a :: a). Elem NonEmpty (a ':| as) a -> p @@ a)
-> WitAll NonEmpty p (a ':| as)
forall a b. (a -> b) -> a -> b
$ \case
NEIndex (a ':| as) a
Elem NonEmpty (a ':| as) a
NEHead -> forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
NETail Index as a
i -> WitAll [] p as -> forall (a :: a). Elem [] as a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll (forall k (f :: * -> *) (p :: Predicate k) (as :: f k).
AutoAll f p as =>
All f p @@ as
autoAll @_ @[] @p @as) Index as a
Elem [] as a
i
instance Auto p a => AutoAll ((,) j) p '(w, a) where
autoAll :: All ((,) j) p @@ '(w, a)
autoAll = (forall (a :: k). Elem ((,) j) '(w, a) a -> p @@ a)
-> WitAll ((,) j) p '(w, a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem ((,) j) '(w, a) a -> p @@ a)
-> WitAll ((,) j) p '(w, a))
-> (forall (a :: k). Elem ((,) j) '(w, a) a -> p @@ a)
-> WitAll ((,) j) p '(w, a)
forall a b. (a -> b) -> a -> b
$ \case ISnd '(w, a) a
Elem ((,) j) '(w, a) a
ISnd -> forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
instance Auto p a => AutoAll Identity p ('Identity a) where
autoAll :: All Identity p @@ 'Identity a
autoAll = (forall (a :: a). Elem Identity ('Identity a) a -> p @@ a)
-> WitAll Identity p ('Identity a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: a). Elem Identity ('Identity a) a -> p @@ a)
-> WitAll Identity p ('Identity a))
-> (forall (a :: a). Elem Identity ('Identity a) a -> p @@ a)
-> WitAll Identity p ('Identity a)
forall a b. (a -> b) -> a -> b
$ \case IIdentity ('Identity a) a
Elem Identity ('Identity a) a
IId -> forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
instance AutoAll f p as => Auto (All f p) as where
auto :: All f p @@ as
auto = forall k (f :: * -> *) (p :: Predicate k) (as :: f k).
AutoAll f p as =>
All f p @@ as
autoAll @_ @f @p @as
instance SingI a => Auto (NotNull []) (a ': as) where
auto :: NotNull [] @@ (a : as)
auto = Elem [] (a : as) a -> (Evident @@ a) -> WitAny [] Evident (a : as)
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Index (a : as) a
Elem [] (a : as) a
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ Sing a
Evident @@ a
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI a => Auto IsJust ('Just a) where
auto :: IsJust @@ 'Just a
auto = Elem Maybe ('Just a) a
-> (Evident @@ a) -> WitAny Maybe Evident ('Just a)
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny IJust ('Just a) a
Elem Maybe ('Just a) a
forall {k} (b :: k). IJust ('Just b) b
IJust Sing a
Evident @@ a
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI a => Auto IsRight ('Right a) where
auto :: IsRight @@ 'Right a
auto = Elem (Either j) ('Right a) a
-> (Evident @@ a) -> WitAny (Either j) Evident ('Right a)
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny IRight ('Right a) a
Elem (Either j) ('Right a) a
forall {k} {j} (b :: k). IRight ('Right b) b
IRight Sing a
Evident @@ a
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where
auto :: NotNull NonEmpty @@ (a ':| as)
auto = Elem NonEmpty (a ':| as) a
-> (Evident @@ a) -> WitAny NonEmpty Evident (a ':| as)
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny NEIndex (a ':| as) a
Elem NonEmpty (a ':| as) a
forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead Sing a
Evident @@ a
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI a => Auto (NotNull ((,) j)) '(w, a) where
auto :: NotNull ((,) j) @@ '(w, a)
auto = Elem ((,) j) '(w, a) a
-> (Evident @@ a) -> WitAny ((,) j) Evident '(w, a)
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny ISnd '(w, a) a
Elem ((,) j) '(w, a) a
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd Sing a
Evident @@ a
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI a => Auto (NotNull Identity) ('Identity a) where
auto :: NotNull Identity @@ 'Identity a
auto = Elem Identity ('Identity a) a
-> (Evident @@ a) -> WitAny Identity Evident ('Identity a)
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny IIdentity ('Identity a) a
Elem Identity ('Identity a) a
forall {k} (b :: k). IIdentity ('Identity b) b
IId Sing a
Evident @@ a
forall {k} (a :: k). SingI a => Sing a
sing
type AutoNot (p :: Predicate k) = Auto (Not p)
autoNot :: forall k (p :: Predicate k) (a :: k). AutoNot p a => Not p @@ a
autoNot :: forall k (p :: Predicate k) (a :: k). AutoNot p a => Not p @@ a
autoNot = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @k @(Not p) @a
instance Auto (Found p) (f @@ a) => Auto (Found (PPMap f p)) a where
auto :: Found (PPMap f p) @@ a
auto = case forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(Found p) @(f @@ a) of
Sing fst
i :&: p (f @@ a) @@ fst
p -> Sing fst
i Sing fst -> (PPMap f p a @@ fst) -> Sigma v (PPMap f p a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: p (f @@ a) @@ fst
PPMap f p a @@ fst
p
instance Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p)) a where
auto :: NotFound (PPMap f p) @@ a
auto =
(Sigma v (PPMap f p a) -> Σ v (p (f @@ a)))
-> Refuted (Σ v (p (f @@ a))) -> Refuted (Sigma v (PPMap f p a))
forall a b. (a -> b) -> Refuted b -> Refuted a
mapRefuted (\(Sing fst
i :&: PPMap f p a @@ fst
p) -> Sing fst
i Sing fst -> (p (f @@ a) @@ fst) -> Σ v (p (f @@ a))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: p (f @@ a) @@ fst
PPMap f p a @@ fst
p) (Refuted (Σ v (p (f @@ a))) -> Refuted (Sigma v (PPMap f p a)))
-> Refuted (Σ v (p (f @@ a))) -> Refuted (Sigma v (PPMap f p a))
forall a b. (a -> b) -> a -> b
$
forall k (p :: Predicate k) (a :: k). AutoNot p a => Not p @@ a
autoNot @_ @(Found p) @(f @@ a)
instance Auto p (f @@ a) => Auto (PMap f p) a where
auto :: PMap f p @@ a
auto = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @(f @@ a)
instance AutoNot p (f @@ a) => Auto (Not (PMap f p)) a where
auto :: Not (PMap f p) @@ a
auto = forall k (p :: Predicate k) (a :: k). AutoNot p a => Not p @@ a
autoNot @_ @p @(f @@ a)
autoAny ::
forall f p as a.
Auto p a =>
Elem f as a ->
Any f p @@ as
autoAny :: forall {k} (f :: * -> *) (p :: Predicate k) (as :: f k) (a :: k).
Auto p a =>
Elem f as a -> Any f p @@ as
autoAny Elem f as a
i = Elem f as a -> (p @@ a) -> WitAny f p as
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f as a
i (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a)
instance (SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p)) as where
auto :: Not (Any f p) @@ as
auto = Sing as -> (All f (Not p) @@ as) -> Not (Any f p) @@ as
forall {k} (f :: * -> *) (p :: Predicate k) (a :: f k).
Sing a -> (All f (Not p) @@ a) -> None f p @@ a
allNotNone Sing as
forall {k} (a :: k). SingI a => Sing a
sing ((All f (Not p) @@ as) -> Not (Any f p) @@ as)
-> (All f (Not p) @@ as) -> Not (Any f p) @@ as
forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: Predicate k) (as :: f k).
AutoAll f p as =>
All f p @@ as
autoAll @_ @f @(Not p) @as
autoNotAll ::
forall p f as a.
(AutoNot p a, SingI as) =>
Elem f as a ->
Not (All f p) @@ as
autoNotAll :: forall {k} (p :: Predicate k) (f :: * -> *) (as :: f k) (a :: k).
(AutoNot p a, SingI as) =>
Elem f as a -> Not (All f p) @@ as
autoNotAll = Sing as -> (Any f (Not p) @@ as) -> Apply (Not (All f p)) as
forall {k} (f :: * -> *) (p :: Predicate k) (a :: f k).
Sing a -> (Any f (Not p) @@ a) -> NotAll f p @@ a
anyNotNotAll Sing as
forall {k} (a :: k). SingI a => Sing a
sing (WitAny f (Not p) as -> WitAll f p as -> Void)
-> (Elem f as a -> WitAny f (Not p) as)
-> Elem f as a
-> WitAll f p as
-> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elem f as a -> Any f (Not p) @@ as
Elem f as a -> WitAny f (Not p) as
forall {k} (f :: * -> *) (p :: Predicate k) (as :: f k) (a :: k).
Auto p a =>
Elem f as a -> Any f p @@ as
autoAny
instance (SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p))) as where
auto :: Not (Found (AnyMatch f p)) @@ as
auto =
(Sigma v (AnyMatch f p as) -> WitAny f (Found p) as)
-> Refuted (WitAny f (Found p) as)
-> Refuted (Sigma v (AnyMatch f p as))
forall a b. (a -> b) -> Refuted b -> Refuted a
mapRefuted (\(Sing fst
s :&: WitAny Elem f as a1
i FlipPP p fst @@ a1
p) -> Elem f as a1 -> (Found p @@ a1) -> WitAny f (Found p) as
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f as a1
i (Sing fst
s Sing fst -> (p a1 @@ fst) -> Sigma v (p a1)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: FlipPP p fst @@ a1
p a1 @@ fst
p)) (Refuted (WitAny f (Found p) as)
-> Refuted (Sigma v (AnyMatch f p as)))
-> Refuted (WitAny f (Found p) as)
-> Refuted (Sigma v (AnyMatch f p as))
forall a b. (a -> b) -> a -> b
$
forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(Not (Any f (Found p))) @as
instance SingI as => Auto (TyPred (Rec WrappedSing)) as where
auto :: TyPred (Rec WrappedSing) @@ as
auto = Sing as -> Rec WrappedSing as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI as => Auto (TyPred (PMaybe WrappedSing)) as where
auto :: TyPred (PMaybe WrappedSing) @@ as
auto = Sing as -> PMaybe WrappedSing as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI as => Auto (TyPred (NERec WrappedSing)) as where
auto :: TyPred (NERec WrappedSing) @@ as
auto = Sing as -> NERec WrappedSing as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI as => Auto (TyPred (PEither WrappedSing)) as where
auto :: TyPred (PEither WrappedSing) @@ as
auto = Sing as -> PEither WrappedSing as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI as => Auto (TyPred (PTup WrappedSing)) as where
auto :: TyPred (PTup WrappedSing) @@ as
auto = Sing as -> PTup WrappedSing as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI as => Auto (TyPred (PIdentity WrappedSing)) as where
auto :: TyPred (PIdentity WrappedSing) @@ as
auto = Sing as -> PIdentity WrappedSing as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance (SingI as, Provable p) => Auto (TyPred (Rec (Wit p))) as where
auto :: TyPred (Rec (Wit p)) @@ as
auto = Sing as -> Rec (Wit p) as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance (SingI as, Provable p) => Auto (TyPred (PMaybe (Wit p))) as where
auto :: TyPred (PMaybe (Wit p)) @@ as
auto = Sing as -> PMaybe (Wit p) as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance (SingI as, Provable p) => Auto (TyPred (NERec (Wit p))) as where
auto :: TyPred (NERec (Wit p)) @@ as
auto = Sing as -> NERec (Wit p) as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance (SingI as, Provable p) => Auto (TyPred (PEither (Wit p))) as where
auto :: TyPred (PEither (Wit p)) @@ as
auto = Sing as -> PEither (Wit p) as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance (SingI as, Provable p) => Auto (TyPred (PTup (Wit p))) as where
auto :: TyPred (PTup (Wit p)) @@ as
auto = Sing as -> PTup (Wit p) as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing
instance (SingI as, Provable p) => Auto (TyPred (PIdentity (Wit p))) as where
auto :: TyPred (PIdentity (Wit p)) @@ as
auto = Sing as -> PIdentity (Wit p) as
forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC Sing as
forall {k} (a :: k). SingI a => Sing a
sing