Shouldn't this require ImpredicativeTypes?
The following program compiles:
{-# LANGUAGE RankNTypes #-}
module TestRN1 where
type X = forall a . a
comp :: (X -> c) -> (a -> X) -> (a -> c)
comp = (.)
But this one fails:
{-# LANGUAGE RankNTypes #-}
module TestRN2 where
comp :: ((forall a . a) -> c) -> (a -> (forall a . a)) -> (a -> c)
comp = (.)
Error:
Cannot instantiate unification variable ‘b0’
with a type involving foralls: forall a1. a1
Perhaps you want ImpredicativeTypes
In the expression: (.)
In an equation for ‘comp’: comp = (.)
I would expect both to fail. Both seem to rely on impredicative types. I wouldn't expect expansion of a type synonym to make a difference between a type-checking program and one that does not typecheck.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.4 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |