Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 7.6.1 Component: Compiler (Type checker) | Version: 6.7 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby: |Blocking: 5498 Related: | +--- Comment(by simonpj): See also #7148 -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:38 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 7.6.1 Component: Compiler (Type checker) | Version: 6.7 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby: |Blocking: 5498 Related: | +--- Changes (by ezyang): * cc: ezyang@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:37 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: simonpj Type: bug | Status: new Priority: low |Milestone: 7.4.1 Component: Compiler (Type checker) | Version: 6.7 Keywords: | Testcase: Blockedby: | Difficulty: Unknown Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown +--- Comment(by simonpj): See also #5498 -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:34 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: simonpj Type: bug | Status: new Priority: low |Milestone: 7.2.1 Component: Compiler (Type checker) | Version: 6.7 Keywords: | Testcase: Blockedby: | Difficulty: Unknown Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown +--- Changes (by liyang): * cc: hackage.haskell.org@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: simonpj Type: bug | Status: new Priority: low |Milestone: 7.0.1 Component: Compiler (Type checker) | Version: 6.7 Keywords: | Testcase: Blockedby: | Difficulty: Unknown Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown +--- Comment(by simonpj): See also #4846 -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom
sets
+---
Reporter: sorear |Owner: simonpj
Type: bug | Status: new
Priority: normal |Milestone: 6.12 branch
Component: Compiler (Type checker) | Version: 6.7
Keywords: | Difficulty: Unknown
Os: Unknown/Multiple | Testcase:
Architecture: Unknown/Multiple | Failure: None/Unknown
+---
Changes (by jmaessen):
* cc: jmaes...@… (added)
* failure: = None/Unknown
Comment:
Here's a simple example program that violates the invariant of `Set` while
using ''only'' newtype deriving (and not more complex extensions such as
multiparameter type classes or type functions):
{{{
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Main(main) where
import Data.Set
class IsoInt a where
convFromInt :: item Int - item a
instance IsoInt Int where
convFromInt = id
newtype Down a = Down a deriving (Eq, Show, IsoInt)
instance Ord a = Ord (Down a) where
compare (Down a) (Down b) = compare b a
asSetDown :: Set (Down Int) - Set (Down Int)
asSetDown = id
a1 = toAscList . asSetDown . convFromInt . fromAscList $ [0..10]
a2 = toAscList . asSetDown . fromAscList . reverse . convFromInt $ [0..10]
main = do
print a1
print a2
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:26
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: simonpj Type: bug | Status: new Priority: normal |Milestone: 6.12 branch Component: Compiler (Type checker) | Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Testcase: | Os: Unknown/Multiple Architecture: Unknown/Multiple | +--- Changes (by BenMoseley): * cc: b...@moseley.name (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: simonpj Type: bug | Status: new Priority: normal |Milestone: 6.12 branch Component: Compiler (Type checker) | Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Testcase: | Os: Unknown/Multiple Architecture: Unknown/Multiple | +--- Comment (by SamB): Well, we had a conversation about this on IRC today, and Cale has convinced me that there is a bug in the definition of ~ in your papers. Cale The main reason that newtypes exist is 1) to ensure that things are not confused with the original type, and 2) to allow separate instances to be written without overhead.[[BR]] Cale For ~ to resolve them as the same type goes against both.[[BR]] Cale Basically, the way that ~ is treating newtype right now is how it ought to be treating 'type' -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: simonpj Type: bug | Status: new Priority: normal |Milestone: 6.12 branch Component: Compiler (Type checker) | Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Testcase: | Os: Unknown/Multiple Architecture: Unknown/Multiple | +--- Comment (by SamB): Okay, it seems to me that in order to solve this problem, GHC needs to be able to prove, somehow or other, that each method to be derived can be safely converted from the one type to the other. Correct? And the main choice here is whether it should A. try to do this on it's own, and prove that it can just cast between the one and the other or B. require the user to explicitly provide Functor, BiFunctor, etc. instances for GHC to use during this process, yes? Probably it is best to take an approach that we can be sure is safe without too many aspirins, and use approach B, but have GHC issue a warning whenever it is unable to optimize away the coercions for some of the methods, and therefore unable to re-use the dictionary. The rules for the derivation itself should preferably be written up in a paper so that the other compilers, too, can benefit from this extremely convenient feature, though doubtless it will become somewhat less convenient in some ways if this bug is fixed. For this approach to work well with multi-parameter types, however, we'd presumably need to add a lot more Functor-related classes to base, would we not? But which ones? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: simonpj Type: bug | Status: new Priority: normal |Milestone: 6.12 branch Component: Compiler (Type checker) | Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Testcase: | Os: Unknown/Multiple Architecture: Unknown/Multiple | +--- Changes (by igloo): * milestone: 6.10 branch = 6.12 branch -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: simonpj Type: bug | Status: new Priority: normal |Milestone: 6.10 branch Component: Compiler (Type checker) | Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Testcase: | Os: Unknown/Multiple Architecture: Unknown/Multiple | +--- Comment (by simonpj): See #2721 for another example. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets -+-- Reporter: sorear | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 6.10 branch Component: Compiler (Type checker) |Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Testcase: | Architecture: Unknown/Multiple Os: Unknown/Multiple | -+-- Changes (by morrow): * cc: [EMAIL PROTECTED] (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets -+-- Reporter: sorear | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 6.10 branch Component: Compiler (Type checker) |Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Testcase: | Architecture: Unknown Os: Unknown | -+-- Changes (by dfranke): * cc: [EMAIL PROTECTED] (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets -+-- Reporter: sorear | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 6.10 branch Component: Compiler (Type checker) |Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Testcase: | Architecture: Unknown Os: Unknown | -+-- Changes (by simonmar): * priority: high = normal * milestone: 6.8 branch = 6.10 branch -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom
sets
+---
Reporter: sorear |Owner: simonpj
Type: bug | Status: new
Priority: high |Milestone: 6.8 branch
Component: Compiler (Type checker) | Version: 6.7
Severity: critical | Resolution:
Keywords: | Difficulty: Unknown
Os: Unknown | Testcase:
Architecture: Unknown |
+---
Comment (by Isaac Dupree):
Replying to [comment:12 toms]:
However, GADTs are definitely not functors.
...
We can attempt to fix the situation by imposing conditions on the
types involved in
a newtype deriving:
* generate the fmap code, and hence demand explicit Functor
instances.
We should be able to expect the compiler to eliminate any runtime
overhead.
From Frisby we have a data type that is a Functor and a GADT, but not a
Functor in the way you and GHC expect:
{{{
data PE a where
-- leaving out most of the constructors, but note especially PMap
Char :: IntSet.IntSet - PE Char
Failure :: PE a
Not :: PE a - PE ()
Then :: PE a - PE b - PE (a,b)
PMap :: (a - b) - PE a - PE b
instance Functor PE where
fmap = PMap
}}}
Applying the `fmap`-option would make interesting, type-correct code be
generated that could not be optimized away (so the dictionaries couldn't
be shared).
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496#comment:14
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom
sets
+---
Reporter: sorear |Owner:
Type: bug | Status: new
Priority: normal |Milestone:
Component: Compiler (Type checker) | Version: 6.7
Severity: critical | Resolution:
Keywords: | Difficulty: Unknown
Os: Unknown | Testcase:
Architecture: Unknown |
+---
Changes (by chak):
* cc: samb = samb,chak
Comment:
There are really two issues here mixed up. One one hand we have an
infelicity in combining the FC equalities introduced by newtypes and type
families. That's a bad thing from a theoretical point of view, but I
don't know of an exploit to break type safety with that. In fact, I think
it is merely a problem of the type-preserving translation to FC in GHC and
not with the source type system (ie, all accepted programs are fine, even
if they lead to fishy FC).
On the other hand, the example code demonstrates that newtype deriving in
its current generality is unsound and leads GHC to accept source programs
that it should not accept. Here is an alternative example that exploits
the same problem using GADTs instead of type families (its not quite as
dramatic as it doesn't segv, but it refutes an irrefutable pattern it
really shouldn't):
{{{
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
class IsInt t where
isInt :: c Int - c t
instance IsInt Int where isInt = id
newtype Moo = Moo Int deriving(IsInt,Show)
data Z a where
ZI :: Double - Z Int
ZM :: (Int, Int) - Z Moo
foo :: Z Moo - Moo
foo ~(ZM (i, _)) = Moo i
main = print $ foo (isInt (ZI 4.0))
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: Type: bug | Status: new Priority: normal |Milestone: Component: Compiler (Type checker) | Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Os: Unknown | Testcase: Architecture: Unknown | +--- Changes (by SamB): * severity: normal = critical Comment: An unsound typesystem is a very bad thing. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets +--- Reporter: sorear |Owner: Type: bug | Status: new Priority: normal |Milestone: Component: Compiler (Type checker) | Version: 6.7 Severity: critical | Resolution: Keywords: | Difficulty: Unknown Os: Unknown | Testcase: Architecture: Unknown | +--- Changes (by SamB): * cc: = samb -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1496: Newtypes and type families combine to produce inconsistent FC(X) axiom sets
#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom
sets
+---
Reporter: sorear |Owner:
Type: bug | Status: new
Priority: normal |Milestone:
Component: Compiler (Type checker) | Version: 6.7
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Os: Unknown | Testcase:
Architecture: Unknown |
+---
Changes (by sorear):
* component: Compiler = Compiler (Type checker)
* summary: System FC{Newtypes,TypeFamilies} is unsound = Newtypes and
type families combine to produce inconsistent
FC(X) axiom sets
Old description:
{{{
{-# 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
}}}
{{{
[EMAIL PROTECTED]:/tmp$ ghc -dcore-lint Z.hs
[EMAIL PROTECTED]:/tmp$ ./a.out
Segmentation fault
[EMAIL PROTECTED]:/tmp$ ghc -V
The Glorious Glasgow Haskell Compilation System, version 6.7.20070612
[EMAIL PROTECTED]:/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)
}}}
New description:
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
}}}
{{{
[EMAIL PROTECTED]:/tmp$ ghc -dcore-lint Z.hs
[EMAIL PROTECTED]:/tmp$ ./a.out
Segmentation fault
[EMAIL PROTECTED]:/tmp$ ghc -V
The Glorious Glasgow Haskell Compilation System, version 6.7.20070612
[EMAIL PROTECTED]:/tmp$
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1496
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
