{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}

#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE ConstrainedClassMethods, TypeFamilyDependencies #-}
#endif
module Proof.Equational
  ( (:~:) (..),
    (:=:),
    sym,
    trans,
    Equality (..),
    Preorder (..),
    reflexivity',
    (:\/:),
    (:/\:),
    (=<=),
    (=>=),
    (=~=),
    Leibniz (..),
    Reason (..),
    because,
    by,
    (===),
    start,
    byDefinition,
    admitted,
    Proxy (..),
    cong,
    cong',
    Proposition (..),
    HVec (..),
    FromBool (..),
    applyNAry,
    applyNAry',
    fromBool',

    -- * Conversion between equalities
    fromRefl,
    fromLeibniz,
    reflToLeibniz,
    leibnizToRefl,

    -- * Coercion
    coerce,
    coerceInner,
    coerce',
    withRefl,

    -- * Re-exported modules
    module Data.Proxy,
  )
where

import Data.Kind (Type)
import Data.Proxy
import Data.Type.Equality hiding (apply)
import Unsafe.Coerce

infix 4 :=:

type a :\/: b = Either a b

infixr 2 :\/:

type a :/\: b = (a, b)

infixr 3 :/\:

type (:=:) = (:~:)

data Leibniz a b = Leibniz {forall {k} (a :: k) (b :: k).
Leibniz a b -> forall (f :: k -> *). f a -> f b
apply :: forall f. f a -> f b}

leibnizToRefl :: Leibniz a b -> a :=: b
leibnizToRefl :: forall {k} (a :: k) (b :: k). Leibniz a b -> a :=: b
leibnizToRefl Leibniz a b
eq = forall {k} (a :: k) (b :: k).
Leibniz a b -> forall (f :: k -> *). f a -> f b
apply Leibniz a b
eq forall {k} (a :: k). a :~: a
Refl

fromLeibniz :: (Preorder eq) => Leibniz a b -> eq a b
fromLeibniz :: forall {k} (eq :: k -> k -> *) (a :: k) (b :: k).
Preorder eq =>
Leibniz a b -> eq a b
fromLeibniz Leibniz a b
eq = forall {k} (a :: k) (b :: k).
Leibniz a b -> forall (f :: k -> *). f a -> f b
apply Leibniz a b
eq (forall k (eq :: k -> k -> *) (proxy :: k -> *) (a :: k).
Preorder eq =>
proxy a -> eq a a
reflexivity forall {k} (t :: k). Proxy t
Proxy)

fromRefl :: (Preorder eq) => a :=: b -> eq a b
fromRefl :: forall {k} (eq :: k -> k -> *) (a :: k) (b :: k).
Preorder eq =>
(a :=: b) -> eq a b
fromRefl a :~: b
Refl = forall {k} (r :: k -> k -> *) (x :: k). Preorder r => r x x
reflexivity'

reflToLeibniz :: a :=: b -> Leibniz a b
reflToLeibniz :: forall {k} (a :: k) (b :: k). (a :=: b) -> Leibniz a b
reflToLeibniz a :~: b
Refl = forall {k} (a :: k) (b :: k).
(forall (f :: k -> *). f a -> f b) -> Leibniz a b
Leibniz forall a. a -> a
id

class Preorder (eq :: k -> k -> Type) where
  reflexivity :: proxy a -> eq a a
  transitivity :: eq a b -> eq b c -> eq a c

class Preorder eq => Equality (eq :: k -> k -> Type) where
  symmetry :: eq a b -> eq b a

instance Preorder (:=:) where
  {-# SPECIALIZE instance Preorder (:=:) #-}
  transitivity :: forall (a :: k) (b :: k) (c :: k).
(a :=: b) -> (b :=: c) -> a :=: c
transitivity a :~: b
Refl b :~: c
Refl = forall {k} (a :: k). a :~: a
Refl
  {-# INLINE [1] transitivity #-}

  reflexivity :: forall (proxy :: k -> *) (a :: k). proxy a -> a :=: a
reflexivity proxy a
_ = forall {k} (a :: k). a :~: a
Refl
  {-# INLINE [1] reflexivity #-}

instance Equality (:=:) where
  {-# SPECIALIZE instance Equality (:~:) #-}
  symmetry :: forall (a :: k) (b :: k). (a :=: b) -> b :=: a
symmetry a :~: b
Refl = forall {k} (a :: k). a :~: a
Refl
  {-# INLINE [1] symmetry #-}

instance Preorder (->) where
  reflexivity :: forall (proxy :: * -> *) a. proxy a -> a -> a
reflexivity proxy a
_ = forall a. a -> a
id
  transitivity :: forall a b c. (a -> b) -> (b -> c) -> a -> c
transitivity = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)

leibniz_refl :: Leibniz a a
leibniz_refl :: forall {k} (a :: k). Leibniz a a
leibniz_refl = forall {k} (a :: k) (b :: k).
(forall (f :: k -> *). f a -> f b) -> Leibniz a b
Leibniz forall a. a -> a
id

instance Preorder Leibniz where
  reflexivity :: forall (proxy :: k -> *) (a :: k). proxy a -> Leibniz a a
reflexivity proxy a
_ = forall {k} (a :: k). Leibniz a a
leibniz_refl
  transitivity :: forall (a :: k) (b :: k) (c :: k).
Leibniz a b -> Leibniz b c -> Leibniz a c
transitivity (Leibniz forall (f :: k -> *). f a -> f b
aEqb) (Leibniz forall (f :: k -> *). f b -> f c
bEqc) = forall {k} (a :: k) (b :: k).
(forall (f :: k -> *). f a -> f b) -> Leibniz a b
Leibniz forall a b. (a -> b) -> a -> b
$ forall (f :: k -> *). f b -> f c
bEqc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: k -> *). f a -> f b
aEqb

instance Equality Leibniz where
  symmetry :: forall (a :: k) (b :: k). Leibniz a b -> Leibniz b a
symmetry Leibniz a b
eq = forall {k} {k} (f :: k -> k -> *) (a :: k) (b :: k).
Flip f a b -> f b a
unFlip forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k) (b :: k).
Leibniz a b -> forall (f :: k -> *). f a -> f b
apply Leibniz a b
eq forall a b. (a -> b) -> a -> b
$ forall {k} {k} (f :: k -> k -> *) (a :: k) (b :: k).
f b a -> Flip f a b
Flip forall {k} (a :: k). Leibniz a a
leibniz_refl

newtype Flip f a b = Flip {forall {k} {k} (f :: k -> k -> *) (a :: k) (b :: k).
Flip f a b -> f b a
unFlip :: f b a}

data Reason eq x y where
  Because :: proxy y -> eq x y -> Reason eq x y

reflexivity' :: (Preorder r) => r x x
reflexivity' :: forall {k} (r :: k -> k -> *) (x :: k). Preorder r => r x x
reflexivity' = forall k (eq :: k -> k -> *) (proxy :: k -> *) (a :: k).
Preorder eq =>
proxy a -> eq a a
reflexivity forall {k} (t :: k). Proxy t
Proxy

by, because :: proxy y -> eq x y -> Reason eq x y
because :: forall {k} {k} (proxy :: k -> *) (y :: k) (eq :: k -> k -> *)
       (x :: k).
proxy y -> eq x y -> Reason eq x y
because = forall {k} {k} (proxy :: k -> *) (y :: k) (eq :: k -> k -> *)
       (x :: k).
proxy y -> eq x y -> Reason eq x y
Because
by :: forall {k} {k} (proxy :: k -> *) (y :: k) (eq :: k -> k -> *)
       (x :: k).
proxy y -> eq x y -> Reason eq x y
by = forall {k} {k} (proxy :: k -> *) (y :: k) (eq :: k -> k -> *)
       (x :: k).
proxy y -> eq x y -> Reason eq x y
Because

infixl 4 ===, =<=, =~=, =>=

infix 5 `Because`

infix 5 `because`

(=<=) :: Preorder r => r x y -> Reason r y z -> r x z
r x y
eq =<= :: forall {k} (r :: k -> k -> *) (x :: k) (y :: k) (z :: k).
Preorder r =>
r x y -> Reason r y z -> r x z
=<= (proxy z
_ `Because` r y z
eq') = forall k (eq :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Preorder eq =>
eq a b -> eq b c -> eq a c
transitivity r x y
eq r y z
eq'
{-# SPECIALIZE INLINE [1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}

(=>=) :: Preorder r => r y z -> Reason r x y -> r x z
r y z
eq =>= :: forall {k} (r :: k -> k -> *) (y :: k) (z :: k) (x :: k).
Preorder r =>
r y z -> Reason r x y -> r x z
=>= (proxy y
_ `Because` r x y
eq') = forall k (eq :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Preorder eq =>
eq a b -> eq b c -> eq a c
transitivity r x y
eq' r y z
eq
{-# SPECIALIZE INLINE [1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}

(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
=== :: forall {k} (eq :: k -> k -> *) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
(===) = forall {k} (r :: k -> k -> *) (x :: k) (y :: k) (z :: k).
Preorder r =>
r x y -> Reason r y z -> r x z
(=<=)
{-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}

(=~=) :: r x y -> proxy y -> r x y
r x y
eq =~= :: forall {k} {k} (r :: k -> k -> *) (x :: k) (y :: k)
       (proxy :: k -> *).
r x y -> proxy y -> r x y
=~= proxy y
_ = r x y
eq

start :: Preorder eq => proxy a -> eq a a
start :: forall {k} (eq :: k -> k -> *) (proxy :: k -> *) (a :: k).
Preorder eq =>
proxy a -> eq a a
start = forall k (eq :: k -> k -> *) (proxy :: k -> *) (a :: k).
Preorder eq =>
proxy a -> eq a a
reflexivity

byDefinition :: (Preorder eq) => eq a a
byDefinition :: forall {k} (r :: k -> k -> *) (x :: k). Preorder r => r x x
byDefinition = forall k (eq :: k -> k -> *) (proxy :: k -> *) (a :: k).
Preorder eq =>
proxy a -> eq a a
reflexivity forall {k} (t :: k). Proxy t
Proxy

admitted :: Reason eq x y
admitted :: forall {k} {k} (eq :: k -> k -> *) (x :: k) (y :: k). Reason eq x y
admitted = forall a. HasCallStack => a
undefined
{-# WARNING admitted "There are some goals left yet unproven." #-}

cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b
cong :: forall {k} {k} (f :: k -> k) (a :: k) (b :: k).
Proxy f -> (a :=: b) -> f a :=: f b
cong Proxy f
Proxy a :~: b
Refl = forall {k} (a :: k). a :~: a
Refl

cong' :: (pxy m -> pxy (f m)) -> a :=: b -> f a :=: f b
cong' :: forall {k} (pxy :: k -> *) (m :: k) (f :: k -> k) (a :: k)
       (b :: k).
(pxy m -> pxy (f m)) -> (a :=: b) -> f a :=: f b
cong' pxy m -> pxy (f m)
_ a :~: b
Refl = forall {k} (a :: k). a :~: a
Refl

{- | Type coercion. 'coerce' is using @unsafeCoerce a@.
 So, please, please do not provide the @undefined@ as the proof.
 Using this function instead of pattern-matching on equality proof,
 you can reduce the overhead introduced by run-time proof.
-}
coerceInner, coerce :: (a :=: b) -> f a -> f b
{-# DEPRECATED coerce "Use coerceInner instead" #-}
coerce :: forall {k} (a :: k) (b :: k) (f :: k -> *). (a :=: b) -> f a -> f b
coerce = forall {k} (a :: k) (b :: k) (f :: k -> *). (a :=: b) -> f a -> f b
coerceInner
{-# INLINE coerce #-}
coerceInner :: forall {k} (a :: k) (b :: k) (f :: k -> *). (a :=: b) -> f a -> f b
coerceInner a :=: b
_ = forall a b. a -> b
unsafeCoerce
{-# INLINE [1] coerceInner #-}

-- | Coercion for identity types.
coerce' :: a :=: b -> a -> b
coerce' :: forall a b. (a :=: b) -> a -> b
coerce' a :=: b
_ = forall a b. a -> b
unsafeCoerce
{-# INLINE [1] coerce' #-}

{-# RULES
"coerce/unsafeCoerce" [~1] forall xs.
  coerceInner xs =
    unsafeCoerce
"coerce'/unsafeCoerce" [~1] forall xs.
  coerce' xs =
    unsafeCoerce
  #-}

{- | Solves equality constraint without explicit coercion.
   It has the same effect as @'Data.Type.Equality.gcastWith'@,
   but some hacks is done to reduce runtime overhead.
-}
withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r
withRefl :: forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
withRefl a :~: b
_ = forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (forall a b. a -> b
unsafeCoerce (forall {k} (a :: k). a :~: a
Refl :: () :~: ()) :: a :~: b)

class Proposition (f :: k -> Type) where
  type OriginalProp (f :: k -> Type) (n :: k) :: Type
  unWrap :: f n -> OriginalProp f n
  wrap :: OriginalProp f n -> f n

data HVec (xs :: [Type]) where
  HNil :: HVec '[]
  (:-) :: x -> HVec xs -> HVec (x ': xs)

infixr 9 :-

type family (xs :: [Type]) :~> (a :: Type) :: Type where
  '[] :~> a = a
  (x ': xs) :~> a = x -> (xs :~> a)

infixr 1 :~>

data HVecView (xs :: [Type]) :: Type where
  HNilView :: HVecView '[]
  HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts)

deriving instance Show (HVecView xs)

class KnownTypeList (xs :: [Type]) where
  viewHVec' :: HVecView xs

instance KnownTypeList '[] where
  viewHVec' :: HVecView '[]
viewHVec' = HVecView '[]
HNilView

instance KnownTypeList ts => KnownTypeList (t ': ts) where
  viewHVec' :: HVecView (t : ts)
viewHVec' = forall x (xs :: [*]). Proxy x -> HVecView xs -> HVecView (x : xs)
HConsView forall {k} (t :: k). Proxy t
Proxy forall (xs :: [*]). KnownTypeList xs => HVecView xs
viewHVec'

newtype Magic (xs :: [Type]) a = Magic {forall (xs :: [*]) a. Magic xs a -> KnownTypeList xs => a
_viewHVec' :: KnownTypeList xs => a}

withKnownTypeList :: forall a xs. HVecView xs -> (KnownTypeList xs => a) -> a
withKnownTypeList :: forall a (xs :: [*]). HVecView xs -> (KnownTypeList xs => a) -> a
withKnownTypeList HVecView xs
xs KnownTypeList xs => a
f = (forall a b. a -> b
unsafeCoerce (forall (xs :: [*]) a. (KnownTypeList xs => a) -> Magic xs a
Magic KnownTypeList xs => a
f :: Magic xs a) :: HVecView xs -> a) HVecView xs
xs

apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c
apply' :: forall (ts :: [*]) c. HVecView ts -> (HVec ts -> c) -> ts :~> c
apply' HVecView ts
HNilView HVec ts -> c
f = HVec ts -> c
f HVec '[]
HNil
apply' (HConsView Proxy t
Proxy HVecView ts
ts) HVec ts -> c
f = \t
a ->
  forall a (xs :: [*]). HVecView xs -> (KnownTypeList xs => a) -> a
withKnownTypeList HVecView ts
ts forall a b. (a -> b) -> a -> b
$
    forall (ts :: [*]) c. HVecView ts -> (HVec ts -> c) -> ts :~> c
apply' HVecView ts
ts (\HVec ts
ts' -> HVec ts -> c
f forall a b. (a -> b) -> a -> b
$ t
a forall x (xs :: [*]). x -> HVec xs -> HVec (x : xs)
:- HVec ts
ts')

applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c
applyNAry :: forall (ts :: [*]) c.
KnownTypeList ts =>
(HVec ts -> c) -> ts :~> c
applyNAry = forall (ts :: [*]) c. HVecView ts -> (HVec ts -> c) -> ts :~> c
apply' (forall (xs :: [*]). KnownTypeList xs => HVecView xs
viewHVec' :: HVecView ts)

applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
applyNAry' :: forall (ts :: [*]) (proxy :: [*] -> *) (proxy' :: * -> *) c.
KnownTypeList ts =>
proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
applyNAry' proxy ts
_ proxy' c
_ = forall (ts :: [*]) c.
KnownTypeList ts =>
(HVec ts -> c) -> ts :~> c
applyNAry

class FromBool (c :: Type) where
  type Predicate c :: Bool
  type Args c :: [Type]
  fromBool :: Predicate c ~ 'True => HVec (Args c) -> c

fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ 'True) => proxy c -> Args c :~> c
fromBool' :: forall (proxy :: * -> *) c.
(KnownTypeList (Args c), FromBool c, Predicate c ~ 'True) =>
proxy c -> Args c :~> c
fromBool' proxy c
pxyc = forall (ts :: [*]) (proxy :: [*] -> *) (proxy' :: * -> *) c.
KnownTypeList ts =>
proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
applyNAry' (forall {k} (t :: k). Proxy t
Proxy :: Proxy (Args c)) proxy c
pxyc forall c. (FromBool c, Predicate c ~ 'True) => HVec (Args c) -> c
fromBool