Opened 3 years ago

Closed 2 years ago

Last modified 2 years ago

#10443 closed bug (invalid)

Regression in forall typechecking

Reported by: alanz Owned by: simonpj
Priority: highest Milestone: 7.10.2
Component: Compiler (Type checker) Version: 7.10.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


The following bug showed up when trying to install ghc-mod against the current ghc-7.10 branch

Ths code below, from

instance (MonadBaseControl IO m) => MonadBaseControl IO (GhcModT m) where
    type StM (GhcModT m) a =
          StM (StateT GhcModState
                (ErrorT GhcModError
                  (JournalT GhcModLog
                    (ReaderT GhcModEnv m) ) ) ) a
    liftBaseWith f = GhcModT . liftBaseWith $ \runInBase ->
        f $ runInBase . unGhcModT

    restoreM = GhcModT . restoreM
    {-# INLINE liftBaseWith #-}
    {-# INLINE restoreM #-}

Which compiles fine with GHC 7.10.1 now has the error

    Couldn't match expected type ‘StateT
                                    (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))
                                  -> IO (StM m (Either GhcModError (a1, GhcModState), GhcModLog))’
                with actual type ‘forall a2.
                                    (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))
                                  -> IO
                                                (JournalT GhcModLog (ReaderT GhcModEnv m))))
    Relevant bindings include
      runInBase :: forall a.
                     (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))
                   -> IO
                              (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m))))
        (bound at Language/Haskell/GhcMod/Monad/Types.hs:345:48)
      f :: RunInBase (GhcModT m) IO -> IO a
        (bound at Language/Haskell/GhcMod/Monad/Types.hs:345:18)
      liftBaseWith :: (RunInBase (GhcModT m) IO -> IO a) -> GhcModT m a
        (bound at Language/Haskell/GhcMod/Monad/Types.hs:345:5)
    In the first argument of ‘(.)’, namely ‘runInBase’
    In the second argument of ‘($)’, namely ‘runInBase . unGhcModT’

A laborious git bisect tracked it down to

681d82c0d44f06f0b958b75778c30b0910df982b is the first bad commit
commit 681d82c0d44f06f0b958b75778c30b0910df982b
Author: Simon Peyton Jones <>
Date:   Tue Apr 7 14:45:04 2015 +0100

    Look inside synonyms for foralls when unifying
    This fixes Trac #10194
    (cherry picked from commit 553c5182156c5e4c15e3bd1c17c6d83a95a6c408)

:040000 040000 1f0e62661ed1c48a9cbfab72ca3e38bb9e501412 ef6786fdb952d3446121b27b56f6103533d52356 M	compiler
:040000 040000 d607f1bff94578b0677df9cba01371dad6b26a32 ac715cec4fd8d43a53ecee132eae2b4c0c65e31a M	testsuite

Change History (6)

comment:1 Changed 3 years ago by alanz

Oops, steps to show up the problem, once the relevant version of GHC is built

git clone
cd ghc-mod
git checkout b52c0a5d767282369f2748c5ec070b802ed8e23c
cabal install

comment:2 Changed 2 years ago by hvr

Owner: set to simonpj
Priority: highhighest

Simon, could you give this one a quick glance for triaging?

comment:3 Changed 2 years ago by alanz

I've just noticed that line 294

deriving instance Generic Version

in Language.Haskell.GhcMod.Types needs to be commented out too.

comment:4 Changed 2 years ago by simonpj

Resolution: invalid
Status: newclosed

OK I've looked at this. It's a bug that 7.8 accepts it. The offending code is

    liftBaseWith f = GhcModT . liftBaseWith $ \runInBase ->
        f $ runInBase . unGhcModT

Here is a self-contained smaller version

{-# LANGUAGE RankNTypes #-}
module Foo where

type RunInBase m = forall b. m b -> m b

lbw :: (RunInBase m -> m a) -> m a
lbw = error "urk"

foo1 f = (id . lbw) (\r -> r f)
foo2 f = id (lbw (\r -> r f))

Now foo2 is accepted by 7.10, but foo1 is not. Why is foo1 rejected?

  • Note that RunInBase is a polymorphic type.
  • So in foo2, in the application (lbw (\r -> r f)), GHC can look up the type of lbw, and propagate it into the argumet (\r -> r f). So r gets a polymorphic type, f :: RunInBase m.
  • But in foo1, the call doesn't look like (lbw arg); instead it looks like (id . lbw) arg. So the higher-rank propagation doesn't happen, and r gets a monotype, something like r :: t -> m a.
  • So in the end we get
        Couldn't match type ‘t -> m a’ with ‘RunInBase m’

You want proper impredicative polymorphism, and GHC doesn't have that.

There was a bug in GHC 7.8 that unpredictably allowed certain bits of impredicativity, but I fixed that.

You can fix ghc-mod by writing

    liftBaseWith f = GhcModT (liftBaseWith $ \runInBase ->
        f $ runInBase . unGhcModT)

So I clain that this is not a bug.

Yell if you disagree


comment:5 Changed 2 years ago by alanz

I agree with the reasoning, but this is a change from 7.10.1 to ghc-7.10 branch, i.e. 7.10.2

Does it make sense to put something in the release notes for 7.10.2 about this?

comment:6 Changed 2 years ago by simonpj

Yes, it's a change in behaviour from 7.10.1 to 7.10.2; but of course all bug-fixes are!


Note: See TracTickets for help on using tickets.