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 t2This 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' = fThis 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 |