#1330: Church2 test gives a rather confusing error with the HEAD
----------------------------------------+-----------------------------------
Reporter: igloo | Owner:
Type: bug | Status: new
Priority: normal | Milestone: 6.8
Component: Compiler (Type checker) | Version: 6.7
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Os: Unknown | Testcase: Church2
Architecture: Unknown |
----------------------------------------+-----------------------------------
Comment (by simonpj):
Sigh. This a great example of why typechecking for impredicative
polymorphism is so darn tricky. Here is what is happening. The call `n
(mul m) n1` means that we try to check `(mul m)` expecting it to have type
`CNat -> CNat`. Not knowing (yet) what type to instantiate `mul` to, we
instantiate it to type `box(a)`. So now we are faced with the task of
checking
{{{
box(a) -> box(a) <= CNat -> CNat
}}}
If you follow through the rules of Fig 3
of[http://research.microsoft.com/~simonpj/papers/boxy/boxy-icfp.pdf the
paper], we find that, from the ''argument'' side of the arrows we must
equate `box(a)` and `CNat`. That leaves us with the following problem:
{{{
box(CNat) -> box(CNat) <= CNat -> CNat
}}}
Looking now at the ''result''side of the arrow we get
{{{
box(CNat) <= CNat
}}}
You might think that this is obviously possible, but rule SKOL says to
instantiate the `CNat` onn the right; and that soon leads the reported
mis-match.
The trouble is that GHC does as much zonking as possible before reporting
the error, and does not show the boxes. Result: we display two identical-
looking types.
I'm not sure how to fix this, and in any case I'm unhappy with the
impredicative-polymoprhism story. So I'm going to leave this as one more
reason why the current story is unsatisfactory, and hope that Stephanie
and Dimitrios eventually show the way forward!
Meanwhile, better make this an expected failure.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1330>
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
