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