GHC: Ticket #5498: Generalized newtype deriving allows creating of instances I can't create by hand
http://ghc.haskell.org/trac/ghc/ticket/5498
<p>
First here is a simple module that establishes a list where once created (with a min element) subsequent elements inserted should always be larger than the min:
</p>
<pre class="wiki">-- | Here we expose a MinList API that only allows elements
-- to be inserted into a list if they are at least greater
-- than an initial element the list is created with.
module MinList (
MinList,
newMinList,
insertMinList,
printIntMinList
) where
data MinList a = MinList a [a]
newMinList :: Ord a => a -> MinList a
newMinList n = MinList n []
insertMinList :: Ord a => MinList a -> a -> MinList a
insertMinList s@(MinList m xs) n | n > m = MinList m (n:xs)
| otherwise = s
printIntMinList :: MinList Int -> IO ()
printIntMinList (MinList min xs) = putStrLn $ "MinList Int :: MinList " ++ show min ++ " " ++ show xs
</pre><p>
Now I import this module and use generalized newtype deriving to create a function I couldn't create by hand:
</p>
<pre class="wiki">{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-- | We use newtype to create an isomorphic type to Int
-- with a reversed Ord dictionary. We now use the MinList
-- API of MinList to create a new MinList. Then we use newtype
-- deriving to convert the newtype MinList to an Int
-- MinList. This final result breaks the invariants of
-- MinList which shouldn't be possible with the exposed
-- API of MinList.
module Main where
import MinList
class IntIso t where
intIso :: c t -> c Int
instance IntIso Int where
intIso = id
newtype Down a = Down a deriving (Eq, IntIso)
instance Ord a => Ord (Down a) where
compare (Down a) (Down b) = compare b a
fine :: MinList (Down Int)
fine = foldl (\x y -> insertMinList x $ Down y) (newMinList $ Down 0) [-1,-2,-3,-4,1,2,3,4]
bad :: MinList Int
bad = intIso fine
main = do
printIntMinList bad
</pre><p>
The problem here is the isoInt method where I can do:
</p>
<pre class="wiki">isoInt :: MinList (Down Int) -> MinList Int
</pre><p>
which I shouldn't be able to do since I don't have the constructors for <code>MinList</code>.
</p>
<p>
This is the reason I've currently disabled newtype deriving in Safe Haskell but potentially we can enable it if this bug is fixed.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/5498
Trac 1.2.2.dev0simonpjSat, 24 Sep 2011 01:55:36 GMTdescription changed; cc set
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:1
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:1
<ul>
<li><strong>cc</strong>
<em>dimitris@…</em> <em>sweirich@…</em> added
</li>
<li><strong>description</strong>
modified (<a href="/trac/ghc/ticket/5498?action=diff&version=1">diff</a>)
</li>
</ul>
<p>
I believe that this bug is very closely related to <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1496" title="#1496: bug: Newtypes and type families combine to produce inconsistent FC(X) axiom sets (closed: fixed)">#1496</a> (just look at the type of the class moethod in each case).
</p>
<p>
We have an as-yet-unimplemented solution to <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1496" title="#1496: bug: Newtypes and type families combine to produce inconsistent FC(X) axiom sets (closed: fixed)">#1496</a>, namely our POPL'11 paper <a class="ext-link" href="http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/"><span class="icon"></span>Generative type abstraction and type level computation</a>. I don't yet know if the same approach deals with the problem you identify in this ticket, but my nose tells me yes. I'm adding Stephanie and Dimitrios to the cc.
</p>
TicketsimonmarFri, 07 Oct 2011 14:21:04 GMT
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:2
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:2
<p>
The fix is to reject the <code>deriving</code> clause with an error, right? Couldn't we fix that without any deep type checker changes, just with a syntactic restriction on what classes you can derive for a newtype?
</p>
TicketdtereiThu, 20 Oct 2011 07:13:25 GMT
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:3
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:3
<p>
How much work would it be to implement the fix from the paper? I'm guessing its in a complex part of the compiler I have no knowledge of so am probably not really the right person for the job.
</p>
<p>
What about what Simon M proposes? I'm not sure if this would be enough though as you can also combine newtype deriving with GADTs or TypeFamilies to cause segfaults which is something <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/SafeHaskell">SafeHaskell</a> tries to prevent.
</p>
TicketsimonpjFri, 21 Oct 2011 14:51:37 GMT
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:4
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:4
<p>
I really don't know of a "simple syntactic restriction" that would do the job. And the "roles" paper requires thought about how to implement it. Definitely it must wait until the current stuff for kind inference is done.
</p>
<p>
Is this really ruining anyone's day?
</p>
<p>
Simon
</p>
TicketsimonpjFri, 21 Oct 2011 14:54:24 GMTblockedby set
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:5
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:5
<ul>
<li><strong>blockedby</strong>
set to <em>1496</em>
</li>
</ul>
TicketiglooThu, 10 Nov 2011 01:22:17 GMTmilestone set
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:6
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:6
<ul>
<li><strong>milestone</strong>
set to <em>7.6.1</em>
</li>
</ul>
TicketiglooWed, 12 Sep 2012 11:12:04 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:7
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:7
<ul>
<li><strong>milestone</strong>
changed from <em>7.6.1</em> to <em>7.6.2</em>
</li>
</ul>
TicketgoldfireTue, 23 Jul 2013 11:26:10 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:8
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:8
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
See <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/Roles">Roles</a> for the concrete approach toward a solution to the seg-faulting problem. Roles won't fix the abstraction problem that is the main subject of this ticket, though.
</p>
TicketnomeataTue, 07 Jan 2014 11:40:30 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:9
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:9
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
This should not be possible any more: In the type <code>intIso :: forall c. c t -> c Int</code>, <code>c</code>’s type parameter is considered to be nominal, so <code>coerce</code> will not allow changing <code>c (Down a)</code> to <code>c a</code> any more. And GND is now based on <code>Coercible</code>...
</p>
TicketsimonpjTue, 07 Jan 2014 12:22:40 GMTtestcase set
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:10
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:10
<ul>
<li><strong>testcase</strong>
set to <em>deriving/should_fail/T5498</em>
</li>
</ul>
<p>
Indeed. The program is indeed rejected, although the error message is not fantastic. I've added it as a test.
</p>
<p>
I think you can enable GND in Safe Haskell.
</p>
<p>
Simon
</p>
TicketSimon Peyton Jones <simonpj@…>Fri, 10 Jan 2014 08:53:00 GMT
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:11
http://ghc.haskell.org/trac/ghc/ticket/5498#comment:11
<p>
In <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/1285af76c32c84332835d5d430146403bf610796/testsuite" title="Test Trac #5498">1285af76c32c84332835d5d430146403bf610796/testsuite</a>:
</p>
<pre class="message">Test Trac #5498</pre>
Ticket