GHC: Ticket #2418: desugaring type function application to constraint makes bug disappear
http://ghc.haskell.org/trac/ghc/ticket/2418
<p>
When considering type functions, I find it helpful to desugar their applications into additional constraints (<code>tf a</code> becomes <code>tf a~tfa=>tfa</code>). But consider this example from a recent <a class="ext-link" href="http://www.haskell.org/pipermail/haskell-cafe/2008-July/044911.html"><span class="icon"></span>haskell-cafe thread</a>:
</p>
<pre class="wiki">{-# OPTIONS_GHC -fglasgow-exts #-}
class Blah f a where blah :: a -> T f f a
class A f where type T f :: (* -> *) -> * -> *
-- wrapper :: forall a f tf . (Blah f a,T f~tf) => a -> tf f a
wrapper :: forall a f . (Blah f a) => a -> T f f a
wrapper x = blah x
</pre><p>
for which <code>GHCi, version 6.9.20080514</code> yields:
</p>
<pre class="wiki">C:\Documents and Settings\cr3\Desktop\TF.hs:8:12:
Could not deduce (Blah f a) from the context (Blah f1 a)
arising from a use of `blah'
at C:\Documents and Settings\cr3\Desktop\TF.hs:8:12-17
Possible fix:
add (Blah f a) to the context of the type signature for `wrapper'
In the expression: blah x
In the definition of `wrapper': wrapper x = blah x
C:\Documents and Settings\cr3\Desktop\TF.hs:8:12:
Couldn't match expected type `T f1 f1 a'
against inferred type `T f f a'
In the expression: blah x
In the definition of `wrapper': wrapper x = blah x
Failed, modules loaded: none.
</pre><p>
Switching to the desugared version of the <code>wrapper</code> signature makes the error go away, so the "desugared" and original version are not equivalent in the current implementation of type families! See also <a class="ext-link" href="http://www.haskell.org/pipermail/haskell-cafe/2008-July/044914.html"><span class="icon"></span>http://www.haskell.org/pipermail/haskell-cafe/2008-July/044914.html</a>.
</p>
<p>
For added fun, GHCi reports the sugared type when using the desugared one:
</p>
<pre class="wiki">*Main> :t wrapper
wrapper :: (Blah f a) => a -> T f f a
</pre>en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/2418
Trac 1.2simonpjFri, 04 Jul 2008 11:59:08 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:1
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:1
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
Thanks. We're collecting type-function-related bugs here <a class="ext-link" href="http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsStatus"><span class="icon"></span>http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsStatus</a>. Manuel is on the job, now that his exam season is nearly over.
</p>
<p>
Simon
</p>
TicketiglooSun, 06 Jul 2008 18:03:44 GMTmilestone set
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:2
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:2
<ul>
<li><strong>milestone</strong>
set to <em>6.10.1</em>
</li>
</ul>
TicketchakTue, 08 Jul 2008 06:18:30 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:3
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:3
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>duplicate</em>
</li>
</ul>
<p>
This is actually a duplicate of <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2146" title="#2146: bug: Decomposition rule for equalities is too weak in case of higher-kinded ... (closed: fixed)">#2146</a> (which more accurately pinpoints the underlying problem).
</p>
TicketclausTue, 08 Jul 2008 09:13:55 GMT
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:4
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:4
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2418#comment:3" title="Comment 3">chak</a>:
</p>
<blockquote class="citation">
<p>
This is actually a duplicate of <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2146" title="#2146: bug: Decomposition rule for equalities is too weak in case of higher-kinded ... (closed: fixed)">#2146</a> (which more accurately pinpoints the underlying problem).
</p>
</blockquote>
<p>
How so? I had some trouble reconstructing the intended example in <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2146" title="#2146: bug: Decomposition rule for equalities is too weak in case of higher-kinded ... (closed: fixed)">#2146</a>, but given the implicit constraints (higher-kinded & ignores first parameter), I assume it is something like:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
type family F a :: * -> *
type instance F a = (,) String
foo :: (F Int a ~ F Int [a]) => a -> [a]
foo = undefined
foo' :: (F Int a ~ F Bool [a]) => a -> [a]
foo' = undefined
</pre><p>
for which <code>GHCi, version 6.9.20080514</code> (a version that fails the desugaring test) gives the expected errors
</p>
<pre class="wiki">C:\Documents and Settings\cr3\Desktop\F.hs:6:0:
Occurs check: cannot construct the infinite type: a = [a]
When generalising the type(s) for `foo'
C:\Documents and Settings\cr3\Desktop\F.hs:9:0:
Occurs check: cannot construct the infinite type: a = [a]
When generalising the type(s) for `foo''
Failed, modules loaded: none.
</pre>
TicketchakWed, 09 Jul 2008 02:41:08 GMT
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:5
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:5
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2418#comment:4" title="Comment 4">claus</a>:
</p>
<blockquote class="citation">
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2418#comment:3" title="Comment 3">chak</a>:
</p>
<blockquote class="citation">
<p>
This is actually a duplicate of <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2146" title="#2146: bug: Decomposition rule for equalities is too weak in case of higher-kinded ... (closed: fixed)">#2146</a> (which more accurately pinpoints the underlying problem).
</p>
</blockquote>
<p>
How so?
</p>
</blockquote>
<p>
<code>T</code> is a unary type synonym family, so in
</p>
<pre class="wiki">wrapper :: forall a f . (Blah f a) => a -> T f f a
</pre><p>
you should read the result type as <code>(T f) f a</code>, where <code>T f</code> is the <em>family application,</em> whereas the application of <code>(T f)</code> to the second <code>f</code> and to <code>a</code> are vanilla type applications. The bug is that GHC mistakenly takes the whole of <code>T f f a</code> as tertiary family application. (If it <em>were</em> a tertiary family application, the signature would be ambiguous and the error message would be correct - but it's unary, so GHC is wrong in rejecting the program.)
</p>
<p>
This also explains why what you call the desugared variant works:
</p>
<pre class="wiki">wrapper :: forall a f tf . (Blah f a,T f~tf) => a -> tf f a
</pre><p>
Here <code>tf f a</code> syntactically contains no type family. So, GHC correctly takes this to be vanilla type applications.
</p>
<p>
The place in the type checker where things go wrong is in the implementation of what we call the <em>decomposition rule</em> (see our forthcoming ICFP'08 paper for details on the type checking algorithm). That's exactly what <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2146" title="#2146: bug: Decomposition rule for equalities is too weak in case of higher-kinded ... (closed: fixed)">#2146</a> is about. (In any case, I will also add the example of the present ticket to the testsuite when I fix the bug.)
</p>
TicketsimonmarTue, 30 Sep 2008 15:40:40 GMTarchitecture changed
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:6
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:6
<ul>
<li><strong>architecture</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:51:53 GMTos changed
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:7
http://ghc.haskell.org/trac/ghc/ticket/2418#comment:7
<ul>
<li><strong>os</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
Ticket