Opened 3 years ago

Closed 2 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 Revisions:


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 3 years ago by michalt

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

foo :: GADT Char
foo = undefined

test = mkString foo

which instance should be called? The one for Int or Bool?

comment:2 Changed 3 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 3 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 3 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 3 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:

       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 2 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 2 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 2 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.

Note: See TracTickets for help on using tickets.