[GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets

[GHC]

#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
----------------------------------------+-----------------------------------
    Reporter:  sorear                   |        Owner:         
        Type:  bug                      |       Status:  new    
    Priority:  normal                   |    Milestone:         
   Component:  Compiler (Type checker)  |      Version:  6.7    
    Severity:  critical                 |   Resolution:         
    Keywords:                           |   Difficulty:  Unknown
          Os:  Unknown                  |     Testcase:         
Architecture:  Unknown                  |  
----------------------------------------+-----------------------------------
Changes (by chak):

  * cc:  samb => samb,chak

Comment:

 There are really two issues here mixed up.  One one hand we have an
 infelicity in combining the FC equalities introduced by newtypes and type
 families.  That's a bad thing from a theoretical point of view, but I
 don't know of an exploit to break type safety with that.  In fact, I think
 it is merely a problem of the type-preserving translation to FC in GHC and
 not with the source type system (ie, all accepted programs are fine, even
 if they lead to fishy FC).

 On the other hand, the example code demonstrates that newtype deriving in
 its current generality is unsound and leads GHC to accept source programs
 that it should not accept.  Here is an alternative example that exploits
 the same problem using GADTs instead of type families (its not quite as
 dramatic as it doesn't segv, but it refutes an irrefutable pattern it
 really shouldn't):
 {{{
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}

 class IsInt t where
     isInt :: c Int -> c t
 instance IsInt Int where isInt = id

 newtype Moo = Moo Int deriving(IsInt,Show)

 data Z a where
   ZI :: Double -> Z Int
   ZM :: (Int, Int) -> Z Moo

 foo :: Z Moo -> Moo
 foo ~(ZM (i, _)) = Moo i

 main = print $ foo (isInt (ZI 4.0))
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1496>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
-------------- next part --------------
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs at haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs