{-# 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
-- Copyright   : (c) Justin Le 2018
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Useful utilities for situations where you know that a predicate @P@ is
-- satisfied for a specific @a@ at compile-time.
--
-- @since 0.1.1.0
module Data.Type.Predicate.Auto (
  -- * Automatically generate witnesses at compile-time
    Auto(..)
  , autoTC
  , AutoNot
  , autoNot
  , autoAny, autoNotAll
  , AutoProvable
  -- ** Helper classes
  , 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

-- | Automatically generate a witness for predicate @p@ applied to input
-- @a@.
--
-- Mostly useful for situations where you know @a@ at compile-time, so you
-- can just write 'auto' directly in your source code.  The choice is
-- intended to mirror the @auto@ keyword in languages like Idris.
--
-- Very close in nature to the @Known@ typeclass in the /type-combinators/
-- library.
--
-- Admittedly this interface is a bit clunky and ad-hoc; at this point you
-- can just try writing 'auto' in your code and praying that it works.  You
-- always have the option, of course, to just manually write proofs.  If
-- you have any inference rules to suggest, feel free to submit a PR!
--
-- An important limitation of 'Auto' is the Haskell type system prevents
-- "either-or" constraints; this could potentially be implemented using
-- compiler plugins.
--
-- One consequence of this is that it is impossible to automatically derive
-- @'Any' f p@ and @'Not' ('All' f p)@.
--
-- For these, the compiler needs help; you can use 'autoAny' and
-- 'autoNotAll' for these situations.
class Auto (p :: Predicate k) (a :: k) where
    -- | Have the compiler generate a witness for @p \@\@ a@.
    --
    -- Must be called using type application syntax:
    --
    -- @
    -- 'auto' @_ @p @a
    -- @
    auto :: p @@ a

-- | A version of 'auto' that "just works" with type inference, if the
-- predicate is a type constructor.
--
-- @since 0.2.1.0
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 = forall {k} (a :: k). SingI a => Sing a
sing

-- | @since 0.1.2.0
instance SingI a => Auto (Not Impossible) a where
    auto :: Not Impossible @@ a
auto = (forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
sing)

instance Auto (EqualTo a) a where
    auto :: EqualTo a @@ a
auto = 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

-- | Helper "predicate transformer" that gives you an instant 'auto' for
-- any 'Provable' instance.
--
-- For example, say you have predicate @P@ that you know is 'Provable', and
-- you wish to generate a @P \@\@ x@, for some specific @x@ you know at
-- compile-time.  You can use:
--
-- @
-- 'auto' \@_ \@('AutoProvable' P) \@x
-- @
--
-- to obtain a @P \@\@ x@.
--
-- 'AutoProvable' is essentially the identity function.
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
prove @p @a forall {k} (a :: k). SingI a => Sing a
sing

-- | Typeclass representing 'Elem's pointing to an @a :: k@ that can be
-- generated automatically from type-level collection @as :: f k@.
--
-- If GHC knows both the type-level collection and the element you want to
-- find at compile-time, this instance should allow it to find it.
--
-- Used to help in the instance of 'Auto' for the 'In' predicate.
--
-- Example usage:
--
-- @
-- 'autoElem' :: 'Index' '[1,6,2,3] 2
-- -- IS (IS IZ)        -- third spot
-- @
--
-- And when used with 'Auto':
--
-- @
-- 'auto' \@_ \@('In' [] '[1,6,2,3]) \@2
-- -- IS (IS IZ)
-- @
class AutoElem f (as :: f k) (a :: k) where
    -- | Generate the 'Elem' pointing to the @a :: @ in a type-level
    -- collection @as :: f k@.
    autoElem :: Elem f as a

instance {-# OVERLAPPING #-} AutoElem [] (a ': as) a where
    autoElem :: Elem [] (a : as) a
autoElem = 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 = forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS 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 = 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 = forall {k} {j} (b :: k). IRight ('Right b) b
IRight

instance AutoElem NonEmpty (a ':| as) a where
    autoElem :: Elem NonEmpty (a ':| as) a
autoElem = 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 = forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail forall k (f :: * -> *) (as :: f k) (a :: k).
AutoElem f as a =>
Elem f as a
autoElem

-- | @since 0.1.2.0
instance AutoElem ((,) j) '(w, a) a where
    autoElem :: Elem ((,) j) '(w, a) a
autoElem = 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 = 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

-- | Helper class for deriving 'Auto' instances for 'All' predicates; each
-- 'Universe' instance is expected to implement these if possible, to get
-- free 'Auto' instaces for their 'All' predicates.
--
-- Also helps for 'Not' 'Any' predicates and 'Not' 'Found' 'AnyMatch'
-- predicates.
--
-- @since 0.1.2.0
class AutoAll f (p :: Predicate k) (as :: f k) where
    -- | Generate an 'All' for a given predicate over all items in @as@.
    autoAll :: All f p @@ as

instance AutoAll [] p '[] where
    autoAll :: All [] p @@ '[]
autoAll = 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. (a -> b) -> a -> b
$ \case {}

instance (Auto p a, AutoAll [] p as) => AutoAll [] p (a ': as) where
    autoAll :: All [] p @@ (a : as)
autoAll = 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. (a -> b) -> a -> b
$ \case
        Elem [] (a : as) a
Index (a : as) a
IZ   -> forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
        IS Index bs a
i -> 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
i

instance AutoAll Maybe p 'Nothing where
    autoAll :: All Maybe p @@ 'Nothing
autoAll = 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. (a -> b) -> a -> b
$ \case {}

instance Auto p a => AutoAll Maybe p ('Just a) where
    autoAll :: All Maybe p @@ 'Just a
autoAll = 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. (a -> b) -> a -> b
$ \case Elem Maybe ('Just a) a
IJust ('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 k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll 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 k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case Elem (Either j) ('Right a) a
IRight ('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 k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case
        Elem NonEmpty (a ':| as) a
NEIndex (a ':| as) a
NEHead   -> forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a
        NETail Index as a
i -> 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
i

instance Auto p a => AutoAll ((,) j) p '(w, a) where
    autoAll :: All ((,) j) p @@ '(w, a)
autoAll = 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. (a -> b) -> a -> b
$ \case Elem ((,) j) '(w, a) a
ISnd '(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 k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case Elem Identity ('Identity a) a
IIdentity ('Identity a) a
IId -> forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @p @a

-- | @since 0.1.2.0
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

-- | @since 0.1.2.0
instance SingI a => Auto (NotNull []) (a ': as) where
    auto :: NotNull [] @@ (a : as)
auto = forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ forall {k} (a :: k). SingI a => Sing a
sing

-- | @since 0.1.2.0
instance SingI a => Auto IsJust ('Just a) where
    auto :: IsJust @@ 'Just a
auto = forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny forall {k} (b :: k). IJust ('Just b) b
IJust forall {k} (a :: k). SingI a => Sing a
sing

-- | @since 0.1.2.0
instance SingI a => Auto IsRight ('Right a) where
    auto :: IsRight @@ 'Right a
auto = forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny forall {k} {j} (b :: k). IRight ('Right b) b
IRight forall {k} (a :: k). SingI a => Sing a
sing

-- | @since 0.1.2.0
instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where
    auto :: NotNull NonEmpty @@ (a ':| as)
auto = forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead forall {k} (a :: k). SingI a => Sing a
sing

-- | @since 0.1.2.0
instance SingI a => Auto (NotNull ((,) j)) '(w, a) where
    auto :: NotNull ((,) j) @@ '(w, a)
auto = forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd forall {k} (a :: k). SingI a => Sing a
sing

instance SingI a => Auto (NotNull Identity) ('Identity a) where
    auto :: NotNull Identity @@ 'Identity a
auto = forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny forall {k} (b :: k). IIdentity ('Identity b) b
IId forall {k} (a :: k). SingI a => Sing a
sing

-- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to
-- not be true at compiletime.
--
-- @since 0.1.2.0
type AutoNot (p :: Predicate k) = Auto (Not p)

-- | Disprove @p \@\@ a@ at compiletime.
--
-- @
-- 'autoNot' \@_ \@p \@a :: 'Not' p '@@' a
-- @
--
-- @since 0.1.2.0
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

-- | @since 0.1.2.0
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 forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: p (f @@ a) @@ fst
p

-- | @since 0.1.2.0
instance Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p)) a where
    auto :: NotFound (PPMap f p) @@ a
auto = forall a b. (a -> b) -> Refuted b -> Refuted a
mapRefuted (\(Sing fst
i :&: PPMap f p a @@ fst
p) -> Sing fst
i forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: PPMap f p a @@ fst
p)
         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)

-- | @since 0.1.2.0
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)

-- | @since 0.1.2.0
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)

-- | Helper function to generate an @'Any' f p@ if you can pick out
-- a specific @a@ in @as@ where the predicate is provable at compile-time.
--
-- This is used to get around a fundamental limitation of 'Auto' as
-- a Haskell typeclass.
--
-- @since 0.1.2.0
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 = 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)

-- | @since 0.1.2.0
instance (SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p)) as where
    auto :: Not (Any f p) @@ as
auto = forall {k} (f :: * -> *) (p :: Predicate k).
All f (Not p) --> None f p
allNotNone forall {k} (a :: k). SingI a => Sing a
sing 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

-- | Helper function to generate a @'Not' ('All' f p)@ if you can pick out
-- a specific @a@ in @as@ where the predicate is disprovable at compile-time.
--
-- This is used to get around a fundamental limitation of 'Auto' as
-- a Haskell typeclass.
--
-- @since 0.1.2.0
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 = forall {k} (f :: * -> *) (p :: Predicate k).
Any f (Not p) --> NotAll f p
anyNotNotAll forall {k} (a :: k). SingI a => Sing a
sing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: * -> *) (p :: Predicate k) (as :: f k) (a :: k).
Auto p a =>
Elem f as a -> Any f p @@ as
autoAny

-- | @since 0.1.2.0
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 = forall a b. (a -> b) -> Refuted b -> Refuted a
mapRefuted (\(Sing fst
s :&: WitAny Elem f as a1
i FlipPP p fst @@ a1
p) -> 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 forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: FlipPP p fst @@ a1
p))
         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

-- | @since 3.0.0
instance SingI as => Auto (TyPred (Rec WrappedSing)) as where
    auto :: TyPred (Rec WrappedSing) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance SingI as => Auto (TyPred (PMaybe WrappedSing)) as where
    auto :: TyPred (PMaybe WrappedSing) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance SingI as => Auto (TyPred (NERec WrappedSing)) as where
    auto :: TyPred (NERec WrappedSing) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance SingI as => Auto (TyPred (PEither WrappedSing)) as where
    auto :: TyPred (PEither WrappedSing) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance SingI as => Auto (TyPred (PTup WrappedSing)) as where
    auto :: TyPred (PTup WrappedSing) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance SingI as => Auto (TyPred (PIdentity WrappedSing)) as where
    auto :: TyPred (PIdentity WrappedSing) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing

-- | @since 3.0.0
instance (SingI as, Provable p) => Auto (TyPred (Rec (Wit p))) as where
    auto :: TyPred (Rec (Wit p)) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance (SingI as, Provable p) => Auto (TyPred (PMaybe (Wit p))) as where
    auto :: TyPred (PMaybe (Wit p)) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance (SingI as, Provable p) => Auto (TyPred (NERec (Wit p))) as where
    auto :: TyPred (NERec (Wit p)) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance (SingI as, Provable p) => Auto (TyPred (PEither (Wit p))) as where
    auto :: TyPred (PEither (Wit p)) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance (SingI as, Provable p) => Auto (TyPred (PTup (Wit p))) as where
    auto :: TyPred (PTup (Wit p)) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing
-- | @since 3.0.0
instance (SingI as, Provable p) => Auto (TyPred (PIdentity (Wit p))) as where
    auto :: TyPred (PIdentity (Wit p)) @@ as
auto = forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC forall {k} (a :: k). SingI a => Sing a
sing