module Data.Type.Witness.General.TestHetEquality
    ( (:~~:)(..)
    , withHRefl
    , hetHomoEq
    , TestHetEquality(..)
    , HetEqual(..)
    ) where

import Import

withHRefl :: forall ka (a :: ka) kb (b :: kb) (r :: Type). a :~~: b -> ((a ~~ b) => r) -> r
withHRefl :: forall ka (a :: ka) kb (b :: kb) r.
(a :~~: b) -> ((a ~~ b) => r) -> r
withHRefl a :~~: b
HRefl (a ~~ b) => r
r = (a ~~ b) => r
r

-- | somewhat awkwardly named
hetHomoEq :: forall (k :: Type) (a :: k) (b :: k). a :~~: b -> a :~: b
hetHomoEq :: forall k (a :: k) (b :: k). (a :~~: b) -> a :~: b
hetHomoEq a :~~: b
HRefl = forall {k} (a :: k). a :~: a
Refl

class TestHetEquality (w :: forall k. k -> Type) where
    testHetEquality :: forall (ka :: Type) (a :: ka) (kb :: Type) (b :: kb). w a -> w b -> Maybe (a :~~: b)

-- | Equivalent to ':~~:', but can be made an instance of 'TestHetEquality'
type HetEqual :: forall ka. ka -> forall kb. kb -> Type
data HetEqual a b where
    HetRefl :: forall k (a :: k). HetEqual a a

instance forall k (a :: k). TestHetEquality (HetEqual a) where
    testHetEquality :: forall ka (a :: ka) kb (b :: kb).
HetEqual a a -> HetEqual a b -> Maybe (a :~~: b)
testHetEquality HetEqual a a
HetRefl HetEqual a b
HetRefl = forall a. a -> Maybe a
Just forall {k1} (a :: k1). a :~~: a
HRefl