Haskell › Haskell - Glasgow-haskell-bugs

[GHC] #6074: Instance inference failure with GADTs

Classic

List

Threaded

9 messages Options

GHC

[GHC] #6074: Instance inference failure with GADTs

#6074: Instance inference failure with GADTs
------------------------------+---------------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler
Version: 7.5 | Keywords: GADTs
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby: | Blocking:
Related: |
------------------------------+---------------------------------------------
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.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6074>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6074: Instance inference failure with GADTs

GHC

Re: [GHC] #6074: Instance inference failure with GADTs

In reply to this post by GHC

#6074: Instance inference failure with GADTs
------------------------------+---------------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler
Version: 7.5 | Keywords: GADTs
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby: | Blocking:
Related: |
------------------------------+---------------------------------------------

Comment(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`!

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6074#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6074: Instance inference failure with GADTs

In reply to this post by GHC

#6074: Instance inference failure with GADTs
---------------------------------+------------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.5
Keywords: GADTs | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Changes (by simonpj):

* difficulty: => Unknown

Comment:

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.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6074#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6074: Instance inference failure with GADTs

In reply to this post by GHC

#6074: Instance inference failure with GADTs
---------------------------------+------------------------------------------
Reporter: goldfire | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.5
Keywords: GADTs | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Changes (by goldfire):

* type: bug => feature request

Comment:

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.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6074#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6074: Instance inference failure with GADTs

In reply to this post by GHC

#6074: Instance inference failure with GADTs
---------------------------------+------------------------------------------
Reporter: goldfire | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.5
Keywords: GADTs | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------

Comment(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.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6074#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6074: Instance inference failure with GADTs

In reply to this post by GHC

#6074: Instance inference failure with GADTs
----------------------------------------+-----------------------------------
Reporter: goldfire | Owner:
Type: feature request | Status: new
Priority: normal | Milestone: 7.8.1
Component: Compiler (Type checker) | Version: 7.5
Keywords: GADTs | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
----------------------------------------+-----------------------------------
Changes (by igloo):

* component: Compiler => Compiler (Type checker)
* milestone: => 7.8.1

Comment:

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.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6074#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6074: Instance inference failure with GADTs

In reply to this post by GHC

GHC

Re: [GHC] #6074: Instance inference failure with GADTs

In reply to this post by GHC

#6074: Instance inference failure with GADTs
--------------------------------------+-------------------------------------
Reporter: goldfire | Owner:
Type: feature request | Status: closed
Priority: normal | Milestone: 7.8.1
Component: Compiler (Type checker) | Version: 7.5
Resolution: wontfix | Keywords: GADTs
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Difficulty: Unknown
Testcase: | Blockedby:
Blocking: | Related:
--------------------------------------+-------------------------------------
Changes (by igloo):

* status: new => closed
* resolution: => wontfix

Comment:

OK, I don't see this ticket going anywhere then, so closing.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6074#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs