Changes between Initial Version and Version 1 of Ticket #1496


Ignore:
Timestamp:
Jul 4, 2007 11:56:45 PM (8 years ago)
Author:
sorear
Comment:

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  
     1Given: 
     2 
    13{{{ 
    24{-# OPTIONS_GHC -ftype-families #-} 
     
    46data family Z :: * -> * 
    57 
    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) 
     8newtype Moo = Moo Int 
    119 
    1210newtype instance Z Int = ZI Double 
    1311newtype instance Z Moo = ZM (Int,Int) 
    14  
    15 main = case isInt (ZI 4.0) of ZM tu -> print tu 
    1612}}} 
    1713 
    18 {{{ 
    19 stefan@stefans:/tmp$ ghc -dcore-lint 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 newtype-deriving 
    28 hack, but as the resulting core passes Core Lint this is othogonal to that bug. 
    29 The family of axioms produced is inconsistant: 
     14We generate the axioms: 
    3015 
    3116{{{ 
     
    3621(from the newtype) 
    3722Moo ~ Int 
     23}}} 
    3824 
     25And can prove: 
     26 
     27{{{ 
    3928(production REFL in the FC(X) paper) 
    4029Z ~ Z 
     
    5241Double ~ (Int,Int) 
    5342}}} 
     43 
     44Tickling this seems to require the newtype cheat, but the inconsistant axioms 
     45allow code to pass Core Lint and still crash: 
     46 
     47{{{ 
     48newtype Moo = Moo Int deriving(IsInt) 
     49class IsInt t where 
     50    isInt :: c Int -> c t 
     51instance IsInt Int where isInt = id 
     52main = case isInt (ZI 4.0) of ZM tu -> print tu 
     53}}} 
     54 
     55{{{ 
     56stefan@stefans:/tmp$ ghc -dcore-lint Z.hs 
     57stefan@stefans:/tmp$ ./a.out 
     58Segmentation fault 
     59stefan@stefans:/tmp$ ghc -V 
     60The Glorious Glasgow Haskell Compilation System, version 6.7.20070612 
     61stefan@stefans:/tmp$ 
     62}}}