{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE Rank2Types, ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}

-- * Leibniz equality can be made injective

module LeibnizInjective where

-- * Witness for the Leibniz equality

newtype EQU a b = EQU{subst:: forall c. c a -> c b}

-- * Leibniz equality is reflexive, symmetric and transitive
-- Here is the constructive proof

refl :: EQU a a
refl =  EQU id

-- * An Unusual `functor'
tran :: EQU a u -> EQU u b -> EQU a b
tran au ub = subst ub au
-- Why it works? We consider (EQU a u) as (EQU a) u,
-- and so instantiate c to be EQU a

-- To show symmetry, we have to ``swap'' the arguments
-- in EQU a b. We use the following auxiliary ``type function''

newtype FS b a = FS{unFS:: EQU a b}

symm :: EQU a b -> EQU b a
symm equ = unFS . subst equ . FS $ refl

-- Useful type-level lambdas, so to speak
newtype F1 t b a = F1{unF1:: EQU t (a->b)}

newtype F2 t a b = F2{unF2:: EQU t (a->b)}

eq_arr :: EQU a1 a2 -> EQU b1 b2 -> EQU (a1->b1) (a2->b2)
eq_arr a1a2 b1b2 = 
    unF2 . subst b1b2 . F2 . unF1 . subst a1a2 . F1 $ refl

-- We now attempt to show the converse of eq_arr

-- Injectivity
-- The original article used a projection type family Fst
-- type family Fst a :: *
-- type instance Fst (x->y) = x
-- type instance Fst (x,y)  = x
-- -- etc.
-- The following generalization (type family Arg) has been
-- suggested by Jeremy Yallop

type family Arg a :: *
type instance Arg (f a) = a

newtype ArgA a b = ArgA{unArgA :: EQU (Arg a) (Arg b)}

-- The general injectivity
-- f below cannot be a type synonym or a type function!
eq_f :: EQU (f a) (f1 b) -> EQU a b
eq_f eq = unArgA . subst eq $ ra
 where
 ra :: ArgA (f a) (f a)
 ra = ArgA refl

-- Why is this sound?

-- First of all, 'f' in eq_f above cannot be a synonym or a type function
type NI a = Bool
eq_ni :: EQU (NI Char) (NI Int)
eq_ni = refl

{-
eq_bad = eq_f eq_ni

    Couldn't match expected type `f a' against inferred type `Bool'
      Expected type: EQU (f a) (f b)
      Inferred type: EQU (NI Char) (NI Int)
    In the first argument of `eq_f', namely `eq_ni'
-}


-- For that reason, we cannot be arity-generic
type family Arg2 a :: *
type instance Arg2 (f a b) = a

newtype Arg2A a b = Arg2A{unArg2A :: EQU (Arg2 a) (Arg2 b)}

eq_f2 :: EQU (f a1 b1) (f1 a2 b2) -> EQU a1 a2
eq_f2 eq = unArg2A . subst eq $ ra
 where
 ra :: Arg2A (f a1 b1) (f a1 b1)
 ra = Arg2A refl

-- We now accomplish our task: `inverting' eq_arr

eq_arr2 :: EQU (a1->b1) (a2->b2) -> EQU b1 b2
eq_arr2 = eq_f 

eq_arr1 :: EQU (a1->b1) (a2->b2) -> EQU a1 a2
eq_arr1 = eq_f2

-- Incidentally, the injectivity patently demonstrates
-- that Leibniz equality is stronger than bijection:

data Bij a b = Bij (a->b) (b->a)

data FF a = FF				-- A forgetful functor

-- We may define a bijection between FF Int and FF Bool
bij_ff :: Bij (FF Int) (FF Bool)
bij_ff = Bij (\FF -> FF) (\FF -> FF)

-- But we can't derive Leibniz equality witness
-- EQU (FF Int) (FF Bool)
-- Being inter-convertible in any context is far more
-- demanding than being inter-convertible in the empty context.


-- Tests

-- Using the equality witness to extract values from
-- under an existential wrapper
data Wrap a = forall b. Wrap (EQU (a-> Bool) (b -> Bool)) (b->Bool)

tw1 :: Wrap Int
tw1 = Wrap refl (> 4)

{-
-- The following naive extraction of course does not work:
extract1 = 
    case tw1 of
     Wrap _ f -> f (5::Int)

    Couldn't match expected type `b' against inferred type `Int'
      `b' is a rigid type variable bound by
          the constructor `Wrap'
            at /home/oleg/langs/Haskell/LeibnizInjective.hs:71:5
    In the first argument of `f', namely `(5 :: Int)'

-}

-- But the extraction using the type equality witness convinces
-- the type checker.
newtype Id a = Id{unId:: a}

test = case tw1 of
	Wrap eq f -> f (cast_arg eq 5)
 where
 cast_arg :: EQU (a -> b1) (c -> b2) -> a -> c
 cast_arg eq n = unId . subst (eq_arr1 eq)  $ (Id n)