Unsoundness in the RTTI scheme when newtypes are involved

[mnislaih]

To be filled with further details soon

[mnislaih]

This means that the debugger can assign incorrect types to the variables in a breakpoint.

An example. If we have a polymorphic function with a type variable of kind (* -> *) in its signature in some argument, and in a function call that parameter happens to be instantiated with a newtype of a certain shape, RTTI can panic or even worse, recover a false type. Concretely,

newtype MkT2 a = MkT2 [Maybe a]
...
fmapInt :: Functor f => (Int->b) -> f Int -> f b
fmapInt f x = fmap f x

MkT2 a is isomorphic to [Maybe a], but MkT2 itself has no correspondent isomorphic type! The RTTI mechanism makes an assumption that every newtype is isomorphic to some type, but that is true in all cases only if the type constructor is fully applied. If not, it doesn't need to be true.

This is what RTTI will currently do. Suppose a function If fmapInt is called with a MkT2 value, the RTTI scheme, in absence of the newtype evidence, will either

1) see the (:) constructor, conclude that t = [] and since now the type of x is monomorphic, and stop there if there is no need to reconstruct the term too. It has computed a false type.

2) if there is the need to reconstruct the term, see the (:) constructor and the Just constructor below it, and conjecture that the type of x is [Maybe Int]. So far so good, but then when it tries to satisfy the constraint that x::t Int it panics with "Can't unify".

3) even if the term is reconstructed as in 2), it is possible to compute a wrong type if the closure with the Just constructor is unevaluated.

[mnislaih]

(replace t with f in the types in items 1)-3) above)

[mnislaih]

Fixed up to some point by the patch below.

Thu Sep 18 05:21:33 PDT 2008  pepe
 * Fix a couple of issues with :print

It is still possible to make :print compute unsound types, e.g. with recursive newtypes like:

newtype In f = In (f (In f))

I don't think this can be fixed completely without resorting to a separate compilation mode for :print, where newtypes are replaced by strict one-constructor datatypes.

[igloo]

This was merged into the 6.10 branch too.