What is the use case of eqT rather than cast?

Question

In Data.Typeable there is a function cast

cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b 

and a function eqT

eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b) 

They seem to be nearly identical in effect and implementation, I was wondering if there is any practical import to the description of eqT: extract a witness of equality of two types.

Answer 1

This is awkward:

checkEq :: forall a b. (Typeable a, Typeable b, Eq b) => a -> a -> Maybe Bool
checkEq a a' = do
    b  <- cast @_ @b a
    b' <- cast a'
    pure (b == b')

Internally, that checks the cast twice, and does two Maybe pattern matches. But once we've done one cast, we know the other will succeed!

This is better:

checkEq a a' = (\Refl -> a == a') <$> eqT @a @b

Just one check, just one Maybe pattern match.

This kind of thing often comes up when you have existentially-quantified Typeable things in data structures, and want to do operations on them that take multiple arguments. Bringing a type equality into scope once (with a Refl pattern) and then being able to use that equality multiple times is both more convenient and more efficient than repeatedly casting.

Edit

chi points out that it is actually possible to do just one cast in this case:

checkEq a a' = (\eq -> eq a a') <$> cast ((==) @b)
checkEq a a' = uncurry ((==) @b) <$> cast (a, a')

In the general case, you can build a tuple of all the operations you need to cast, or all the values you need to cast. I guess this doesn't really leave me with a strong technical argument for either one over the other!