GHC: Ticket #345: GADT - fundep interaction
http://ghc.haskell.org/trac/ghc/ticket/345
<pre class="wiki">GADTs and fundeps don't seem to interact in the way
that I (perhaps naively) expect. I expected that for
each case, the type variables would be instantiated
according to the type of the constructors, and then the
fundep would be used to figure out the result type.
{-# OPTIONS_GHC -fglasgow-exts #-}
data Succ n
data Zero
class Plus x y z | x y -> z
instance Plus Zero x x
instance Plus x y z => Plus (Succ x) y (Succ z)
infixr 5 :::
data List :: * -> * -> * where
Nil :: List a Zero
(:::) :: a -> List a n -> List a (Succ n)
append :: Plus x y z => List a x -> List a y -> List a z
append Nil ys = ys
append (x ::: xs) ys = x ::: append xs ys
{-
GHC 6.4 says:
Couldn't match the rigid variable `y' against `Succ z'
`y' is bound by the type signature for `append'
Expected type: List a y
Inferred type: List a (Succ z)
In the expression: x ::: (append xs ys)
In the definition of `append': append (x ::: xs) ys
= x ::: (append xs ys)
-}
</pre>en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/345
Trac 1.0.9simonpjThu, 28 Sep 2006 12:06:38 GMTdescription changed; difficulty, os, architecture, milestone set
http://ghc.haskell.org/trac/ghc/ticket/345#comment:1
http://ghc.haskell.org/trac/ghc/ticket/345#comment:1
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>description</strong>
modified (<a href="/trac/ghc/ticket/345?action=diff&version=1">diff</a>)
</li>
<li><strong>os</strong>
set to <em>Unknown</em>
</li>
<li><strong>architecture</strong>
set to <em>Unknown</em>
</li>
<li><strong>milestone</strong>
set to <em>6.8</em>
</li>
</ul>
TicketsimonpjFri, 10 Nov 2006 12:59:16 GMTtestcase set
http://ghc.haskell.org/trac/ghc/ticket/345#comment:2
http://ghc.haskell.org/trac/ghc/ticket/345#comment:2
<ul>
<li><strong>testcase</strong>
set to <em>gadt-fd</em>
</li>
</ul>
TicketsimonpjFri, 10 Nov 2006 14:37:06 GMT
http://ghc.haskell.org/trac/ghc/ticket/345#comment:3
http://ghc.haskell.org/trac/ghc/ticket/345#comment:3
<p>
This one still doesn't work, even with the new implication-constraint machinery. It's a good example of the need for full-on equality constraints.
</p>
<p>
Simon
</p>
TicketjyrinxSat, 03 Mar 2007 07:26:17 GMT
http://ghc.haskell.org/trac/ghc/ticket/345#comment:4
http://ghc.haskell.org/trac/ghc/ticket/345#comment:4
<p>
GHC doesn't even like the first clause nowadays. Sez version 6.7.20070224:
</p>
<pre class="wiki"> Couldn't match expected type `z' (a rigid variable)
against inferred type `y' (a rigid variable)
`z' is bound by the type signature for `append' at Bug345.hs:16:19
`y' is bound by the type signature for `append' at Bug345.hs:16:17
Expected type: List a z
Inferred type: List a y
In the expression: ys
In the definition of `append': append Nil ys = ys
</pre><p>
(I did have to compile with -fallow-undecidable-instances, though.)
</p>
TicketguestTue, 03 Jul 2007 09:27:39 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/345#comment:5
http://ghc.haskell.org/trac/ghc/ticket/345#comment:5
<ul>
<li><strong>cc</strong>
<em>kyrab@…</em> added
</li>
</ul>
TicketguestTue, 03 Jul 2007 10:59:55 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/345#comment:6
http://ghc.haskell.org/trac/ghc/ticket/345#comment:6
<ul>
<li><strong>cc</strong>
<em>kyrab@…</em> added; <em>kyrab@…</em> removed
</li>
</ul>
TicketiglooTue, 03 Jul 2007 17:47:48 GMTpriority changed
http://ghc.haskell.org/trac/ghc/ticket/345#comment:7
http://ghc.haskell.org/trac/ghc/ticket/345#comment:7
<ul>
<li><strong>priority</strong>
changed from <em>normal</em> to <em>high</em>
</li>
</ul>
TicketsimonpjThu, 02 Aug 2007 07:47:34 GMT
http://ghc.haskell.org/trac/ghc/ticket/345#comment:8
http://ghc.haskell.org/trac/ghc/ticket/345#comment:8
<p>
See also <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1573" title="bug: GADT and typeclass funcional dependencies not working well together (closed: duplicate)">#1573</a>, which gives another example.
</p>
<p>
I plan to fix this by the upcoming work on indexed type families. Tom Schrivjers has built a prototype implementation, which mostly works. I need to review and commit it. Stay tuned.
</p>
<p>
Simon
</p>
TicketiglooThu, 09 Aug 2007 13:03:49 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/345#comment:9
http://ghc.haskell.org/trac/ghc/ticket/345#comment:9
<ul>
<li><strong>milestone</strong>
changed from <em>6.8</em> to <em>6.1</em>
</li>
</ul>
<p>
Simon PJ will look at this in the HEAD, after 6.8 is forked.
</p>
TicketsimonpjThu, 09 Aug 2007 13:05:59 GMT
http://ghc.haskell.org/trac/ghc/ticket/345#comment:10
http://ghc.haskell.org/trac/ghc/ticket/345#comment:10
<p>
To clarify, my intention is that we'll solve it with type functions, which will play nice with GADTs. I'm not sure fundeps ever will.
</p>
<p>
Simon
</p>
TicketchakTue, 11 Dec 2007 07:24:19 GMT
http://ghc.haskell.org/trac/ghc/ticket/345#comment:11
http://ghc.haskell.org/trac/ghc/ticket/345#comment:11
<p>
The corresponding problem in the type families world has now been fixed - eg <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1723" title="bug: type unsafety with type family + GADT (closed: fixed)">#1723</a>. I am unsure what the intention with this bug is. Close it, and tell people to use type families? Wait until FDs are being implemented by way of type families?
</p>
TicketsimonpjTue, 11 Dec 2007 09:21:09 GMTpriority, milestone changed
http://ghc.haskell.org/trac/ghc/ticket/345#comment:12
http://ghc.haskell.org/trac/ghc/ticket/345#comment:12
<ul>
<li><strong>priority</strong>
changed from <em>high</em> to <em>low</em>
</li>
<li><strong>milestone</strong>
changed from <em>6.10 branch</em> to <em>_|_</em>
</li>
</ul>
<p>
Ultimately, I think we can implement fundeps using type families, and then the fundep version will work too. Until then, it'll only work in type-family form.
</p>
<p>
So, since we now have a good workaround (well, actually, a better way to write the program rather than a workaround), I'll leave it open, but at low priority and with milestone bottom.
</p>
<p>
Simon
</p>
TicketsimonmarTue, 30 Sep 2008 15:37:40 GMTarchitecture changed
http://ghc.haskell.org/trac/ghc/ticket/345#comment:13
http://ghc.haskell.org/trac/ghc/ticket/345#comment:13
<ul>
<li><strong>architecture</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:52:01 GMTos changed
http://ghc.haskell.org/trac/ghc/ticket/345#comment:14
http://ghc.haskell.org/trac/ghc/ticket/345#comment:14
<ul>
<li><strong>os</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarThu, 19 Nov 2009 12:53:27 GMTfailure set
http://ghc.haskell.org/trac/ghc/ticket/345#comment:15
http://ghc.haskell.org/trac/ghc/ticket/345#comment:15
<ul>
<li><strong>failure</strong>
set to <em>GHC rejects valid program</em>
</li>
</ul>
TicketthomieSun, 24 Jan 2016 16:38:29 GMTcc changed; keywords set
http://ghc.haskell.org/trac/ghc/ticket/345#comment:16
http://ghc.haskell.org/trac/ghc/ticket/345#comment:16
<ul>
<li><strong>keywords</strong>
<em>GADTs</em> added
</li>
<li><strong>cc</strong>
<em>kyrab@…</em> <em>tomasz.zielonka@…</em> added; <em>kyrab@…</em> removed
</li>
</ul>
Ticket