[GHC] #1496: System FC{Newtypes,TypeFamilies} is unsound

[GHC]

#1496: System FC{Newtypes,TypeFamilies} is unsound
-----------------------+----------------------------------------------------
  Reporter:  sorear    |          Owner:         
      Type:  bug       |         Status:  new    
  Priority:  normal    |      Milestone:         
 Component:  Compiler  |        Version:  6.7    
  Severity:  normal    |       Keywords:         
Difficulty:  Unknown   |             Os:  Unknown
  Testcase:            |   Architecture:  Unknown
-----------------------+----------------------------------------------------
{{{
 {-# 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
 }}}

 {{{
 stefan at stefans:/tmp$ ghc -dcore-lint Z.hs
 stefan at stefans:/tmp$ ./a.out
 Segmentation fault
 stefan at stefans:/tmp$ ghc -V
 The Glorious Glasgow Haskell Compilation System, version 6.7.20070612
 stefan at stefans:/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)
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1496>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
-------------- next part --------------
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs at haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs