GHC: Ticket #6074: Instance inference failure with GADTs
http://ghc.haskell.org/trac/ghc/ticket/6074
<p>
Consider the following code:
</p>
<pre class="wiki">{-# LANGUAGE GADTs, FlexibleInstances #-}
class Stringable a where
toString :: a -> String
data GADT a where
GInt :: GADT Int
GBool :: GADT Bool
instance Stringable (GADT Int) where
toString _ = "constructor GInt"
instance Stringable (GADT Bool) where
toString _ = "constructor GBool"
mkString :: GADT a -> String
mkString g = toString g
mkString' :: GADT a -> String
mkString' g = case g of
GInt -> toString g
GBool -> toString g
</pre><p>
The function <tt>mkString</tt> does not compile, while the function <tt>mkString'</tt> does. The problem seems to be that there is no instance declaration for <tt>GADT a</tt>, although there are instances for all the possible instantiations of <tt>a</tt>. It seems that requiring a <tt>case</tt> statement where all patterns are accounted for and all branches contain the same expression should be unnecessary.
</p>
<p>
This was tested on 7.5.20120426.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/6074
Trac 1.0.1michaltFri, 04 May 2012 11:39:42 GMT
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:1
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:1
<p>
I'm definitely not an expert with type systems, but I don't think GHC can do
that. The problem is that <tt></tt><tt>a</tt><tt></tt> can be in fact anything. Consider something
like:
</p>
<pre class="wiki">foo :: GADT Char
foo = undefined
test = mkString foo
</pre><p>
which instance should be called? The one for <tt></tt><tt>Int</tt><tt></tt> or <tt></tt><tt>Bool</tt><tt></tt>?
</p>
TicketdreixelFri, 04 May 2012 12:09:11 GMT
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:2
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:2
<p>
I think this is a feature request. Indeed michalt points out that this cannot work in the way presented. But what if we use <tt>XDataKinds</tt>?
</p>
<pre class="wiki">data Index = TInt | TBool
data GADT (a :: Index) where
GInt :: GADT TInt
GBool :: GADT TBool
class Stringable a where
toString :: a -> String
instance Stringable (GADT TInt) where
toString _ = "constructor GInt"
instance Stringable (GADT TBool) where
toString _ = "constructor GBool"
mkString :: GADT a -> String
mkString g = toString g
</pre><p>
Now we know that the instances of <tt>Stringable</tt> for <tt>GADT a</tt> cover all possible types of <tt>a</tt>!
</p>
TicketsimonpjFri, 04 May 2012 13:07:36 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:3
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:3
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
I think this is a non-starter. Consider the translation of the orignal code into FC:
</p>
<pre class="wiki">mkString' :: GADT a -> String
mkString' g = case g of
GInt -> toString Int dStringableInt g
GBool -> toString Bool dStringableBool g
</pre><p>
Remember that <tt>toString :: forall a. Stringable a => a -> String</tt>. So it takes a value argument that is a <tt>Stringable</tt> dictionary. And the two calls may LOOK the same to you, but they aren't really the same: we must pass two different dictionaries (in this case gotten from the two instance declarations. (And there's a different type parameter too.)
</p>
<p>
Another way to put it is: what is the FC translation of this?
</p>
<pre class="wiki">mkString :: GADT a -> String
mkString g = toString g
</pre><p>
So I don't see where to go with this one.
</p>
TicketgoldfireFri, 04 May 2012 13:20:38 GMTtype changed
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:4
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:4
<ul>
<li><strong>type</strong>
changed from <em>bug</em> to <em>feature request</em>
</li>
</ul>
<p>
Yes, I was worried about all of these problems when I made the post. It seems possible to circumvent the problem michalt brings up with some strictness guarantee to eliminate the possibility of <tt>undefined</tt> and friends. And, in truth, my situation is the one dreixel points out, where I'm using a closed data kind.
</p>
<p>
But, of course, simonpj's point is well taken and was my chief worry. I guess my best hope would be that there could be some construct that produces the pattern-match automatically when given the term to match over and the branch expression. In fact, I played around writing some such construct in Template Haskell, but TH doesn't have access to inferred types of expressions, so it's quite clunky to use.
</p>
<p>
I doubt there's much interest in this particular feature, so I'll just change the ticket to be a feature request and go back to the drawing board on my own design. Thanks for the feedback.
</p>
TicketdreixelFri, 04 May 2012 13:30:36 GMT
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:5
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:5
<p>
I think there's quite some interest in this feature. Ian previously pointed out this example:
</p>
<pre class="wiki"> data MyKind = K1 | K2
type family F (i :: MyKind) :: *
type instance F K1 = Int
type instance F K2 = Bool
data D i = D (F i)
deriving (Data, Typeable)
</pre><p>
This triggers an error:
</p>
<pre class="wiki"> 3.hs:13:15:
No instances for (Data (F i), Typeable (D i))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add instance declarations for (Data (F i), Typeable (D i))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Data (D i))
</pre><p>
But we know what <tt>F i</tt> can give us for any <tt>i :: MyKind</tt>, and that is <tt>Int</tt> or <tt>Bool</tt>, both unproblematic for deriving <tt>Data</tt>. In particular, we know that the type family <tt>F</tt> is closed! The general question is how we can have the type checker take advantage of this.
</p>
TicketiglooTue, 09 Oct 2012 15:54:28 GMTcomponent changed; milestone set
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:6
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:6
<ul>
<li><strong>component</strong>
changed from <em>Compiler</em> to <em>Compiler (Type checker)</em>
</li>
<li><strong>milestone</strong>
set to <em>7.8.1</em>
</li>
</ul>
<p>
If in dreixel's version I change the <tt>mkString</tt> definition to
</p>
<pre class="wiki">mkString :: GADT a -> GADT a
mkString g = g
</pre><p>
then the core looks like this:
</p>
<pre class="wiki">Main.mkString :: forall (a :: Main.Index). Main.GADT a -> Main.GADT a
Main.mkString = \ (@ (b :: Main.Index)) (g :: Main.GADT b) -> g
</pre><p>
As <tt>b</tt> is a type, presumably it is never <tt>_|_</tt>. Are we allowed to pattern match on <tt>b</tt> at this point, or is it going to be erased later on?
</p>
<p>
If we can match on <tt>b</tt> then something may be possible, but otherwise I agree that it looks like a non-starter.
</p>
TicketsimonpjTue, 09 Oct 2012 16:08:52 GMT
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:7
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:7
<p>
No, types are erased at runtime. You can't match on them. That's what GADTs are for: value-level things where matching conveys type information!
</p>
TicketiglooTue, 09 Oct 2012 16:13:41 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:8
http://ghc.haskell.org/trac/ghc/ticket/6074#comment:8
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>wontfix</em>
</li>
</ul>
<p>
OK, I don't see this ticket going anywhere then, so closing.
</p>
Ticket