https://twitter.com/kazu_yamamoto/status/798776602855256065

ET.agda

module ET where

open import Data.Maybe                                                                                                     
open import Data.Nat
open import Data.Bool using (Bool; true)
open import Data.Product using (∃; _,_; _×_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (Dec; yes; no)

data TypeRep : Set where
  BoolTypeRep : TypeRep
  NatTypeRep : TypeRep

Typeable : TypeRep → Set
Typeable BoolTypeRep = Bool
Typeable NatTypeRep = ℕ

testEquality : (a b : TypeRep) -> Dec (a ≡ b)
testEquality BoolTypeRep BoolTypeRep = yes refl
testEquality BoolTypeRep NatTypeRep = no (λ ())
testEquality NatTypeRep BoolTypeRep = no (λ ())
testEquality NatTypeRep NatTypeRep = yes refl

data T a : Set where
  unT : a → T a

data ET' (a : TypeRep) : Set where
  unET' : T (Typeable a) → ET' a

ET = ∃ ET'

foo : {a : Set} -> T a -> T a -> Bool
foo _ _ = true

bar : ET → ET → Maybe Bool
bar (proj₁ , proj₂) (proj₃ , proj₄) with testEquality proj₁ proj₃
bar (proj₁ , unET' x) (.proj₁ , unET' x₁) | yes refl = just (foo x x₁)
bar (proj₁ , proj₂) (proj₃ , proj₄) | no ¬p = nothing -- different type !                

a : ET
a = NatTypeRep , unET' (unT 1)

b : ET
b = NatTypeRep , unET' (unT 2)

c : ET
c = BoolTypeRep , unET' (unT true)

ab = bar a b -- just true                                                                                                  

ac = bar a c -- nothing            

ET.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
import Data.Singletons
import Data.Singletons.TypeRepStar ()
import Data.Type.Equality
import Data.Typeable
                                                                                                                           
data T a = T { unT :: a }

data ET = forall a . Typeable a => ET { unET :: T a }

withET :: ET -> (forall a . Typeable a => T a -> r) -> r
withET (ET t) f = f t

foo :: T a -> T a -> Bool
foo _ _ = True

bar :: ET -> ET -> Bool
bar eta etb = withET eta $ \a -> withET etb $ \b -> case testEquality (singByProxy a) (singByProxy b) of
  Just Refl -> foo a b
  Nothing   -> error "different type"