Skip to content

Rank-n typechecking regression between GHC 8.4 and 8.6

The following program typechecks on GHC 7.0.4 through 8.4.4:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where

f    :: (forall a. a -> forall b. b -> c) -> ()
f (_ ::  forall a. a -> forall b. b -> c)  = ()

However, it does not typecheck on GHC 8.6.3:

$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:7:4: error:
    • Couldn't match type ‘b0 -> c1’ with ‘forall b. b -> c’
      Expected type: a -> forall b. b -> c
        Actual type: a -> b0 -> c1
    • When checking that the pattern signature:
          forall a. a -> forall b. b -> c
        fits the type of its context: forall a. a -> forall b. b -> c1
      In the pattern: _ :: forall a. a -> forall b. b -> c
      In an equation for ‘f’:
          f (_ :: forall a. a -> forall b. b -> c) = ()
    • Relevant bindings include
        f :: (forall a. a -> forall b. b -> c1) -> () (bound at Bug.hs:7:1)
  |
7 | f (_ ::  forall a. a -> forall b. b -> c)  = ()
  |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Edited by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information