{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Predicate (
Predicate, Wit(..)
, TyPred, Evident, EqualTo, BoolPred, Impossible, In
, PMap, type Not, decideNot
, Prove, type (-->), type (-->#)
, Provable(..)
, Disprovable, disprove
, ProvableTC, proveTC
, TFunctor(..)
, compImpl
, Decide, type (-?>), type (-?>#)
, Decidable(..)
, DecidableTC, decideTC
, DFunctor(..)
, Decision(..)
, flipDecision, mapDecision
, elimDisproof
, forgetDisproof, forgetProof, isProved, isDisproved
, mapRefuted
) where
import Data.Functor.Identity
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
import Data.Maybe
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.Prelude hiding (Not, ElemSym1)
import Data.Singletons.Prelude.Identity
import Data.Type.Functor.Product
import Data.Void
import qualified Data.Singletons.Prelude.List.NonEmpty as NE
type Predicate k = k ~> Type
type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)
data Evident :: Predicate k
type instance Apply Evident a = Sing a
type Impossible = (Not Evident :: Predicate k)
type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)
type BoolPred (p :: k ~> Bool) = (PMap p (EqualTo 'True) :: Predicate k)
type PMap (f :: k ~> j) (p :: Predicate j) = (p .@#@$$$ f :: Predicate k)
newtype Wit p a = Wit { Wit p a -> p @@ a
getWit :: p @@ a }
type Decide p = forall a. Sing a -> Decision (p @@ a)
type p -?> q = forall a. Sing a -> p @@ a -> Decision (q @@ a)
type (p -?># q) h = forall a. Sing a -> p @@ a -> h (Decision (q @@ a))
type Prove p = forall a. Sing a -> p @@ a
type p --> q = forall a. Sing a -> p @@ a -> q @@ a
type (p --># q) h = forall a. Sing a -> p @@ a -> h (q @@ a)
infixr 1 -?>
infixr 1 -?>#
infixr 1 -->
infixr 1 -->#
class Decidable p where
decide :: Decide p
default decide :: Provable p => Decide p
decide = Apply p a -> Decision (Apply p a)
forall a. a -> Decision a
Proved (Apply p a -> Decision (Apply p a))
-> (Sing a -> Apply p a) -> Sing a -> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p
class Provable p where
prove :: Prove p
type Disprovable p = Provable (Not p)
disprove :: forall p. Disprovable p => Prove (Not p)
disprove :: Prove (Not p)
disprove = Provable (Not p) => Prove (Not p)
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @(Not p)
type DecidableTC p = Decidable (TyPred p)
decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)
decideTC :: Sing a -> Decision (t a)
decideTC = Decidable (TyPred t) => Decide (TyPred t)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @(TyPred t)
type ProvableTC p = Provable (TyPred p)
proveTC :: forall t a. ProvableTC t => Sing a -> t a
proveTC :: Sing a -> t a
proveTC = Provable (TyPred t) => Prove (TyPred t)
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @(TyPred t)
class DFunctor f where
dmap :: forall p q. (p -?> q) -> (f p -?> f q)
class TFunctor f where
tmap :: forall p q. (p --> q) -> (f p --> f q)
instance (SDecide k, SingI (a :: k)) => Decidable (EqualTo a) where
decide :: Sing a -> Decision (EqualTo a @@ a)
decide = (Sing a
forall k (a :: k). SingI a => Sing a
sing Sing a -> Sing a -> Decision (a :~: a)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~)
instance Decidable Evident
instance Provable Evident where
prove :: Sing a -> Evident @@ a
prove = Sing a -> Evident @@ a
forall a. a -> a
id
instance Decidable (TyPred WrappedSing)
instance Provable (TyPred WrappedSing) where
prove :: Sing a -> TyPred WrappedSing @@ a
prove = Sing a -> TyPred WrappedSing @@ a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing
instance Provable p => Provable (TyPred (Rec (Wit p))) where
prove :: Sing a -> TyPred (Rec (Wit p)) @@ a
prove = (forall (a :: u). Sing a -> Wit p a)
-> Prod [] Sing a -> Prod [] (Wit p) a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (Rec Sing a -> Rec (Wit p) a)
-> (SList a -> Rec Sing a) -> SList a -> Rec (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SList a -> Rec Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (Rec (Wit p))) where
decide :: Sing a -> Decision (TyPred (Rec (Wit p)) @@ a)
decide = \case
SNil -> Rec (Wit p) '[] -> Decision (Rec (Wit p) '[])
forall a. a -> Decision a
Proved Rec (Wit p) '[]
forall u (a :: u -> *). Rec a '[]
RNil
x `SCons` xs -> case Sing n1 -> Decision (p @@ n1)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing n1
x of
Proved p :: p @@ n1
p -> case Sing n2 -> Decision (Rec (Wit p) n2)
forall k1 (t :: k1 -> *) (a :: k1).
DecidableTC t =>
Sing a -> Decision (t a)
decideTC Sing n2
xs of
Proved ps :: Rec (Wit p) n2
ps -> Rec (Wit p) (n1 : n2) -> Decision (TyPred (Rec (Wit p)) @@ a)
forall a. a -> Decision a
Proved (Rec (Wit p) (n1 : n2) -> Decision (TyPred (Rec (Wit p)) @@ a))
-> Rec (Wit p) (n1 : n2) -> Decision (TyPred (Rec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ (p @@ n1) -> Wit p n1
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit p @@ n1
p Wit p n1 -> Rec (Wit p) n2 -> Rec (Wit p) (n1 : n2)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec (Wit p) n2
ps
Disproved vs :: Refuted (Rec (Wit p) n2)
vs -> Refuted (Rec (Wit p) (n1 : n2))
-> Decision (TyPred (Rec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Rec (Wit p) (n1 : n2))
-> Decision (TyPred (Rec (Wit p)) @@ a))
-> Refuted (Rec (Wit p) (n1 : n2))
-> Decision (TyPred (Rec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
_ :& ps :: Rec (Wit p) rs
ps -> Refuted (Rec (Wit p) n2)
vs Rec (Wit p) n2
Rec (Wit p) rs
ps
Disproved v :: Refuted (p @@ n1)
v -> Refuted (Rec (Wit p) (n1 : n2))
-> Decision (TyPred (Rec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Rec (Wit p) (n1 : n2))
-> Decision (TyPred (Rec (Wit p)) @@ a))
-> Refuted (Rec (Wit p) (n1 : n2))
-> Decision (TyPred (Rec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
Wit p :& _ -> Refuted (p @@ n1)
v p @@ n1
p @@ r
p
instance Provable (TyPred (Rec WrappedSing)) where
prove :: Sing a -> TyPred (Rec WrappedSing) @@ a
prove = (forall (a :: u). Sing a -> WrappedSing a)
-> Prod [] Sing a -> Prod [] WrappedSing a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: u). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (Rec Sing a -> Rec WrappedSing a)
-> (SList a -> Rec Sing a) -> SList a -> Rec WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SList a -> Rec Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (Rec WrappedSing))
instance Provable p => Provable (TyPred (PMaybe (Wit p))) where
prove :: Sing a -> TyPred (PMaybe (Wit p)) @@ a
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod Maybe Sing a -> Prod Maybe (Wit p) a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (PMaybe Sing a -> PMaybe (Wit p) a)
-> (SMaybe a -> PMaybe Sing a) -> SMaybe a -> PMaybe (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMaybe a -> PMaybe Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (PMaybe (Wit p))) where
decide :: Sing a -> Decision (TyPred (PMaybe (Wit p)) @@ a)
decide = \case
SNothing -> PMaybe (Wit p) 'Nothing -> Decision (PMaybe (Wit p) 'Nothing)
forall a. a -> Decision a
Proved PMaybe (Wit p) 'Nothing
forall k (a :: k -> *). PMaybe a 'Nothing
PNothing
SJust x -> (Apply p n -> PMaybe (Wit p) ('Just n))
-> (PMaybe (Wit p) ('Just n) -> Apply p n)
-> Decision (Apply p n)
-> Decision (PMaybe (Wit p) ('Just n))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Wit p n -> PMaybe (Wit p) ('Just n)
forall k (a :: k -> *) (a1 :: k). a a1 -> PMaybe a ('Just a1)
PJust (Wit p n -> PMaybe (Wit p) ('Just n))
-> (Apply p n -> Wit p n) -> Apply p n -> PMaybe (Wit p) ('Just n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Apply p n -> Wit p n
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PJust (Wit p :: p @@ a1
p) -> Apply p n
p @@ a1
p)
(Decision (Apply p n) -> Decision (PMaybe (Wit p) ('Just n)))
-> (Sing n -> Decision (Apply p n))
-> Sing n
-> Decision (PMaybe (Wit p) ('Just n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decidable p => Decide p
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p
(Sing n -> Decision (TyPred (PMaybe (Wit p)) @@ a))
-> Sing n -> Decision (TyPred (PMaybe (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n
x
instance Provable (TyPred (PMaybe WrappedSing)) where
prove :: Sing a -> TyPred (PMaybe WrappedSing) @@ a
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod Maybe Sing a -> Prod Maybe WrappedSing a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (PMaybe Sing a -> PMaybe WrappedSing a)
-> (SMaybe a -> PMaybe Sing a) -> SMaybe a -> PMaybe WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMaybe a -> PMaybe Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (PMaybe WrappedSing))
instance Provable p => Provable (TyPred (NERec (Wit p))) where
prove :: Sing a -> TyPred (NERec (Wit p)) @@ a
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod NonEmpty Sing a -> Prod NonEmpty (Wit p) a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (NERec Sing a -> NERec (Wit p) a)
-> (SNonEmpty a -> NERec Sing a) -> SNonEmpty a -> NERec (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNonEmpty a -> NERec Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (NERec (Wit p))) where
decide :: Sing a -> Decision (TyPred (NERec (Wit p)) @@ a)
decide = \case
x NE.:%| xs -> case Sing n1 -> Decision (p @@ n1)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing n1
x of
Proved p :: p @@ n1
p -> case Sing n2 -> Decision (Rec (Wit p) n2)
forall k1 (t :: k1 -> *) (a :: k1).
DecidableTC t =>
Sing a -> Decision (t a)
decideTC Sing n2
xs of
Proved ps :: Rec (Wit p) n2
ps -> NERec (Wit p) (n1 ':| n2) -> Decision (TyPred (NERec (Wit p)) @@ a)
forall a. a -> Decision a
Proved (NERec (Wit p) (n1 ':| n2)
-> Decision (TyPred (NERec (Wit p)) @@ a))
-> NERec (Wit p) (n1 ':| n2)
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ (p @@ n1) -> Wit p n1
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit p @@ n1
p Wit p n1 -> Rec (Wit p) n2 -> NERec (Wit p) (n1 ':| n2)
forall k (a :: k -> *) (a1 :: k) (as :: [k]).
a a1 -> Rec a as -> NERec a (a1 ':| as)
:&| Rec (Wit p) n2
ps
Disproved vs :: Refuted (Rec (Wit p) n2)
vs -> Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a))
-> Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
_ :&| ps :: Rec (Wit p) as
ps -> Refuted (Rec (Wit p) n2)
vs Rec (Wit p) n2
Rec (Wit p) as
ps
Disproved v :: Refuted (p @@ n1)
v -> Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a))
-> Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
Wit p :&| _ -> Refuted (p @@ n1)
v p @@ n1
p @@ a1
p
instance Provable (TyPred (NERec WrappedSing)) where
prove :: Sing a -> TyPred (NERec WrappedSing) @@ a
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod NonEmpty Sing a -> Prod NonEmpty WrappedSing a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (NERec Sing a -> NERec WrappedSing a)
-> (SNonEmpty a -> NERec Sing a)
-> SNonEmpty a
-> NERec WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNonEmpty a -> NERec Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (NERec WrappedSing))
instance Provable p => Provable (TyPred (PIdentity (Wit p))) where
prove :: Sing a -> TyPred (PIdentity (Wit p)) @@ a
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod Identity Sing a -> Prod Identity (Wit p) a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (PIdentity Sing a -> PIdentity (Wit p) a)
-> (SIdentity a -> PIdentity Sing a)
-> SIdentity a
-> PIdentity (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIdentity a -> PIdentity Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (PIdentity (Wit p))) where
decide :: Sing a -> Decision (TyPred (PIdentity (Wit p)) @@ a)
decide = \case
SIdentity x -> (Apply p n -> PIdentity (Wit p) ('Identity n))
-> (PIdentity (Wit p) ('Identity n) -> Apply p n)
-> Decision (Apply p n)
-> Decision (PIdentity (Wit p) ('Identity n))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Wit p n -> PIdentity (Wit p) ('Identity n)
forall k (a :: k -> *) (a1 :: k).
a a1 -> PIdentity a ('Identity a1)
PIdentity (Wit p n -> PIdentity (Wit p) ('Identity n))
-> (Apply p n -> Wit p n)
-> Apply p n
-> PIdentity (Wit p) ('Identity n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Apply p n -> Wit p n
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PIdentity (Wit p :: p @@ a1
p) -> Apply p n
p @@ a1
p)
(Decision (Apply p n)
-> Decision (PIdentity (Wit p) ('Identity n)))
-> (Sing n -> Decision (Apply p n))
-> Sing n
-> Decision (PIdentity (Wit p) ('Identity n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decidable p => Decide p
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p
(Sing n -> Decision (TyPred (PIdentity (Wit p)) @@ a))
-> Sing n -> Decision (TyPred (PIdentity (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n
x
instance Provable (TyPred (PIdentity WrappedSing)) where
prove :: Sing a -> TyPred (PIdentity WrappedSing) @@ a
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod Identity Sing a -> Prod Identity WrappedSing a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (PIdentity Sing a -> PIdentity WrappedSing a)
-> (SIdentity a -> PIdentity Sing a)
-> SIdentity a
-> PIdentity WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIdentity a -> PIdentity Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (PIdentity WrappedSing))
instance Provable p => Provable (TyPred (PEither (Wit p))) where
prove :: Sing a -> TyPred (PEither (Wit p)) @@ a
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod (Either j) Sing a -> Prod (Either j) (Wit p) a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (PEither Sing a -> PEither (Wit p) a)
-> (SEither a -> PEither Sing a) -> SEither a -> PEither (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEither a -> PEither Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (PEither (Wit p))) where
decide :: Sing a -> Decision (TyPred (PEither (Wit p)) @@ a)
decide = \case
SLeft x -> PEither (Wit p) ('Left n)
-> Decision (TyPred (PEither (Wit p)) @@ a)
forall a. a -> Decision a
Proved (PEither (Wit p) ('Left n)
-> Decision (TyPred (PEither (Wit p)) @@ a))
-> PEither (Wit p) ('Left n)
-> Decision (TyPred (PEither (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n -> PEither (Wit p) ('Left n)
forall j k (e :: j) (a :: k -> *). Sing e -> PEither a ('Left e)
PLeft Sing n
x
SRight y -> (Apply p n -> PEither (Wit p) ('Right n))
-> (PEither (Wit p) ('Right n) -> Apply p n)
-> Decision (Apply p n)
-> Decision (PEither (Wit p) ('Right n))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Wit p n -> PEither (Wit p) ('Right n)
forall k j (a :: k -> *) (a1 :: k). a a1 -> PEither a ('Right a1)
PRight (Wit p n -> PEither (Wit p) ('Right n))
-> (Apply p n -> Wit p n)
-> Apply p n
-> PEither (Wit p) ('Right n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Apply p n -> Wit p n
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PRight (Wit p :: p @@ a1
p) -> Apply p n
p @@ a1
p)
(Decision (Apply p n) -> Decision (PEither (Wit p) ('Right n)))
-> (Sing n -> Decision (Apply p n))
-> Sing n
-> Decision (PEither (Wit p) ('Right n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decidable p => Decide p
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p
(Sing n -> Decision (TyPred (PEither (Wit p)) @@ a))
-> Sing n -> Decision (TyPred (PEither (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n
y
instance Provable (TyPred (PEither WrappedSing)) where
prove :: Sing a -> TyPred (PEither WrappedSing) @@ a
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod (Either j) Sing a -> Prod (Either j) WrappedSing a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (PEither Sing a -> PEither WrappedSing a)
-> (SEither a -> PEither Sing a)
-> SEither a
-> PEither WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEither a -> PEither Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (PEither WrappedSing))
instance Provable p => Provable (TyPred (PTup (Wit p))) where
prove :: Sing a -> TyPred (PTup (Wit p)) @@ a
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod ((,) j) Sing a -> Prod ((,) j) (Wit p) a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (PTup Sing a -> PTup (Wit p) a)
-> (STuple2 a -> PTup Sing a) -> STuple2 a -> PTup (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STuple2 a -> PTup Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (PTup (Wit p))) where
decide :: Sing a -> Decision (TyPred (PTup (Wit p)) @@ a)
decide (STuple2 x y) = (Apply p n2 -> PTup (Wit p) '(n1, n2))
-> (PTup (Wit p) '(n1, n2) -> Apply p n2)
-> Decision (Apply p n2)
-> Decision (PTup (Wit p) '(n1, n2))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Sing n1 -> Wit p n2 -> PTup (Wit p) '(n1, n2)
forall j k (w :: j) (a :: k -> *) (a1 :: k).
Sing w -> a a1 -> PTup a '(w, a1)
PTup Sing n1
x (Wit p n2 -> PTup (Wit p) '(n1, n2))
-> (Apply p n2 -> Wit p n2) -> Apply p n2 -> PTup (Wit p) '(n1, n2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Apply p n2 -> Wit p n2
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PTup _ (Wit p :: p @@ a1
p) -> Apply p n2
p @@ a1
p)
(Decision (Apply p n2) -> Decision (PTup (Wit p) '(n1, n2)))
-> (Sing n2 -> Decision (Apply p n2))
-> Sing n2
-> Decision (PTup (Wit p) '(n1, n2))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decidable p => Decide p
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p
(Sing n2 -> Decision (TyPred (PTup (Wit p)) @@ a))
-> Sing n2 -> Decision (TyPred (PTup (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n2
y
instance Provable (TyPred (PTup WrappedSing)) where
prove :: Sing a -> TyPred (PTup WrappedSing) @@ a
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod ((,) j) Sing a -> Prod ((,) j) WrappedSing a
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (PTup Sing a -> PTup WrappedSing a)
-> (STuple2 a -> PTup Sing a) -> STuple2 a -> PTup WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STuple2 a -> PTup Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (PTup WrappedSing))
instance (Decidable p, SingI f) => Decidable (PMap f p) where
decide :: Sing a -> Decision (PMap f p @@ a)
decide = Decidable p => Decide p
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p (Sing (Apply f a) -> Decision (p @@ Apply f a))
-> (Sing a -> Sing (Apply f a))
-> Sing a
-> Decision (p @@ Apply f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
forall k1 k2 (f :: k1 ~> k2).
SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing (Sing f
forall k (a :: k). SingI a => Sing a
sing :: Sing f)
instance (Provable p, SingI f) => Provable (PMap f p) where
prove :: Sing a -> PMap f p @@ a
prove = Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p (Sing (Apply f a) -> p @@ Apply f a)
-> (Sing a -> Sing (Apply f a)) -> Sing a -> p @@ Apply f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
forall k1 k2 (f :: k1 ~> k2).
SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing (Sing f
forall k (a :: k). SingI a => Sing a
sing :: Sing f)
compImpl
:: forall p q r. ()
=> p --> q
-> q --> r
-> p --> r
compImpl :: (p --> q) -> (q --> r) -> p --> r
compImpl f :: p --> q
f g :: q --> r
g s :: Sing a
s = Sing a -> (q @@ a) -> Apply r a
q --> r
g Sing a
s ((q @@ a) -> Apply r a)
-> (Apply p a -> q @@ a) -> Apply p a -> Apply r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Apply p a -> q @@ a
p --> q
f Sing a
s
data Not :: Predicate k -> Predicate k
type instance Apply (Not p) a = Refuted (p @@ a)
instance Decidable p => Decidable (Not p) where
decide :: Sing a -> Decision (Not p @@ a)
decide (x :: Sing a) = Decision (p @@ a) -> Decision (Not p @@ a)
forall k1 (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
decideNot @p @a (Sing a -> Decision (p @@ a)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing a
x)
instance Provable (Not Impossible) where
prove :: Sing a -> Not Impossible @@ a
prove x :: Sing a
x v :: Sing a -> Void
v = Void -> Void
forall a. Void -> a
absurd (Void -> Void) -> Void -> Void
forall a b. (a -> b) -> a -> b
$ Sing a -> Void
v Sing a
x
decideNot
:: forall p a. ()
=> Decision (p @@ a)
-> Decision (Not p @@ a)
decideNot :: Decision (p @@ a) -> Decision (Not p @@ a)
decideNot = Decision (p @@ a) -> Decision (Not p @@ a)
forall a. Decision a -> Decision (Refuted a)
flipDecision
flipDecision
:: Decision a
-> Decision (Refuted a)
flipDecision :: Decision a -> Decision (Refuted a)
flipDecision = \case
Proved p :: a
p -> Refuted (Refuted a) -> Decision (Refuted a)
forall a. Refuted a -> Decision a
Disproved (Refuted a -> Refuted a
forall a b. (a -> b) -> a -> b
$ a
p)
Disproved v :: Refuted a
v -> Refuted a -> Decision (Refuted a)
forall a. a -> Decision a
Proved Refuted a
v
mapDecision
:: (a -> b)
-> (b -> a)
-> Decision a
-> Decision b
mapDecision :: (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision f :: a -> b
f g :: b -> a
g = \case
Proved p :: a
p -> b -> Decision b
forall a. a -> Decision a
Proved (b -> Decision b) -> b -> Decision b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
p
Disproved v :: Refuted a
v -> Refuted b -> Decision b
forall a. Refuted a -> Decision a
Disproved (Refuted b -> Decision b) -> Refuted b -> Decision b
forall a b. (a -> b) -> a -> b
$ (b -> a) -> Refuted a -> Refuted b
forall a b. (a -> b) -> Refuted b -> Refuted a
mapRefuted b -> a
g Refuted a
v
forgetDisproof
:: Decision a
-> Maybe a
forgetDisproof :: Decision a -> Maybe a
forgetDisproof = \case
Proved p :: a
p -> a -> Maybe a
forall a. a -> Maybe a
Just a
p
Disproved _ -> Maybe a
forall a. Maybe a
Nothing
forgetProof
:: Decision a
-> Maybe (Refuted a)
forgetProof :: Decision a -> Maybe (Refuted a)
forgetProof = Decision (Refuted a) -> Maybe (Refuted a)
forall a. Decision a -> Maybe a
forgetDisproof (Decision (Refuted a) -> Maybe (Refuted a))
-> (Decision a -> Decision (Refuted a))
-> Decision a
-> Maybe (Refuted a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decision a -> Decision (Refuted a)
forall a. Decision a -> Decision (Refuted a)
flipDecision
isProved :: Decision a -> Bool
isProved :: Decision a -> Bool
isProved = Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (Maybe a -> Bool) -> (Decision a -> Maybe a) -> Decision a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decision a -> Maybe a
forall a. Decision a -> Maybe a
forgetDisproof
isDisproved :: Decision a -> Bool
isDisproved :: Decision a -> Bool
isDisproved = Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe a -> Bool) -> (Decision a -> Maybe a) -> Decision a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decision a -> Maybe a
forall a. Decision a -> Maybe a
forgetDisproof
elimDisproof
:: Decision a
-> Refuted (Refuted a)
-> a
elimDisproof :: Decision a -> Refuted (Refuted a) -> a
elimDisproof = \case
Proved p :: a
p -> a -> Refuted (Refuted a) -> a
forall a b. a -> b -> a
const a
p
Disproved v :: Refuted a
v -> Void -> a
forall a. Void -> a
absurd (Void -> a)
-> (Refuted (Refuted a) -> Void) -> Refuted (Refuted a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Refuted (Refuted a) -> Refuted (Refuted a)
forall a b. (a -> b) -> a -> b
$ Refuted a
v)
mapRefuted
:: (a -> b)
-> Refuted b
-> Refuted a
mapRefuted :: (a -> b) -> Refuted b -> Refuted a
mapRefuted = (Refuted b -> (a -> b) -> Refuted a)
-> (a -> b) -> Refuted b -> Refuted a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Refuted b -> (a -> b) -> Refuted a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
instance (SDecide k, SingI (as :: [k])) => Decidable (In [] as) where
decide :: forall a. Sing a -> Decision (Index as a)
decide :: Sing a -> Decision (Index as a)
decide x :: Sing a
x = Sing as -> Decision (Index as a)
forall (bs :: [k]). Sing bs -> Decision (Index bs a)
go (SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as)
where
go :: Sing bs -> Decision (Index bs a)
go :: Sing bs -> Decision (Index bs a)
go = \case
SNil -> Refuted (Index bs a) -> Decision (Index bs a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Index bs a) -> Decision (Index bs a))
-> Refuted (Index bs a) -> Decision (Index bs a)
forall a b. (a -> b) -> a -> b
$ \case {}
y `SCons` ys -> case Sing a
x Sing a -> Sing n1 -> Decision (a :~: n1)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
Proved Refl -> Index (a : n2) a -> Decision (Index (a : n2) a)
forall a. a -> Decision a
Proved Index (a : n2) a
forall k (b :: k) (as :: [k]). Index (b : as) b
IZ
Disproved v :: Refuted (a :~: n1)
v -> case Sing n2 -> Decision (Index n2 a)
forall (bs :: [k]). Sing bs -> Decision (Index bs a)
go Sing n2
ys of
Proved i :: Index n2 a
i -> Index (n1 : n2) a -> Decision (Index (n1 : n2) a)
forall a. a -> Decision a
Proved (Index n2 a -> Index (n1 : n2) a
forall k (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Index n2 a
i)
Disproved u :: Refuted (Index n2 a)
u -> Refuted (Index bs a) -> Decision (Index bs a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Index bs a) -> Decision (Index bs a))
-> Refuted (Index bs a) -> Decision (Index bs a)
forall a b. (a -> b) -> a -> b
$ \case
IZ -> Refuted (a :~: n1)
v a :~: n1
forall k (a :: k). a :~: a
Refl
IS i :: Index bs a
i -> Refuted (Index n2 a)
u Index n2 a
Index bs a
i
instance (SDecide k, SingI (as :: Maybe k)) => Decidable (In Maybe as) where
decide :: Sing a -> Decision (In Maybe as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
SNothing -> Refuted (IJust 'Nothing a) -> Decision (In Maybe as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IJust 'Nothing a) -> Decision (In Maybe as @@ a))
-> Refuted (IJust 'Nothing a) -> Decision (In Maybe as @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
SJust y -> case Sing a
x Sing a -> Sing n -> Decision (a :~: n)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
Proved Refl -> IJust ('Just a) a -> Decision (IJust ('Just a) a)
forall a. a -> Decision a
Proved IJust ('Just a) a
forall k (b :: k). IJust ('Just b) b
IJust
Disproved v :: Refuted (a :~: n)
v -> Refuted (IJust ('Just n) a) -> Decision (In Maybe as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IJust ('Just n) a) -> Decision (In Maybe as @@ a))
-> Refuted (IJust ('Just n) a) -> Decision (In Maybe as @@ a)
forall a b. (a -> b) -> a -> b
$ \case IJust -> Refuted (a :~: n)
v a :~: n
forall k (a :: k). a :~: a
Refl
instance (SDecide k, SingI (as :: Either j k)) => Decidable (In (Either j) as) where
decide :: Sing a -> Decision (In (Either j) as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
SLeft _ -> Refuted (IRight ('Left n) a) -> Decision (In (Either j) as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IRight ('Left n) a) -> Decision (In (Either j) as @@ a))
-> Refuted (IRight ('Left n) a) -> Decision (In (Either j) as @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
SRight y -> case Sing a
x Sing a -> Sing n -> Decision (a :~: n)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
Proved Refl -> IRight ('Right a) a -> Decision (IRight ('Right a) a)
forall a. a -> Decision a
Proved IRight ('Right a) a
forall k j (b :: k). IRight ('Right b) b
IRight
Disproved v :: Refuted (a :~: n)
v -> Refuted (IRight ('Right n) a) -> Decision (In (Either j) as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IRight ('Right n) a) -> Decision (In (Either j) as @@ a))
-> Refuted (IRight ('Right n) a)
-> Decision (In (Either j) as @@ a)
forall a b. (a -> b) -> a -> b
$ \case IRight -> Refuted (a :~: n)
v a :~: n
forall k (a :: k). a :~: a
Refl
instance (SDecide k, SingI (as :: NonEmpty k)) => Decidable (In NonEmpty as) where
decide :: Sing a -> Decision (In NonEmpty as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
y NE.:%| (Sing :: Sing bs) -> case Sing a
x Sing a -> Sing n1 -> Decision (a :~: n1)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
Proved Refl -> NEIndex (a ':| n2) a -> Decision (NEIndex (a ':| n2) a)
forall a. a -> Decision a
Proved NEIndex (a ':| n2) a
forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead
Disproved v :: Refuted (a :~: n1)
v -> case Sing a -> Decision (In [] n2 @@ a)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @(In [] bs) Sing a
x of
Proved i :: In [] n2 @@ a
i -> NEIndex (n1 ':| n2) a -> Decision (In NonEmpty as @@ a)
forall a. a -> Decision a
Proved (NEIndex (n1 ':| n2) a -> Decision (In NonEmpty as @@ a))
-> NEIndex (n1 ':| n2) a -> Decision (In NonEmpty as @@ a)
forall a b. (a -> b) -> a -> b
$ Index n2 a -> NEIndex (n1 ':| n2) a
forall k (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail Index n2 a
In [] n2 @@ a
i
Disproved u :: Refuted (In [] n2 @@ a)
u -> Refuted (NEIndex (n1 ':| n2) a) -> Decision (In NonEmpty as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (NEIndex (n1 ':| n2) a) -> Decision (In NonEmpty as @@ a))
-> Refuted (NEIndex (n1 ':| n2) a)
-> Decision (In NonEmpty as @@ a)
forall a b. (a -> b) -> a -> b
$ \case
NEHead -> Refuted (a :~: n1)
v a :~: n1
forall k (a :: k). a :~: a
Refl
NETail i :: Index as a
i -> Refuted (In [] n2 @@ a)
u Index as a
In [] n2 @@ a
i
instance (SDecide k, SingI (as :: (j, k))) => Decidable (In ((,) j) as) where
decide :: Sing a -> Decision (In ((,) j) as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
STuple2 _ y -> case Sing a
x Sing a -> Sing n2 -> Decision (a :~: n2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n2
y of
Proved Refl -> ISnd '(n1, a) a -> Decision (ISnd '(n1, a) a)
forall a. a -> Decision a
Proved ISnd '(n1, a) a
forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd
Disproved v :: Refuted (a :~: n2)
v -> Refuted (ISnd '(n1, n2) a) -> Decision (In ((,) j) as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (ISnd '(n1, n2) a) -> Decision (In ((,) j) as @@ a))
-> Refuted (ISnd '(n1, n2) a) -> Decision (In ((,) j) as @@ a)
forall a b. (a -> b) -> a -> b
$ \case ISnd -> Refuted (a :~: n2)
v a :~: n2
forall k (a :: k). a :~: a
Refl
instance (SDecide k, SingI (as :: Identity k)) => Decidable (In Identity as) where
decide :: Sing a -> Decision (In Identity as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
SIdentity y -> case Sing a
x Sing a -> Sing n -> Decision (a :~: n)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
Proved Refl -> IIdentity ('Identity a) a -> Decision (IIdentity ('Identity a) a)
forall a. a -> Decision a
Proved IIdentity ('Identity a) a
forall k (b :: k). IIdentity ('Identity b) b
IId
Disproved v :: Refuted (a :~: n)
v -> Refuted (IIdentity ('Identity n) a)
-> Decision (In Identity as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IIdentity ('Identity n) a)
-> Decision (In Identity as @@ a))
-> Refuted (IIdentity ('Identity n) a)
-> Decision (In Identity as @@ a)
forall a b. (a -> b) -> a -> b
$ \case IId -> Refuted (a :~: n)
v a :~: n
forall k (a :: k). a :~: a
Refl