{-# LANGUAGE GADTs                #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE NoImplicitPrelude    #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExplicitNamespaces   #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UnicodeSyntax #-}

-- | Defines equality relation on types and provides
-- a simple interface to write proof on haskell types
module Relation.Equality where

import Data.Singletons (Sing)

infix 4 :≡

-- | Equality relation for types
data (a :: k) :≡ (b :: k) where
  Refl ∷ ∀ a. a :≡ a

-- | Operator version of "trans"
(∾) ∷ ∀ a b c. (a :≡ b) → (b :≡ c) → (a :≡ c)
(∾) = trans

-- | Congruence property
cong ∷ ∀ a b c f. (Sing a → Sing b) → (a :≡ c) → (f a :≡ f c)
cong _ Refl = Refl

-- | Transitive property
trans ∷ ∀ a b c. (a :≡ b) → (b :≡ c) → (a :≡ c)
trans Refl Refl = Refl

-- | Symmetric property
sym ∷ ∀ a b. (a :≡ b) → (b :≡ a)
sym Refl = Refl

-- | Type-safe cast using propositional equality
castWith ∷ ∀ a b. (a :≡ b) → a → b
castWith Refl x = x

-- | Generalized form of cast
gcastWith ∷ ∀ a b r. (a :≡ b) → ((a ~ b) ⇒ r) → r
gcastWith Refl x = x
