Opened 4 years ago
Closed 3 years ago
#6074 closed feature request (wontfix)
Instance inference failure with GADTs
Reported by: | goldfire | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 7.8.1 |
Component: | Compiler (Type checker) | Version: | 7.5 |
Keywords: | GADTs | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
Consider the following code:
{-# 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
The function mkString does not compile, while the function mkString' does. The problem seems to be that there is no instance declaration for GADT a, although there are instances for all the possible instantiations of a. It seems that requiring a case statement where all patterns are accounted for and all branches contain the same expression should be unnecessary.
This was tested on 7.5.20120426.
Change History (8)
comment:1 Changed 4 years ago by michalt
comment:2 Changed 4 years ago by dreixel
I think this is a feature request. Indeed michalt points out that this cannot work in the way presented. But what if we use XDataKinds?
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
Now we know that the instances of Stringable for GADT a cover all possible types of a!
comment:3 Changed 4 years ago by simonpj
- difficulty set to Unknown
I think this is a non-starter. Consider the translation of the orignal code into FC:
mkString' :: GADT a -> String mkString' g = case g of GInt -> toString Int dStringableInt g GBool -> toString Bool dStringableBool g
Remember that toString :: forall a. Stringable a => a -> String. So it takes a value argument that is a Stringable 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.)
Another way to put it is: what is the FC translation of this?
mkString :: GADT a -> String mkString g = toString g
So I don't see where to go with this one.
comment:4 Changed 4 years ago by goldfire
- Type changed from bug to feature request
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 undefined and friends. And, in truth, my situation is the one dreixel points out, where I'm using a closed data kind.
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.
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.
comment:5 Changed 4 years ago by dreixel
I think there's quite some interest in this feature. Ian previously pointed out this example:
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)
This triggers an error:
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))
But we know what F i can give us for any i :: MyKind, and that is Int or Bool, both unproblematic for deriving Data. In particular, we know that the type family F is closed! The general question is how we can have the type checker take advantage of this.
comment:6 Changed 3 years ago by igloo
- Component changed from Compiler to Compiler (Type checker)
- Milestone set to 7.8.1
If in dreixel's version I change the mkString definition to
mkString :: GADT a -> GADT a mkString g = g
then the core looks like this:
Main.mkString :: forall (a :: Main.Index). Main.GADT a -> Main.GADT a Main.mkString = \ (@ (b :: Main.Index)) (g :: Main.GADT b) -> g
As b is a type, presumably it is never _|_. Are we allowed to pattern match on b at this point, or is it going to be erased later on?
If we can match on b then something may be possible, but otherwise I agree that it looks like a non-starter.
comment:7 Changed 3 years ago by simonpj
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!
comment:8 Changed 3 years ago by igloo
- Resolution set to wontfix
- Status changed from new to closed
OK, I don't see this ticket going anywhere then, so closing.
I'm definitely not an expert with type systems, but I don't think GHC can do that. The problem is that a can be in fact anything. Consider something like:
which instance should be called? The one for Int or Bool?