{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# 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 :: t a
autoTC = Auto (TyPred t) a => TyPred t @@ a
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 = 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 = 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 = (Auto p a => p @@ a
forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a, Auto q a => q @@ 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 _ = Auto q a => q @@ 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 = Sing a -> p @@ a
forall k1 (p :: k1 ~> *). 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 = 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
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 = 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 = 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 = 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
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 = 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 = 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 = AutoElem f as a => Elem f as a
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) -> All [] 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) -> All [] p @@ '[])
-> (forall (a :: k). Elem [] '[] a -> p @@ a) -> All [] 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)
-> All [] 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)
-> All [] p @@ (a : as))
-> (forall (a :: a). Elem [] (a : as) a -> p @@ a)
-> All [] p @@ (a : as)
forall a b. (a -> b) -> a -> b
$ \case
IZ -> Auto p a => p @@ a
forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
IS i -> WitAll [] p as -> Elem [] as a -> Apply p a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll (AutoAll [] p as => All [] p @@ as
forall k (f :: * -> *) (p :: Predicate k) (as :: f k).
AutoAll f p as =>
All f p @@ as
autoAll @_ @[] @p @as) Elem [] as a
Index bs a
i
instance AutoAll Maybe p 'Nothing where
autoAll :: All Maybe p @@ 'Nothing
autoAll = (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> All 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)
-> All Maybe p @@ 'Nothing)
-> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> All 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)
-> All 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)
-> All Maybe p @@ 'Just a)
-> (forall (a :: a). Elem Maybe ('Just a) a -> p @@ a)
-> All Maybe p @@ 'Just a
forall a b. (a -> b) -> a -> b
$ \case IJust -> Auto p a => p @@ a
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)
-> All (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)
-> All (Either j) p @@ 'Left e)
-> (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> All (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)
-> All (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)
-> All (Either j) p @@ 'Right a)
-> (forall (a :: b). Elem (Either j) ('Right a) a -> p @@ a)
-> All (Either j) p @@ 'Right a
forall a b. (a -> b) -> a -> b
$ \case IRight -> Auto p a => p @@ a
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)
-> All 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)
-> All NonEmpty p @@ (a ':| as))
-> (forall (a :: a). Elem NonEmpty (a ':| as) a -> p @@ a)
-> All NonEmpty p @@ (a ':| as)
forall a b. (a -> b) -> a -> b
$ \case
NEHead -> Auto p a => p @@ a
forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
NETail i -> WitAll [] p as -> Elem [] as a -> Apply p a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll (AutoAll [] p as => All [] p @@ as
forall k (f :: * -> *) (p :: Predicate k) (as :: f k).
AutoAll f p as =>
All f p @@ as
autoAll @_ @[] @p @as) Elem [] as a
Index 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)
-> All ((,) 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)
-> All ((,) j) p @@ '(w, a))
-> (forall (a :: k). Elem ((,) j) '(w, a) a -> p @@ a)
-> All ((,) j) p @@ '(w, a)
forall a b. (a -> b) -> a -> b
$ \case ISnd -> Auto p a => p @@ a
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)
-> All 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)
-> All Identity p @@ 'Identity a)
-> (forall (a :: a). Elem Identity ('Identity a) a -> p @@ a)
-> All Identity p @@ 'Identity a
forall a b. (a -> b) -> a -> b
$ \case IId -> Auto p a => p @@ a
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 = AutoAll f p as => All f p @@ as
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 :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem [] (a : as) a
forall k (b :: k) (as :: [k]). Index (b : as) b
IZ 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 :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem Maybe ('Just a) a
forall k (b :: k). IJust ('Just b) b
IJust 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 :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem (Either j) ('Right a) a
forall k j (b :: k). IRight ('Right b) b
IRight 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 :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem NonEmpty (a ':| as) a
forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead 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 :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem ((,) j) '(w, a) a
forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd 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 :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem Identity ('Identity a) a
forall k (b :: k). IIdentity ('Identity b) b
IId 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 :: Not p @@ a
autoNot = Auto (Not p) a => Not p @@ a
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 Auto (Found p) (f @@ a) => Found p @@ (f @@ a)
forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(Found p) @(f @@ a) of
i :&: 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 (\(i :: Sing fst
i :&: p :: 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))) -> NotFound (PPMap f p) @@ a)
-> Refuted (Σ v (p (f @@ a))) -> NotFound (PPMap f p) @@ a
forall a b. (a -> b) -> a -> b
$ Auto (NotFound p) (f @@ a) => NotFound p @@ (f @@ a)
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 = Auto p (f @@ a) => p @@ (f @@ a)
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 = AutoNot p (f @@ a) => Not p @@ (f @@ a)
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 :: Elem f as a -> Any f p @@ as
autoAny i :: Elem f as a
i = Elem f as a -> (p @@ a) -> WitAny f p as
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f as a
i (Auto p a => p @@ a
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).
All f (Not p) --> None f p
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
$ AutoAll f (Not p) as => All f (Not p) @@ as
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 :: Elem f as a -> Not (All f p) @@ as
autoNotAll = Sing as -> (Any f (Not p) @@ as) -> Not (All f p) @@ as
forall k (f :: * -> *) (p :: Predicate k).
Any f (Not p) --> NotAll f p
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 -> 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 (\(s :: Sing fst
s :&: WitAny i p) -> Elem f as a -> (Found p @@ a) -> WitAny f (Found p) as
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f as a
i (Sing fst
s Sing fst -> (p a @@ fst) -> Sigma v (p a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: FlipPP p fst @@ a
p a @@ fst
p))
(Refuted (WitAny f (Found p) as)
-> Not (Found (AnyMatch f p)) @@ as)
-> Refuted (WitAny f (Found p) as)
-> Not (Found (AnyMatch f p)) @@ as
forall a b. (a -> b) -> a -> b
$ Auto (Not (Any f (Found p))) as => Not (Any f (Found p)) @@ as
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