[GHC] #1995: Unsoundness in the RTTI scheme when newtypes are involved

[GHC]

#1995: Unsoundness in the RTTI scheme when newtypes are involved
----------------------+-----------------------------------------------------
 Reporter:  mnislaih  |          Owner:  mnislaih          
     Type:  bug       |         Status:  new               
 Priority:  normal    |      Milestone:  6.10 branch       
Component:  GHCi      |        Version:  6.8.2             
 Severity:  major     |     Resolution:                    
 Keywords:            |     Difficulty:  Project (> 1 week)
 Testcase:            |   Architecture:  Unknown           
       Os:  Unknown   |  
----------------------+-----------------------------------------------------
Comment (by 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.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1995#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler