{-# 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 :: 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

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

-- | 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 = 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

-- | 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 = 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

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

-- | 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 (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

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

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

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

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

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

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

-- | 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 :: 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

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

-- | @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 = (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)

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

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

-- | 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 :: 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)

-- | @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 = 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

-- | 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 :: 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

-- | @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 = (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

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

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