#5591: Type constructor variables not injective
----------------------------------------+-----------------------------------
Reporter: daniel.is.fischer | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.2.1
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Changes (by simonpj):
* cc: dimitris@…, sweirich@…, byorgey@… (added)
Comment:
As Brent describes on [http://stackoverflow.com/questions/7866375/why-
does-ghc-think-that-this-type-variable-is-not-injective/ StackOverflow],
we did make a change that simplified GHC's internal language a bit, and
allowed us to have unsaturated type functions. The change is described in
6.2 of our POPL'11 paper [http://research.microsoft.com/en-
us/um/people/simonpj/papers/ext-f/popl163af-weirich.pdf Generative type
abstraction and type-level computation].
Daniel Shussler's email also describes a trick due to Oleg that makes his
program compile. Well, it turns out that this trick is really a bug; with
the restrictions describe in our paper, we should not allow type functions
to match on an argument of shape `(a b)`.
So far as we can all remember, the ''only'' reason for the new story was
to allow un-saturated type functions in the intermediate language. But we
can't allow them in the ''source'' language because that would mess up
type inference. So we are paying the price (exemplified by this ticket)
without getting much benefit.
Brent's conclusion on !StackOverflow is that we should go back to
* having `left` and `right` coercion combinators
* requiring type functions to be saturated in the intermediate language
(as well as source)
And that in turn would allow us to type check the program in this ticket.
So that's the plan I think. But gotta get 7.4 out first.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5591#comment:2>
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
