GHC: Ticket #2855: Surprising type (family) type derived
http://ghc.haskell.org/trac/ghc/ticket/2855
<p>
Consider the following module
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
module Bug5 where
class C a where
type T a
f :: T a -> T a -> T a
data D a = D { t :: T a }
g r = f (t r) (t r)
</pre><p>
Now ask for the type of g
</p>
<pre class="wiki">*Bug5> :t g
g :: (T a ~ T a1, C a1) => D a -> T a1
</pre><p>
Why isn't the type
</p>
<pre class="wiki">g :: (C a) => D a -> T a
</pre><p>
?
</p>
<p>
The strange type is a minor nuisance, but it gets worse
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
module Bug6 where
class C a where
type T a
type U a
f :: T a -> T a -> T a
x :: U a -> T a
data D a = D { t :: T a, u :: U a }
g r = f (t r) (x (u r))
</pre><p>
This doesn't type check at all.
</p>
<p>
An even simpler example that fails:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
module Bug7 where
class C a where
type T a
type U a
x :: U a -> T a
data D a = D (U a)
g :: (C a) => D a -> T a
g (D u) = x u
</pre>en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/2855
Trac 1.0.7guestMon, 08 Dec 2008 15:53:27 GMT
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:1
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:1
<p>
Here's more of the same kind:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
module Bug8 where
class C a where
type T a
type U a
x :: U a -> T a
--foo :: (C a) => U a -> T a
foo ua = x ua
</pre><p>
This compiles, and the type of foo is the one in the signature.
But if the signature is included there are type errors.
</p>
TicketsimonpjMon, 08 Dec 2008 16:48:36 GMTtype changed; difficulty set
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:2
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:2
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>type</strong>
changed from <em>bug</em> to <em>feature request</em>
</li>
</ul>
<p>
I'm afraid these aren't bugs. They all arise because type synonym families (unlike data type families) do not have to be injective. For example you ask re <tt>Bug5</tt> why GHC doesn't get the type
</p>
<pre class="wiki">g :: (C a) => D a -> T a
</pre><p>
Answer: because that's not the most general type. The type GHC gives is strictly more general. Suppose
</p>
<pre class="wiki">type instance T Int = Char
type instance T Bool = Char
</pre><p>
then <tt>T Int ~ T Bool</tt>, but of course <tt>Int</tt> and <tt>Bool</tt> are different types.
</p>
<p>
The other examples you give are more tiresome. For example:
</p>
<pre class="wiki">class C a where
type T a
type U a
x :: U a -> T a
data D a = D (U a)
g :: (C a) => D a -> T a
g (D u) = x u
</pre><p>
We know that <tt>(u :: U a)</tt>, but at what type should we call the polymorphic function <tt>x</tt>? Let's say at some type <tt>a1</tt>. Then since <tt>x</tt> is applied to <tt>u</tt> we know that <tt>U a</tt> should be the same type as <tt>U a1</tt>, <em>but that does not require <tt>a</tt> to be the same type as <tt>a1</tt></em>, as we saw above.
</p>
<p>
In this case, it's vexing because the only solution to <tt>(U a ~ U a1)</tt>, where (i) <tt>a</tt> is a skolem constant, and (ii) no other equality constraints are available to solve it, is <tt>a~a1</tt>. But GHC doesn't do that kind of "the only solution" reasoning. Yet anyway.
</p>
<p>
In general, a function with a polymorphic type variable that occurs only under a type function is likely to give rise to this kind of trouble.
</p>
<p>
We're also thinking about allowing you to declare theat a type function is injective, which would solve this problem in a different way.
</p>
<p>
I hope that explains it a bit. I'll leave this open as a feature request... perhaps for injective type functions. (Although I'm not sure whether that'd work in your application.)
</p>
<p>
Simon
</p>
TicketguestMon, 08 Dec 2008 17:13:54 GMT
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:3
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:3
<p>
So what about my attached last example? It's another one of these the type that ghc reports cannot be inserted in the code. Very frustrating.
</p>
<p>
You say "At what type should we call the poymorphic function x?" Well, I want it to be the x from the dictionary (C a) that I'm passing. So there is no doubt at what type it should be called, it's at type (U a). I guess there's no way to express that.
</p>
<p>
This is very annoying, because it means that the associated types simply don't work for some of the tasks that I thought they were supposed to solve.
I can provide a real life example if that helps.
</p>
TicketsimonpjMon, 08 Dec 2008 17:27:57 GMT
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:4
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:4
<p>
Several things going on here. Concerning type signatures, it's indeed annoying that a program can have an inferred type that can't be used as a type signature. I plan to fix that by rejecting both programs. You won't like that, but it's silly to accept one but not the other. I think there's a ticket open for this, but I'm not sure which one...
</p>
<p>
Concering "I want it to be the x from the dictionary (C a) that I'm passing". Yes, I know. That's why I said it's vexing; indeed, the solution you suggest is the <em>only</em> solution that will work. All I'm saying is that this is a new form of reasoning, which GHC does not in any way implement at the moment. It'd take a bit of study to figure out how to do it, or indeed if there is any well-behaved, principal solution. If you can work one out, do tell us!
</p>
<p>
Can you not design your functions so that they take at least one parameter that does not live inside a type-function application? Or, would you be willing for your type functions to be injective, or would that be too restrictive for your application?
</p>
<p>
Simon
</p>
TicketchakTue, 09 Dec 2008 02:17:04 GMT
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:5
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:5
<p>
This is a duplicate of <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1897" title="bug: Ambiguous types and rejected type signatures (closed: fixed)">#1897</a>, is it not?
</p>
<p>
As far as I am concerned, I still think, we should solve this problem in the way Lennart proposed when we discussed this last: <a class="ext-link" href="http://www.mail-archive.com/haskell-cafe@haskell.org/msg39774.html"><span class="icon"></span>http://www.mail-archive.com/haskell-cafe@haskell.org/msg39774.html</a> (after type inference, do type <strong>checking</strong> again with the inferred signatures).
</p>
TicketsimonpjTue, 09 Dec 2008 09:09:03 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:6
http://ghc.haskell.org/trac/ghc/ticket/2855#comment:6
<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>
Yes, it's a dup. So I'll close it now, having linked from <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1897" title="bug: Ambiguous types and rejected type signatures (closed: fixed)">#1897</a>
</p>
<p>
Simon
</p>
Ticket