{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Debug.RecoverRTTI.CheckSame (
samePrim
, sameClassifier_
, sameElem
, sameElems
) where
import Data.SOP
import Data.Type.Equality
import Debug.RecoverRTTI.Classifier
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)
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
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
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
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
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
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
go PrimClassifier a
_ PrimClassifier b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing
_checkAllCases :: PrimClassifier a -> ()
_checkAllCases :: PrimClassifier a -> ()
_checkAllCases = \case
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 -> ()
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 -> ()
PrimClassifier a
C_Value -> ()
PrimClassifier a
C_STRef -> ()
PrimClassifier a
C_TVar -> ()
PrimClassifier a
C_MVar -> ()
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 -> ()
PrimClassifier a
C_Fun -> ()
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)
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'
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
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
C_Prim{} -> ()
C_Other{} -> ()
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