{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

{-|

Propositions and combinators for conveniently constructing them.

-}
module Language.Expression.Prop
  (
    -- * Proposition Types
    Prop
  , Prop'
    -- * DSL
  , expr
  , plit
  , pnot
  , (*&&)
  , (*||)
  , (*->)
  , (*<->)
  , propAnd
  , propOr
    -- * HTraversable
  , LogicOp(..)
  ) where

import           Control.Applicative        (liftA2)
import           Data.List                  (foldl')
-- import           Data.Typeable

-- import           Data.Functor.Classes
import           Data.Functor.Identity

import           Data.SBV

import           Language.Expression
import           Language.Expression.Choice
import           Language.Expression.Pretty
import           Language.Expression.Util

-- | Propositions over general expressions.
type Prop = HFree LogicOp

-- | Propositions over expressions with the given list of operators.
type Prop' ops v = Prop (HFree' ops v)

--------------------------------------------------------------------------------
--  DSL
--------------------------------------------------------------------------------

infixl 3 *&&
infixl 2 *||
infixr 1 *->
infix 1 *<->

-- | Lift an expression into the land of propositions.
expr :: expr a -> Prop expr a
expr :: expr a -> Prop expr a
expr = expr a -> Prop expr a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
t a -> HFree h t a
HPure

plit :: Bool -> Prop expr Bool
plit :: Bool -> Prop expr Bool
plit = LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool)
-> (Bool -> LogicOp (HFree LogicOp expr) Bool)
-> Bool
-> Prop expr Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> LogicOp (HFree LogicOp expr) Bool
forall (t :: * -> *). Bool -> LogicOp t Bool
LogLit

pnot :: Prop expr Bool -> Prop expr Bool
pnot :: Prop expr Bool -> Prop expr Bool
pnot = LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool)
-> (Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool)
-> Prop expr Bool
-> Prop expr Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool
forall (t :: * -> *). t Bool -> LogicOp t Bool
LogNot

(*&&) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool
(*&&) = LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool)
-> (Prop expr Bool
    -> Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool)
-> Prop expr Bool
-> Prop expr Bool
-> Prop expr Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... Prop expr Bool
-> Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool
forall (t :: * -> *). t Bool -> t Bool -> LogicOp t Bool
LogAnd

(*||) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*|| :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool
(*||) = LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool)
-> (Prop expr Bool
    -> Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool)
-> Prop expr Bool
-> Prop expr Bool
-> Prop expr Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... Prop expr Bool
-> Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool
forall (t :: * -> *). t Bool -> t Bool -> LogicOp t Bool
LogOr

(*->) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*-> :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool
(*->) = LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool)
-> (Prop expr Bool
    -> Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool)
-> Prop expr Bool
-> Prop expr Bool
-> Prop expr Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... Prop expr Bool
-> Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool
forall (t :: * -> *). t Bool -> t Bool -> LogicOp t Bool
LogImpl

(*<->) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*<-> :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool
(*<->) = LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (LogicOp (HFree LogicOp expr) Bool -> Prop expr Bool)
-> (Prop expr Bool
    -> Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool)
-> Prop expr Bool
-> Prop expr Bool
-> Prop expr Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... Prop expr Bool
-> Prop expr Bool -> LogicOp (HFree LogicOp expr) Bool
forall (t :: * -> *). t Bool -> t Bool -> LogicOp t Bool
LogEquiv

propAnd :: [Prop expr Bool] -> Prop expr Bool
propAnd :: [Prop expr Bool] -> Prop expr Bool
propAnd []       = Bool -> Prop expr Bool
forall (expr :: * -> *). Bool -> Prop expr Bool
plit Bool
True
propAnd (Prop expr Bool
x : [Prop expr Bool]
xs) = (Prop expr Bool -> Prop expr Bool -> Prop expr Bool)
-> Prop expr Bool -> [Prop expr Bool] -> Prop expr Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Prop expr Bool -> Prop expr Bool -> Prop expr Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
(*&&) Prop expr Bool
x [Prop expr Bool]
xs

propOr :: [Prop expr Bool] -> Prop expr Bool
propOr :: [Prop expr Bool] -> Prop expr Bool
propOr []       = Bool -> Prop expr Bool
forall (expr :: * -> *). Bool -> Prop expr Bool
plit Bool
False
propOr (Prop expr Bool
x : [Prop expr Bool]
xs) = (Prop expr Bool -> Prop expr Bool -> Prop expr Bool)
-> Prop expr Bool -> [Prop expr Bool] -> Prop expr Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Prop expr Bool -> Prop expr Bool -> Prop expr Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
(*||) Prop expr Bool
x [Prop expr Bool]
xs


--------------------------------------------------------------------------------
--  The HTraversable
--------------------------------------------------------------------------------

-- | Logical operations
data LogicOp t a where
  LogLit :: Bool -> LogicOp t Bool
  LogNot :: t Bool -> LogicOp t Bool
  LogAnd :: t Bool -> t Bool -> LogicOp t Bool
  LogOr :: t Bool -> t Bool -> LogicOp t Bool
  LogImpl :: t Bool -> t Bool -> LogicOp t Bool
  LogEquiv :: t Bool -> t Bool -> LogicOp t Bool

instance HFunctor LogicOp
instance HTraversable LogicOp where
  htraverse :: (forall b. t b -> f (t' b)) -> LogicOp t a -> f (LogicOp t' a)
htraverse forall b. t b -> f (t' b)
f = \case
    LogLit Bool
b -> LogicOp t' Bool -> f (LogicOp t' Bool)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LogicOp t' Bool -> f (LogicOp t' Bool))
-> LogicOp t' Bool -> f (LogicOp t' Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> LogicOp t' Bool
forall (t :: * -> *). Bool -> LogicOp t Bool
LogLit Bool
b
    LogNot t Bool
x -> t' Bool -> LogicOp t' Bool
forall (t :: * -> *). t Bool -> LogicOp t Bool
LogNot (t' Bool -> LogicOp t' Bool) -> f (t' Bool) -> f (LogicOp t' Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
x
    LogAnd t Bool
x t Bool
y -> t' Bool -> t' Bool -> LogicOp t' Bool
forall (t :: * -> *). t Bool -> t Bool -> LogicOp t Bool
LogAnd (t' Bool -> t' Bool -> LogicOp t' Bool)
-> f (t' Bool) -> f (t' Bool -> LogicOp t' Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
x f (t' Bool -> LogicOp t' Bool)
-> f (t' Bool) -> f (LogicOp t' Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
y
    LogOr t Bool
x t Bool
y -> t' Bool -> t' Bool -> LogicOp t' Bool
forall (t :: * -> *). t Bool -> t Bool -> LogicOp t Bool
LogOr (t' Bool -> t' Bool -> LogicOp t' Bool)
-> f (t' Bool) -> f (t' Bool -> LogicOp t' Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
x f (t' Bool -> LogicOp t' Bool)
-> f (t' Bool) -> f (LogicOp t' Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
y
    LogImpl t Bool
x t Bool
y -> t' Bool -> t' Bool -> LogicOp t' Bool
forall (t :: * -> *). t Bool -> t Bool -> LogicOp t Bool
LogImpl (t' Bool -> t' Bool -> LogicOp t' Bool)
-> f (t' Bool) -> f (t' Bool -> LogicOp t' Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
x f (t' Bool -> LogicOp t' Bool)
-> f (t' Bool) -> f (LogicOp t' Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
y
    LogEquiv t Bool
x t Bool
y -> t' Bool -> t' Bool -> LogicOp t' Bool
forall (t :: * -> *). t Bool -> t Bool -> LogicOp t Bool
LogEquiv (t' Bool -> t' Bool -> LogicOp t' Bool)
-> f (t' Bool) -> f (t' Bool -> LogicOp t' Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
x f (t' Bool -> LogicOp t' Bool)
-> f (t' Bool) -> f (LogicOp t' Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
y

instance HFoldableAt Identity LogicOp where
  hfoldMap :: (forall b. t b -> Identity b) -> LogicOp t a -> Identity a
hfoldMap = (LogicOp Identity a -> Identity a)
-> (forall b. t b -> Identity b) -> LogicOp t a -> Identity a
forall u (h :: (u -> *) -> u -> *) (k :: u -> *) (a :: u)
       (t :: u -> *).
HFunctor h =>
(h k a -> k a) -> (forall (b :: u). t b -> k b) -> h t a -> k a
implHfoldMap ((LogicOp Identity a -> Identity a)
 -> (forall b. t b -> Identity b) -> LogicOp t a -> Identity a)
-> (LogicOp Identity a -> Identity a)
-> (forall b. t b -> Identity b)
-> LogicOp t a
-> Identity a
forall a b. (a -> b) -> a -> b
$ \case
    LogLit Bool
b -> Bool -> Identity Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
b
    LogNot Identity Bool
x -> Bool -> Bool
not (Bool -> Bool) -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Identity Bool
x
    LogAnd Identity Bool
x Identity Bool
y -> (Bool -> Bool -> Bool)
-> Identity Bool -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) Identity Bool
x Identity Bool
y
    LogOr Identity Bool
x Identity Bool
y -> (Bool -> Bool -> Bool)
-> Identity Bool -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(||) Identity Bool
x Identity Bool
y
    LogImpl Identity Bool
x Identity Bool
y -> (Bool -> Bool -> Bool)
-> Identity Bool -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(||) (Bool -> Bool
not (Bool -> Bool) -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Identity Bool
x) Identity Bool
y
    LogEquiv Identity Bool
x Identity Bool
y -> (Bool -> Bool -> Bool)
-> Identity Bool -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) ((Bool -> Bool -> Bool)
-> Identity Bool -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(||) (Bool -> Bool
not (Bool -> Bool) -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Identity Bool
x) Identity Bool
y) ((Bool -> Bool -> Bool)
-> Identity Bool -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(||) (Bool -> Bool
not (Bool -> Bool) -> Identity Bool -> Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Identity Bool
y) Identity Bool
x)

instance HFoldableAt SBV LogicOp where
  hfoldMap :: (forall b. t b -> SBV b) -> LogicOp t a -> SBV a
hfoldMap = (LogicOp SBV a -> SBV a)
-> (forall b. t b -> SBV b) -> LogicOp t a -> SBV a
forall u (h :: (u -> *) -> u -> *) (k :: u -> *) (a :: u)
       (t :: u -> *).
HFunctor h =>
(h k a -> k a) -> (forall (b :: u). t b -> k b) -> h t a -> k a
implHfoldMap ((LogicOp SBV a -> SBV a)
 -> (forall b. t b -> SBV b) -> LogicOp t a -> SBV a)
-> (LogicOp SBV a -> SBV a)
-> (forall b. t b -> SBV b)
-> LogicOp t a
-> SBV a
forall a b. (a -> b) -> a -> b
$ \case
    LogLit Bool
b -> Bool -> SBool
fromBool Bool
b
    LogNot SBool
x -> SBool -> SBool
sNot SBool
x
    LogAnd SBool
x SBool
y -> SBool
x SBool -> SBool -> SBool
.&& SBool
y
    LogOr SBool
x SBool
y -> SBool
x SBool -> SBool -> SBool
.|| SBool
y
    LogImpl SBool
x SBool
y -> SBool
x SBool -> SBool -> SBool
.=> SBool
y
    LogEquiv SBool
x SBool
y -> SBool
x SBool -> SBool -> SBool
.<=> SBool
y

-- instance HEq LogicOp where
--   liftHEq _ _ (LogLit x) (LogLit y) = x == y
--   liftHEq le _ (LogNot x) (LogNot y) = le svEq x y
--   liftHEq le _ (LogAnd x1 x2) (LogAnd y1 y2) = le svEq x1 y1 && le svEq x2 y2
--   liftHEq le _ (LogOr x1 x2) (LogOr y1 y2) = le svEq x1 y1 && le svEq x2 y2
--   liftHEq le _ (LogImpl x1 x2) (LogImpl y1 y2) = le svEq x1 y1 && le svEq x2 y2
--   liftHEq le _ (LogEquiv x1 x2) (LogEquiv y1 y2) = le svEq x1 y1 && le svEq x2 y2
--   liftHEq _ _ _ _ = False

-- instance (Eq1 t) => Eq1 (LogicOp t) where liftEq = liftLiftEq

-- instance (Eq a, Eq1 t) => Eq (LogicOp t a) where (==) = eq1

instance Pretty2 LogicOp where
  prettys2Prec :: Int -> LogicOp t a -> ShowS
prettys2Prec Int
p = \case
    LogLit Bool
True -> \String
r -> String
"T" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
r
    LogLit Bool
False -> \String
r -> String
"F" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
r
    LogNot t Bool
x -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
8) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"¬ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
9 t Bool
x
    LogAnd t Bool
x t Bool
y ->
      Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
4 t Bool
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ∧ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
4 t Bool
y
    LogOr  t Bool
x t Bool
y ->
      Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
3 t Bool
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ∨ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
3 t Bool
y
    LogImpl  t Bool
x t Bool
y ->
      Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
2 t Bool
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" -> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
2 t Bool
y
    LogEquiv  t Bool
x t Bool
y ->
      Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
1 t Bool
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" <-> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
1 t Bool
y

--------------------------------------------------------------------------------
--  Internal Combinators
--------------------------------------------------------------------------------

-- svEq :: (Typeable a, Typeable b, Eq a) => a -> b -> Bool
-- svEq (x :: a) (y :: b)
--   | Just Refl <- eqT :: Maybe (a :~: b) = x == y
--   | otherwise = False