[lmm]

Usually we have a more powerful type system that means we don't need to. E.g. in something like Go you might have a Reader, whereas in a functional language you might have [A: Reader], i.e. a generic type A for which a Reader typeclass instance exists. This means you don't have to throw away the specific type (ReaderCloseable) to be able to use it as a Reader.

If you really need to cast, most functional languages will still let you - but as you say, it invalidates the proofs so is very much discouraged (e.g. the scalazzi safe subset requires you to not cast).