As others have pointed out, the example is a less defensible choice since the type has already been specialized. Polymorphic types (quantified theorems) begin to greatly restrict the number of programs (proofs) down to the point where you sometimes get "free theorems" such as those discovered by Djinn. For instance
foo :: forall a b. a -> b -> a
is inhabited by precisely one program
foo a b = a
Furthermore, you have the opposite effect such as the nonexistence of functions with types like
freeCoerce :: forall a b. a -> b
The best you can do is write
safeCoerce :: forall a b. a -> Maybe b
which sometimes works but is allowed to fail if the coercion isn't possible.
---
Taking this to a logical extreme you can extend a Hindley-Milner type system to include dependent types and then construct meaningful types (theorems) which are only inhabited by correct and obvious programs. For instance, this Agda type
sort : List a -> Sorted a
maps lists not just to other lists but instead the type of sorted lists guaranteeing the meaning of the function 'sort'.
---
Obviously any static typing system inherits a bit of this power. There's no doubt that reading the signature of a C++ function will help you to make educated guesses at what's going on. Furthermore, a malicious Haskell library implementor could use the "unsafe" family of functions to create something like 'coerce' or a function that has impure side-effects but doesn't end up in the IO monad. There is some amount of trust that libraries do not abuse such unsafe commands and the IO monad can be guaranteed to isolate impure effects---but so long as that isn't violated, the types can be incredibly informative.
---
It's also worth noting that Haskell does have "bottom" inhabiting every type, similar to null but denoting infinite loops instead of null values. So you actually can write coerce without using 'unsafe' commands like
---
Taking this to a logical extreme you can extend a Hindley-Milner type system to include dependent types and then construct meaningful types (theorems) which are only inhabited by correct and obvious programs. For instance, this Agda type
maps lists not just to other lists but instead the type of sorted lists guaranteeing the meaning of the function 'sort'.---
Obviously any static typing system inherits a bit of this power. There's no doubt that reading the signature of a C++ function will help you to make educated guesses at what's going on. Furthermore, a malicious Haskell library implementor could use the "unsafe" family of functions to create something like 'coerce' or a function that has impure side-effects but doesn't end up in the IO monad. There is some amount of trust that libraries do not abuse such unsafe commands and the IO monad can be guaranteed to isolate impure effects---but so long as that isn't violated, the types can be incredibly informative.
---
It's also worth noting that Haskell does have "bottom" inhabiting every type, similar to null but denoting infinite loops instead of null values. So you actually can write coerce without using 'unsafe' commands like