{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

module Debug.RecoverRTTI.CheckSame (
    -- * Check if two classifiers are the same
    samePrim
  , sameClassifier_
  , sameElem
  , sameElems
  ) where

import Data.SOP
import Data.Type.Equality

import Debug.RecoverRTTI.Classifier

{-------------------------------------------------------------------------------
  Equality check
-------------------------------------------------------------------------------}

samePrim :: PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)
samePrim :: forall a b. PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)
samePrim = forall a b. PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)
go
  where
    go :: PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)

    -- Primitive types
    go :: forall a b. PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)
go PrimClassifier a
C_Bool     PrimClassifier b
C_Bool     = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Char     PrimClassifier b
C_Char     = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Double   PrimClassifier b
C_Double   = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Float    PrimClassifier b
C_Float    = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Int      PrimClassifier b
C_Int      = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Int8     PrimClassifier b
C_Int8     = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Int16    PrimClassifier b
C_Int16    = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Int32    PrimClassifier b
C_Int32    = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Int64    PrimClassifier b
C_Int64    = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Integer  PrimClassifier b
C_Integer  = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Ordering PrimClassifier b
C_Ordering = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Unit     PrimClassifier b
C_Unit     = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Word     PrimClassifier b
C_Word     = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Word8    PrimClassifier b
C_Word8    = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Word16   PrimClassifier b
C_Word16   = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Word32   PrimClassifier b
C_Word32   = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Word64   PrimClassifier b
C_Word64   = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl

    -- String types

    go PrimClassifier a
C_String      PrimClassifier b
C_String      = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_BS_Strict   PrimClassifier b
C_BS_Strict   = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_BS_Lazy     PrimClassifier b
C_BS_Lazy     = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_BS_Short    PrimClassifier b
C_BS_Short    = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Text_Strict PrimClassifier b
C_Text_Strict = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Text_Lazy   PrimClassifier b
C_Text_Lazy   = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl

    -- Aeson

    go PrimClassifier a
C_Value PrimClassifier b
C_Value = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl

    -- Reference cells

    go PrimClassifier a
C_STRef PrimClassifier b
C_STRef = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_TVar  PrimClassifier b
C_TVar  = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_MVar  PrimClassifier b
C_MVar  = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl

    -- Containers without type arguments

    go PrimClassifier a
C_IntSet            PrimClassifier b
C_IntSet            = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Prim_ArrayM       PrimClassifier b
C_Prim_ArrayM       = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Vector_Storable   PrimClassifier b
C_Vector_Storable   = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Vector_StorableM  PrimClassifier b
C_Vector_StorableM  = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Vector_Primitive  PrimClassifier b
C_Vector_Primitive  = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go PrimClassifier a
C_Vector_PrimitiveM PrimClassifier b
C_Vector_PrimitiveM = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl

    -- Functions

    go PrimClassifier a
C_Fun PrimClassifier b
C_Fun = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl

    -- Not equal
    go PrimClassifier a
_ PrimClassifier b
_ = forall a. Maybe a
Nothing

    _checkAllCases :: PrimClassifier a -> ()
    _checkAllCases :: forall a. PrimClassifier a -> ()
_checkAllCases = \case
        -- Primitive types

        PrimClassifier a
C_Bool     -> ()
        PrimClassifier a
C_Char     -> ()
        PrimClassifier a
C_Double   -> ()
        PrimClassifier a
C_Float    -> ()
        PrimClassifier a
C_Int      -> ()
        PrimClassifier a
C_Int8     -> ()
        PrimClassifier a
C_Int16    -> ()
        PrimClassifier a
C_Int32    -> ()
        PrimClassifier a
C_Int64    -> ()
        PrimClassifier a
C_Integer  -> ()
        PrimClassifier a
C_Ordering -> ()
        PrimClassifier a
C_Unit     -> ()
        PrimClassifier a
C_Word     -> ()
        PrimClassifier a
C_Word8    -> ()
        PrimClassifier a
C_Word16   -> ()
        PrimClassifier a
C_Word32   -> ()
        PrimClassifier a
C_Word64   -> ()

        -- String types

        PrimClassifier a
C_String      -> ()
        PrimClassifier a
C_BS_Strict   -> ()
        PrimClassifier a
C_BS_Lazy     -> ()
        PrimClassifier a
C_BS_Short    -> ()
        PrimClassifier a
C_Text_Strict -> ()
        PrimClassifier a
C_Text_Lazy   -> ()

        -- Aeson

        PrimClassifier a
C_Value -> ()

        -- Reference cells

        PrimClassifier a
C_STRef -> ()
        PrimClassifier a
C_TVar  -> ()
        PrimClassifier a
C_MVar  -> ()

        -- Containers without type arguments

        PrimClassifier a
C_IntSet            -> ()
        PrimClassifier a
C_Prim_ArrayM       -> ()
        PrimClassifier a
C_Vector_Storable   -> ()
        PrimClassifier a
C_Vector_StorableM  -> ()
        PrimClassifier a
C_Vector_Primitive  -> ()
        PrimClassifier a
C_Vector_PrimitiveM -> ()

        -- Functions

        PrimClassifier a
C_Fun -> ()

-- | Check that two classifiers are the same
--
-- If they are the same, additionally return a proof that that means the
-- /types/ they classify must be equal (note that equality on the classifiers
-- is strictly stronger than equality on the types: for example, non-empty
-- and empty lists have different classifiers, but classify the same type).
--
-- This is defined on the general type 'Classifier_' rather than on 'Classifier'
-- because different user-defined types may both be classified as @UserDefined@
-- yet not be equal to each other
sameClassifier_ :: forall o.
     (forall a b. o a -> o b -> Maybe (a :~: b))
  -> (forall a b. Classifier_ o a -> Classifier_ o b -> Maybe (a :~: b))
sameClassifier_ :: forall (o :: * -> *).
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall a b.
   Classifier_ o a -> Classifier_ o b -> Maybe (a :~: b)
sameClassifier_ forall a b. o a -> o b -> Maybe (a :~: b)
sameOther = forall a b. Classifier_ o a -> Classifier_ o b -> Maybe (a :~: b)
go
  where
    go :: Classifier_ o a -> Classifier_ o b -> Maybe (a :~: b)

    -- User-defined and primitive types
    go :: forall a b. Classifier_ o a -> Classifier_ o b -> Maybe (a :~: b)
go (C_Prim  PrimClassifier a
c) (C_Prim  PrimClassifier b
c') = forall a b. PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)
samePrim  PrimClassifier a
c PrimClassifier b
c'
    go (C_Other o a
c) (C_Other o b
c') = forall a b. o a -> o b -> Maybe (a :~: b)
sameOther o a
c o b
c'

    -- Compound
    go (C_Maybe        Elems o '[a]
c) (C_Maybe        Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_Either       Elems o '[a, b]
c) (C_Either       Elems o '[a, b]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a, b]
c Elems o '[a, b]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_List         Elems o '[a]
c) (C_List         Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_Ratio        Elems o '[a]
c) (C_Ratio        Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_Set          Elems o '[a]
c) (C_Set          Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_Map          Elems o '[a, b]
c) (C_Map          Elems o '[a, b]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a, b]
c Elems o '[a, b]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_IntMap       Elems o '[a]
c) (C_IntMap       Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_Sequence     Elems o '[a]
c) (C_Sequence     Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_Tree         Elems o '[a]
c) (C_Tree         Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_HashSet      Elems o '[a]
c) (C_HashSet      Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_HashMap      Elems o '[a, b]
c) (C_HashMap      Elems o '[a, b]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a, b]
c Elems o '[a, b]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_HM_Array     Elems o '[a]
c) (C_HM_Array     Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_Prim_Array   Elems o '[a]
c) (C_Prim_Array   Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_Vector_Boxed Elems o '[a]
c) (C_Vector_Boxed Elems o '[a]
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o '[a]
c Elems o '[a]
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl
    go (C_Tuple        Elems o xs
c) (C_Tuple        Elems o xs
c') = forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elems o xs
c Elems o xs
c' forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl

    -- No match
    go Classifier_ o a
_ Classifier_ o b
_ = forall a. Maybe a
Nothing
      where
        _checkAllCases :: Classifier_ o a -> ()
        _checkAllCases :: forall a. Classifier_ o a -> ()
_checkAllCases = \case
           -- Primitive and user-defined
           C_Prim{}  -> ()
           C_Other{} -> ()

           -- Compound
           C_Maybe{}        -> ()
           C_Either{}       -> ()
           C_List{}         -> ()
           C_Ratio{}        -> ()
           C_Set{}          -> ()
           C_Map{}          -> ()
           C_IntMap{}       -> ()
           C_Sequence{}     -> ()
           C_Tree{}         -> ()
           C_HashSet{}      -> ()
           C_HashMap{}      -> ()
           C_HM_Array{}     -> ()
           C_Prim_Array{}   -> ()
           C_Vector_Boxed{} -> ()
           C_Tuple{}        -> ()

sameElem :: forall o.
     (forall a b. o a -> o b -> Maybe (a :~: b))
  -> (forall a b. Elem o a -> Elem o b -> Maybe (a :~: b))
sameElem :: forall (o :: * -> *).
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall a b. Elem o a -> Elem o b -> Maybe (a :~: b)
sameElem forall a b. o a -> o b -> Maybe (a :~: b)
sameOther = forall a b. Elem o a -> Elem o b -> Maybe (a :~: b)
go
  where
    go :: Elem o a -> Elem o b -> Maybe (a :~: b)
    go :: forall a b. Elem o a -> Elem o b -> Maybe (a :~: b)
go Elem o a
NoElem     Elem o b
NoElem   = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    go Elem o a
NoElem    (Elem Classifier_ o b
_)  = forall a. Maybe a
Nothing
    go (Elem Classifier_ o a
_)   Elem o b
NoElem   = forall a. Maybe a
Nothing
    go (Elem Classifier_ o a
ca) (Elem Classifier_ o b
cb) = forall (o :: * -> *).
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall a b.
   Classifier_ o a -> Classifier_ o b -> Maybe (a :~: b)
sameClassifier_ forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Classifier_ o a
ca Classifier_ o b
cb

sameElems :: forall o r.
     (forall a b. o a -> o b -> Maybe (a :~: b))
  -> (forall as bs. Elems o as -> Elems o bs -> (as ~ bs => r) -> Maybe r)
sameElems :: forall (o :: * -> *) r.
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall (as :: [*]) (bs :: [*]).
   Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
sameElems forall a b. o a -> o b -> Maybe (a :~: b)
sameOther = forall (as :: [*]) (bs :: [*]).
Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
go
  where
    go :: Elems o as -> Elems o bs -> (as ~ bs => r) -> Maybe r
    go :: forall (as :: [*]) (bs :: [*]).
Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
go (Elems NP (Elem o) as
Nil)       (Elems NP (Elem o) bs
Nil)         (as ~ bs) => r
k = forall a. a -> Maybe a
Just (as ~ bs) => r
k
    go (Elems NP (Elem o) as
Nil)       (Elems (Elem o x
_  :* NP (Elem o) xs
_))   (as ~ bs) => r
_ = forall a. Maybe a
Nothing
    go (Elems (Elem o x
_ :* NP (Elem o) xs
_))  (Elems NP (Elem o) bs
Nil)         (as ~ bs) => r
_ = forall a. Maybe a
Nothing
    go (Elems (Elem o x
c :* NP (Elem o) xs
cs)) (Elems (Elem o x
c' :* NP (Elem o) xs
cs')) (as ~ bs) => r
k = do
        x :~: x
Refl <- forall (o :: * -> *).
(forall a b. o a -> o b -> Maybe (a :~: b))
-> forall a b. Elem o a -> Elem o b -> Maybe (a :~: b)
sameElem forall a b. o a -> o b -> Maybe (a :~: b)
sameOther Elem o x
c Elem o x
c'
        forall (as :: [*]) (bs :: [*]).
Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
go (forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems NP (Elem o) xs
cs) (forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems NP (Elem o) xs
cs') (as ~ bs) => r
k