content: {-# LANGUAGE TypeOperators         #-}
  {-# LANGUAGE RankNTypes            #-}
  {-# LANGUAGE DataKinds             #-}
  {-# LANGUAGE PolyKinds             #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE TypeFamilies          #-}
  {-# LANGUAGE FlexibleContexts      #-}
  {-# LANGUAGE RoleAnnotations       #-}
  
  {-|
    Module      :  Theory.Equality
    Copyright   :  (c) Matt Noonan 2018
    License     :  BSD-style
    Maintainer  :  matt.noonan@gmail.com
    Portability :  portable
  -}
  
  module Theory.Equality
    (
      Equals, type (==)
  
    -- ** Substitutions and equational reasoning
    , (==.)
    , apply
    , substitute
    , substituteL
    , substituteR
  
    -- ** Relating to other forms of equality
    , same
    , reflectEq
    , propEq
    ) where
  
  import Data.Arguments
  import Data.The
  import Theory.Named
  import Logic.Proof (Proof, axiom)
  
  import Lawful
  
  import Unsafe.Coerce
  import Data.Type.Equality ((:~:)(..))
  
  {--------------------------------------------------
    Theory of equality
  --------------------------------------------------}
  
  -- | The @Equals@ relation is used to express equality between two entities.
  --   Given an equality, you are then able to substitute one side of the equality
  --   for the other, anywhere you please.
  newtype Equals x y = Equals Defn
  type role Equals nominal nominal
  
  -- | An infix alias for 'Equals'.
  type x == y = x `Equals` y
  infix 4 ==
  
  instance Argument (Equals x y) 0 where
    type GetArg (Equals x y) 0    = x
    type SetArg (Equals x y) 0 x' = Equals x' y
  
  instance Argument (Equals x y) 1 where
    type GetArg (Equals x y) 1    = y
    type SetArg (Equals x y) 1 y' = Equals x y'
  
  instance Argument (Equals x y) LHS where
    type GetArg (Equals x y) LHS    = x
    type SetArg (Equals x y) LHS x' = Equals x' y
  
  instance Argument (Equals x y) RHS where
    type GetArg (Equals x y) RHS    = y
    type SetArg (Equals x y) RHS y' = Equals x y'
  
  -- | Chain equalities, a la Liquid Haskell.
  (==.) :: Proof (x == y) -> Proof (y == z) -> Proof (x == z)
  _ ==. _ = axiom
  
  -- | Apply a function to both sides of an equality.
  apply :: forall f n x x'. (Argument f n, GetArg f n ~ x)
      => Arg n -> Proof (x == x') -> Proof (f == SetArg f n x')
  apply _ _ = axiom
  
  -- | Given a formula and an equality over one of its arguments,
  --   replace the left-hand side of the equality with the right-hand side.
  substitute :: (Argument f n, GetArg f n ~ x)
      => Arg n -> Proof (x == x') -> f -> Proof (SetArg f n x')
  substitute _ _ _ = axiom
  
  -- | Substitute @x'@ for @x@ under the function @f@, on the left-hand side
  --   of an equality.
  substituteL :: (Argument f n, GetArg f n ~ x)
      => Arg n -> Proof (x == x') -> Proof (f == g) -> Proof (SetArg f n x' == g)
  substituteL _ _ _ = axiom
  
  -- | Substitute @x'@ for @x@ under the function @f@, on the right-hand side
  --   of an equality.
  substituteR :: (Argument f n, GetArg f n ~ x)
      => Arg n -> Proof (x == x') -> Proof (g == f) -> Proof (g == SetArg f n x')
  substituteR _ _ _ = axiom
  
  {--------------------------------------------------
    Theory of equality
  --------------------------------------------------}
  
  -- | Test if the two named arguments are equal and, if so, produce a proof
  --   of equality for the names.
  same :: Lawful Eq a => (a ~~ x) -> (a ~~ y) -> Maybe (Proof (x == y))
  same (The x) (The y) = if x == y then Just axiom else Nothing
  
  {-| Reflect an equality between @x@ and @y@ into a propositional
      equality between the /types/ @x@ and @y@.
  
  @
  newtype Bob = Bob Defn
  
  bob :: Int ~~ Bob
  bob = defn 42
  
  needsBob :: (Int ~~ Bob) -> Int
  needsBob x = the x + the x
  
  isBob :: (Int ~~ name) -> Maybe (Proof (name == Bob))
  isBob = same x bob
  
  f :: (Int ~~ name) -> Int
  f x = case reflectEq \<$\> isBob x of
    Nothing   -> 17
    Just Refl -> needsBob x x
  @
  -}
  reflectEq :: Proof (x == y) -> (x :~: y)
  reflectEq _ = unsafeCoerce (Refl :: a :~: a)
  
  -- | Convert a propositional equality between the types @x@ and @y@
  --   into a proof of @x == y@.
  propEq :: (x :~: y) -> Proof (x == y)
  propEq _ = axiom
  