#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_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
