As far as I underspend all checks of Data.Typeable.cast can be done by compiler in compile-time. While it impose partially what one may consider syntax sugar I believe that there is no restriction that would not allowed compiler to behave like that: cast :: forall a b. a -> Maybe b -- Pseudo-haskell cast x = staticIf a == b then Just x else Nothing [1] Also I may not grasp every element of Haskell but what is the reason of not implementing Typeable by default? Regards [1] You may say that I need unsafeCoerce but 1. I'd prefere to write let x = fromMaybe (error "Wrong types") $ cast x' :: a instead of let x = unsafeCoerce x' :: a in case when I (not compiler) know that x and x' have the same type (a) as it makes the crash big and in Haskell instead of possible some problems with GC or something which I'll find in totally unrelated piece of program. 2. I may want different actions