#5678: Unexpected cryptic GADT type error
---------------------------------+------------------------------------------
Reporter: mikhail.vorozhtsov | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.3
Resolution: invalid | Keywords:
Testcase: | Blockedby:
Difficulty: | Os: Unknown/Multiple
Blocking: | Architecture: Unknown/Multiple
Failure: None/Unknown |
---------------------------------+------------------------------------------
Changes (by simonpj):
* status: new => closed
* resolution: => invalid
Comment:
It's not a bug, I'm afraid. Type inference for GADT programs requires
enough type signatures to work, and this program doesn't. Consider
{{{
void :: Functor f => f a -> f ()
}}}
So the call of `void` gives no clue about what the `a` of `f a` is. It
would have to be purely inferred. So what is the type of the argument?
{{{
case G of G -> return "xyz"
}}}
In this case it can only be `String`, but suppose we had `(x :: G a)`;
what is the type of
{{{
case x of G -> return 3
}}}
is it `n a` or `m Int`? There is no most-general type, and that's the
trouble.
Now, the error message is not a thing of beauty. But it means that we are
unifying the type inside (`String` here) with the type from outside `a0`,
which instantiated the call to `void`. If people can think of a better
way to report such errors it'd be great.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5678#comment:1>
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
