GHC: Ticket #2627: GADT + Type family doesn't unify like I expect
http://ghc.haskell.org/trac/ghc/ticket/2627
<p>
I'd expect this program to compile; the "given" equations in "conn" should add additional constraints to the types determined by the GADT. Instead it looks like (Dual a) is failing to unify with (R _ _), and the same for (Dual b) and (W _ _).
</p>
<pre class="wiki">{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls #-}
module Dual where
data R a b
data W a b
data Z
type family Dual a
type instance Dual Z = Z
type instance Dual (R a b) = W a (Dual b)
type instance Dual (W a b) = R a (Dual b)
data Comm a where
Rd :: (a -> Comm b) -> Comm (R a b)
Wr :: a -> Comm b -> Comm (W a b)
Fin :: Int -> Comm Z
conn :: (Dual a ~ b, Dual b ~ a) => Comm a -> Comm b -> (Int, Int)
conn (Fin x) (Fin y) = (x,y)
conn (Rd k) (Wr a r) = conn (k a) r
conn (Wr a r) (Rd k) = conn r (k a)
</pre><p>
Running off of GHC HEAD:
<tt>The Glorious Glasgow Haskell Compilation System, version 6.11.20080925</tt>
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/2627
Trac 1.0.1simonpjFri, 26 Sep 2008 17:30:34 GMTowner, difficulty set
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:1
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:1
<ul>
<li><strong>owner</strong>
set to <em>chak</em>
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
Nice example -- just the kind of interaction between GADTs and type functions that should now work. I've convinced myself that your code should indeed compile.
</p>
<p>
I stripped out a couple of eqns in the example, and wrote out the derivation that shows it should typecheck.
</p>
<p>
Manuel, over to you!
</p>
<p>
Simon
</p>
<pre class="wiki">conn :: (Dual a ~ b, Dual b ~ a) => Comm a -> Comm b -> (Int, Int)
conn (Rd k) (Wr a r) = conn (k a) r
-- conn (Fin x) (Fin y) = (x,y)
-- conn (Wr a r) (Rd k) = conn r (k a)
{- Simon's reasoning
Given :: Dual a ~ b, Dual b ~ a (sig)
a ~ R a1 b1, b ~ W a2 b2 (gadt match)
k :: a1 -> Con b1
a :: a2
r :: Conn b2
Instantiate conn at: ai, bi (unification variables)
Wanted: Dual ai ~ bi, Dual bi ~ ai
first arg: a1~a2, b1~ai
second: b2~bi
Fixing the unification variables is easy: ai:=b1, bi:=b2
The interesting thing is figuring out that a1~a2
Wanted: a1~a2
Given: Dual a ~ b
=> (substitute for a) Dual (R a1 b1) ~ b
=> (top-level eqn) W a1 (Dual b1) ~ b
=> (substitute for b) W a1 (Dual b1) ~ W a2 b2
=> (decompose) a1~a2
-}
</pre>
TicketsimonpjFri, 26 Sep 2008 17:34:50 GMT
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:2
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:2
<p>
PS. The error message looks like
</p>
<pre class="wiki">T2627.hs:19:13:
Couldn't match expected type `b2' against inferred type `Dual b1'
`b2' is a rigid type variable bound by
the constructor `Wr' at T2627.hs:19:13
In the pattern: Wr a r
In the definition of `conn': conn (Rd k) (Wr a r) = conn (k a) r
</pre><p>
but I'd expect it to say something like "cannot deduce <tt>(b2 ~ Dual b1)</tt> from from <tt>(b ~ Dual a, a ~ Dual b, ... blah blah)</tt>". The current error message is really only right for things like "cannot unify <tt>[a]</tt> against <tt>Maybe Int</tt>" or something.
</p>
TicketryaniFri, 26 Sep 2008 19:09:52 GMT
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:3
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:3
<p>
While playing around with this I also found a crash bug:
</p>
<p>
<tt>conn (Rd k) (Wr a r) = undefined -- typechecks successfully</tt>
<tt>conn (Rd k) (Wr a r) = conn undefined undefined -- crashes</tt>
</p>
<pre class="wiki">ghc: panic! (the 'impossible' happened)
(GHC version 6.11.20080925 for i386-apple-darwin):
TcTyFuns.uMeta: unexpected synonym family
</pre><p>
Interestingly, this example just fails to typecheck:
</p>
<p>
<tt>urk () = conn undefined undefined</tt>
</p>
<p>
with an unhelpful error message:
</p>
<pre class="wiki">Dual.hs:1:0:
Couldn't match expected type `a'
against inferred type `Dual (Dual a)'
</pre><p>
Note the line number of the error... If I remove the () to force the monomorphism restriction to kick in, the line number is more helpful.
</p>
<p>
I find it fascinating that with type equality constraints, "undefined" is no longer a valid argument at all call-sites.
</p>
TicketchakTue, 30 Sep 2008 02:04:41 GMTtestcase set
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:4
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:4
<ul>
<li><strong>testcase</strong>
set to <em>T2627</em>
</li>
</ul>
<p>
Fixed the main issue (and added the code to the test suite).
</p>
<p>
However, the <tt>TcTyFuns.uMeta: unexpected synonym family</tt> issue is still remaining.
</p>
TicketchakTue, 30 Sep 2008 05:34:10 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:5
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:5
<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>
Fixed the panic, too.
</p>
TicketsimonmarTue, 30 Sep 2008 15:40:45 GMTarchitecture changed
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:6
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:6
<ul>
<li><strong>architecture</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:52:00 GMTos changed
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:7
http://ghc.haskell.org/trac/ghc/ticket/2627#comment:7
<ul>
<li><strong>os</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
Ticket