Higher rank typechecking is broken
The oddity was noticed when someone asked the type of lens
from lambdabot and it replied with
1514165211 [04:26:51] <lambdabot> Functor f => (s1 -> a1) -> (s1 -> b1 -> t1) -> (a2 -> f b2) -> s2 -> f t2
This disagrees with lens
's type per definition (way too many foralls and unconstrained type variables), and if handled carefully it could be used to implement unsafeCoerce
within SafeHaskell.
The minimalest example I could come up with:
{-# LANGUAGE RankNTypes #-}
safeCoerce :: a -> b
safeCoerce = f'
where
f :: d -> forall c. d
f x = x
f' = f
This compiles and typechecks on GHC 8.2.2, 8.2.1 (courtesy of hydraz) and HEAD. But not on 8.0.2 (hydraz) or 7.10.3.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | highest |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | hydraz |
Operating system | |
Architecture |