[Haskell] Correct interpretation of the curry-howard isomorphism

[Bruno Oliveira]

Hi all!

I would like to know what is the right interpretation of one of the consequences of the curry-howard isomorphism.

I know that there is a relation between being able to implement coerse :: a -> b, and the fact that a type system is sound.

I thought this would be the right consequence:

------------------------------------------
if we can write a function:

coerce :: a -> b 

then, this would mean (by the curry-howard isomorphism) that the type system is not sound.
------------------------------------------

but then, it would be too easy to write this in haskell:

coerce :: a -> b
coerce x = undefined

As an obvious consequence, Haskell type system would be unsound.

So, I assumed that this would be a wrong interpretation. Would the following be more correct?

------------------------------------------
if we can write a function:

coerce :: a -> b

without calling any other function or primitive (that is, just with making use of the type system), then this would 
mean that the type system is unsound.
------------------------------------------

I would appreciate if someone could provide me with the right interpretation.

Thanks, in advance!

Best Regards,

Bruno Oliveira