Runtime comparison of types for lifting polymorphic data structures into GADTs

Suppose we define a GADT for comparison of types:

data EQT a b where
  Witness :: EQT a a

Is it then possible to declare a function eqt with the following type signature:

eqt :: (Typeable a, Typeable b) => a -> b -> Maybe (EQT a b)

...such that eqt x y evaluates to Just Witness if typeOf x == typeOf y --- and otherwise to Nothing?

The function eqt would make it possible to lift ordinary polymorphic data structures into GADTs.