#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
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
