#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: normal | Resolution:
Keywords: | Difficulty: Unknown
Os: Unknown | Testcase:
Architecture: Unknown |
----------------------------------------+-----------------------------------
Changes (by sorear):
* component: Compiler => Compiler (Type checker)
* summary: System FC{Newtypes,TypeFamilies} is unsound => Newtypes and
type families combine to produce inconsistent
FC(X) axiom sets
Old description:
> {{{
> {-# OPTIONS_GHC -ftype-families #-}
> {-# LANGUAGE GeneralizedNewtypeDeriving #-}
> data family Z :: * -> *
>
> class IsInt t where
> isInt :: c Int -> c t
> instance IsInt Int where isInt = id
>
> newtype Moo = Moo Int deriving(IsInt)
>
> newtype instance Z Int = ZI Double
> newtype instance Z Moo = ZM (Int,Int)
>
> main = case isInt (ZI 4.0) of ZM tu -> print tu
> }}}
>
> {{{
> [EMAIL PROTECTED]:/tmp$ ghc -dcore-lint Z.hs
> [EMAIL PROTECTED]:/tmp$ ./a.out
> Segmentation fault
> [EMAIL PROTECTED]:/tmp$ ghc -V
> The Glorious Glasgow Haskell Compilation System, version 6.7.20070612
> [EMAIL PROTECTED]:/tmp$
> }}}
>
> It does not appear possible to tickle this without using the newtype-
> deriving
> hack, but as the resulting core passes Core Lint this is othogonal to
> that bug.
> The family of axioms produced is inconsistant:
>
> {{{
> (from the instances)
> Z Int ~ Double
> Z Moo ~ (Int,Int)
>
> (from the newtype)
> Moo ~ Int
>
> (production REFL in the FC(X) paper)
> Z ~ Z
>
> (production COMP)
> Z Moo ~ Z Int
>
> (production TRANS)
> Z Moo ~ Double
>
> (production SYM)
> Double ~ Z Moo
>
> (production TRANS)
> Double ~ (Int,Int)
> }}}
New description:
Given:
{{{
{-# OPTIONS_GHC -ftype-families #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
data family Z :: * -> *
newtype Moo = Moo Int
newtype instance Z Int = ZI Double
newtype instance Z Moo = ZM (Int,Int)
}}}
We generate the axioms:
{{{
(from the instances)
Z Int ~ Double
Z Moo ~ (Int,Int)
(from the newtype)
Moo ~ Int
}}}
And can prove:
{{{
(production REFL in the FC(X) paper)
Z ~ Z
(production COMP)
Z Moo ~ Z Int
(production TRANS)
Z Moo ~ Double
(production SYM)
Double ~ Z Moo
(production TRANS)
Double ~ (Int,Int)
}}}
Tickling this seems to require the newtype cheat, but the inconsistant
axioms
allow code to pass Core Lint and still crash:
{{{
newtype Moo = Moo Int deriving(IsInt)
class IsInt t where
isInt :: c Int -> c t
instance IsInt Int where isInt = id
main = case isInt (ZI 4.0) of ZM tu -> print tu
}}}
{{{
[EMAIL PROTECTED]:/tmp$ ghc -dcore-lint Z.hs
[EMAIL PROTECTED]:/tmp$ ./a.out
Segmentation fault
[EMAIL PROTECTED]:/tmp$ ghc -V
The Glorious Glasgow Haskell Compilation System, version 6.7.20070612
[EMAIL PROTECTED]:/tmp$
}}}
--
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
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
