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