id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
1496,Newtypes and type families combine to produce inconsistent FC(X) axiom sets,sorear,simonpj,"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
}}}

{{{
stefan@stefans:/tmp$ ghc -dcore-lint Z.hs
stefan@stefans:/tmp$ ./a.out
Segmentation fault
stefan@stefans:/tmp$ ghc -V
The Glorious Glasgow Haskell Compilation System, version 6.7.20070612
stefan@stefans:/tmp$
}}}",bug,new,normal,7.6.2,Compiler (Type checker),6.7,,,samb chak@… ganesh.sittampalam@… lennart.augustsson@… tom.schrijvers@… df@… mjm2002@… pumpkingod@… ben@… jmaessen@… hackage.haskell.org@… ezyang@…,Unknown/Multiple,Unknown/Multiple,None/Unknown,Unknown,,,5498,