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}}}