Changes between Initial Version and Version 1 of Ticket #1496
 Timestamp:
 Jul 4, 2007 11:56:45 PM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

Ticket #1496
 Property Component changed from Compiler to Compiler (Type checker)
 Property Summary changed from System FC{Newtypes,TypeFamilies} is unsound to Newtypes and type families combine to produce inconsistent FC(X) axiom sets

Ticket #1496 – Description
initial v1 1 Given: 2 1 3 {{{ 2 4 {# OPTIONS_GHC ftypefamilies #} … … 4 6 data family Z :: * > * 5 7 6 class IsInt t where 7 isInt :: c Int > c t 8 instance IsInt Int where isInt = id 9 10 newtype Moo = Moo Int deriving(IsInt) 8 newtype Moo = Moo Int 11 9 12 10 newtype instance Z Int = ZI Double 13 11 newtype instance Z Moo = ZM (Int,Int) 14 15 main = case isInt (ZI 4.0) of ZM tu > print tu16 12 }}} 17 13 18 {{{ 19 stefan@stefans:/tmp$ ghc dcorelint Z.hs 20 stefan@stefans:/tmp$ ./a.out 21 Segmentation fault 22 stefan@stefans:/tmp$ ghc V 23 The Glorious Glasgow Haskell Compilation System, version 6.7.20070612 24 stefan@stefans:/tmp$ 25 }}} 26 27 It does not appear possible to tickle this without using the newtypederiving 28 hack, but as the resulting core passes Core Lint this is othogonal to that bug. 29 The family of axioms produced is inconsistant: 14 We generate the axioms: 30 15 31 16 {{{ … … 36 21 (from the newtype) 37 22 Moo ~ Int 23 }}} 38 24 25 And can prove: 26 27 {{{ 39 28 (production REFL in the FC(X) paper) 40 29 Z ~ Z … … 52 41 Double ~ (Int,Int) 53 42 }}} 43 44 Tickling this seems to require the newtype cheat, but the inconsistant axioms 45 allow code to pass Core Lint and still crash: 46 47 {{{ 48 newtype Moo = Moo Int deriving(IsInt) 49 class IsInt t where 50 isInt :: c Int > c t 51 instance IsInt Int where isInt = id 52 main = case isInt (ZI 4.0) of ZM tu > print tu 53 }}} 54 55 {{{ 56 stefan@stefans:/tmp$ ghc dcorelint Z.hs 57 stefan@stefans:/tmp$ ./a.out 58 Segmentation fault 59 stefan@stefans:/tmp$ ghc V 60 The Glorious Glasgow Haskell Compilation System, version 6.7.20070612 61 stefan@stefans:/tmp$ 62 }}}