Opened 7 years ago

Last modified 9 months ago

#1496 closed bug

Newtypes and type families combine to produce inconsistent FC(X) axiom sets — at Version 1

Reported by: sorear Owned by:
Priority: normal Milestone: 7.6.2
Component: Compiler (Type checker) Version: 6.7
Keywords: Cc: samb, chak@…, ganesh.sittampalam@…, lennart.augustsson@…, tom.schrijvers@…, df@…, mjm2002@…, pumpkingod@…, ben@…, jmaessen@…, hackage.haskell.org@…, ezyang@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description (last modified by sorear)

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$

Change History (1)

comment:1 Changed 7 years ago by sorear

  • Component changed from Compiler to Compiler (Type checker)
  • Description modified (diff)
  • Summary changed from System FC{Newtypes,TypeFamilies} is unsound to Newtypes and type families combine to produce inconsistent FC(X) axiom sets
Note: See TracTickets for help on using tickets.