#1123: Impredicativity bug: forall not hoisted properly
--------------------------------------------------+-------------------------
Reporter: Ashley Yakeley <[EMAIL PROTECTED]> | Owner: simonpj
Type: bug | Status: new
Priority: normal | Milestone: 6.10 branch
Component: Compiler | Version: 6.6
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
--------------------------------------------------+-------------------------
Comment (by simonpj):
You are definitely required to do so! Consider this simpler version:
{{{
data M s a = M (ST s a)
runM :: forall b. Int -> (forall s. M s b) -> b
runM n (M m) = runST m
}}}
What type does `m` have in the RHS of `runM`? You want it to have type
`forall s. ST s b`. So you want the pattern matching on `(M m)` to first
specialise the argument and then re-generalise. I can see why you might
think that'd work, but try writing it in System F:
{{{
runM = /\b. \n:Int. \x:(forall x. M s b).
case (x ???) of
M m -> runST (/\s. ???)
}}}
The only way to make this work is to move the pattern match inside the big
lambda thus:
{{{
runM = /\b. \n:Int. \x:(forall x. M s b).
runST (/\s. case (x s) of
M m -> m)
}}}
And that is just what your un-newtyping function does.
I'm leaving the bug open for its original report though.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1123#comment:10>
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
