{-# 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 :: PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)
samePrim = PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)
forall a b. PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)
go
  where
    go :: PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)

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

    -- String types

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

    -- Aeson

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

    -- Reference cells

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

    -- Containers without type arguments

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

    -- Functions

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

    -- Not equal
    go PrimClassifier a
_ PrimClassifier b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

    _checkAllCases :: PrimClassifier a -> ()
    _checkAllCases :: 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 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 -> Classifier_ o b -> Maybe (a :~: b)
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 :: Classifier_ o a -> Classifier_ o b -> Maybe (a :~: b)
go (C_Prim  PrimClassifier a
c) (C_Prim  PrimClassifier b
c') = PrimClassifier a -> PrimClassifier b -> Maybe (a :~: b)
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') = o a -> o b -> Maybe (a :~: b)
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 a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => 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 a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a, b]
-> Elems o '[a, b]
-> (('[a, b] ~ '[a, b]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a, b] ~ '[a, b]) => a :~: b) -> Maybe (a :~: b))
-> (('[a, b] ~ '[a, b]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[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 a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => a :~: b
forall k (a :: k). a :~: a
Refl
    go (C_Ratio        Elems o '[a]
c) (C_Ratio        Elems o '[a]
c') = (forall a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => a :~: b
forall k (a :: k). a :~: a
Refl
    go (C_Set          Elems o '[a]
c) (C_Set          Elems o '[a]
c') = (forall a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => 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 a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a, b]
-> Elems o '[a, b]
-> (('[a, b] ~ '[a, b]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a, b] ~ '[a, b]) => a :~: b) -> Maybe (a :~: b))
-> (('[a, b] ~ '[a, b]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[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 a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => a :~: b
forall k (a :: k). a :~: a
Refl
    go (C_Sequence     Elems o '[a]
c) (C_Sequence     Elems o '[a]
c') = (forall a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => a :~: b
forall k (a :: k). a :~: a
Refl
    go (C_Tree         Elems o '[a]
c) (C_Tree         Elems o '[a]
c') = (forall a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => a :~: b
forall k (a :: k). a :~: a
Refl
    go (C_HashSet      Elems o '[a]
c) (C_HashSet      Elems o '[a]
c') = (forall a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => 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 a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a, b]
-> Elems o '[a, b]
-> (('[a, b] ~ '[a, b]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a, b] ~ '[a, b]) => a :~: b) -> Maybe (a :~: b))
-> (('[a, b] ~ '[a, b]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[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 a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => 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 a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => 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 a b. o a -> o b -> Maybe (a :~: b))
-> Elems o '[a]
-> Elems o '[a]
-> (('[a] ~ '[a]) => a :~: b)
-> Maybe (a :~: b)
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' ((('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b))
-> (('[a] ~ '[a]) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ ('[a] ~ '[a]) => a :~: b
forall k (a :: k). a :~: a
Refl
    go (C_Tuple        Elems o xs
c) (C_Tuple        Elems o xs
c') = (forall a b. o a -> o b -> Maybe (a :~: b))
-> Elems o xs
-> Elems o xs
-> ((xs ~ xs) => a :~: b)
-> Maybe (a :~: b)
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' (((xs ~ xs) => a :~: b) -> Maybe (a :~: b))
-> ((xs ~ xs) => a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ (xs ~ xs) => a :~: b
forall k (a :: k). a :~: a
Refl

    -- No match
    go Classifier_ o a
_ Classifier_ o b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing
      where
        _checkAllCases :: Classifier_ o a -> ()
        _checkAllCases :: 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 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 a -> Elem o b -> Maybe (a :~: b)
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 :: Elem o a -> Elem o b -> Maybe (a :~: b)
go Elem o a
NoElem     Elem o b
NoElem   = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
    go Elem o a
NoElem    (Elem Classifier_ o b
_)  = Maybe (a :~: b)
forall a. Maybe a
Nothing
    go (Elem Classifier_ o a
_)   Elem o b
NoElem   = Maybe (a :~: b)
forall a. Maybe a
Nothing
    go (Elem Classifier_ o a
ca) (Elem Classifier_ o b
cb) = (forall a b. o a -> o b -> Maybe (a :~: b))
-> Classifier_ o a -> Classifier_ o b -> Maybe (a :~: b)
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 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 as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
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 :: 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 = r -> Maybe r
forall a. a -> Maybe a
Just r
(as ~ bs) => r
k
    go (Elems NP (Elem o) as
Nil)       (Elems (Elem o x
_  :* NP (Elem o) xs
_))   (as ~ bs) => r
_ = Maybe r
forall a. Maybe a
Nothing
    go (Elems (Elem o x
_ :* NP (Elem o) xs
_))  (Elems NP (Elem o) bs
Nil)         (as ~ bs) => r
_ = Maybe 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 a b. o a -> o b -> Maybe (a :~: b))
-> Elem o x -> Elem o x -> Maybe (x :~: x)
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'
        Elems o xs -> Elems o xs -> ((xs ~ xs) => r) -> Maybe r
forall (as :: [*]) (bs :: [*]).
Elems o as -> Elems o bs -> ((as ~ bs) => r) -> Maybe r
go (NP (Elem o) xs -> Elems o xs
forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems NP (Elem o) xs
cs) (NP (Elem o) xs -> Elems o xs
forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems NP (Elem o) xs
cs') (as ~ bs) => r
(xs ~ xs) => r
k