Impredicativity is still sneaking in
This is erroneously accepted:
{-# LANGUAGE RankNTypes #-}
module Bug where
foo :: forall a. (Show a => a -> a) -> ()
foo = undefined
undefined
is being instantiated at (Show a => a -> a) -> ()
, which requires impredicativity. GHC does the right thing (reject!) if we try to instantiate with a type involving proper foralls.
I imagine this is a simple missing check.
Trac metadata
Trac field | Value |
---|---|
Version | 8.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |