#4347: Asymmetry of (impredicative) instantiation/higher rank types -------------------------------+-------------------------------------------- Reporter: dolio | Owner: Type: bug | Status: new Priority: normal | Component: Compiler (Type checker) Version: 7.1 | Keywords: Testcase: | Blockedby: Os: Linux | Blocking: Architecture: x86_64 (amd64) | Failure: GHC rejects valid program -------------------------------+-------------------------------------------- The new type checker in GHC 7 seems to reject some cases of impredicative instantiation that prior versions allowed. I was initially alerted to this by Simon Marlow, who sent a patch for vector-algorithms removing a use of {{{($)}}} where it would have to be instantiated impredicatively.
Initially, I thought this was due to a planned removal of impredicativity, but this cannot be the case, because: {{{ const :: a -> (forall b. b) -> a }}} is accepted by the type checker. However, the simple: {{{ id :: (forall a. a) -> (forall b. b) }}} is not, giving an error message: {{{ Couldn't match type `b' with `forall a. a' `b' is a rigid type variable bound by an expression type signature at <interactive>:1:32 In the expression: id :: (forall a. a) -> (forall b. b) }}} This would seem to indicate that the type is being rewritten to: {{{ forall b. (forall a. a) -> b }}} and then the {{{forall a. a}}} matched with the bare {{{b}}}. It is, of course, fine to rewrite the type this way, since the two are isomorphic, but it is unfortunate that it causes the checker to reject what would otherwise be a valid instantiation. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4347> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler _______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs