#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: |
Description
The following bug showed up when trying to install ghc-mod against the current ghc-7.10 branch
Ths code below, from https://github.com/DanielG/ghc-mod/blob/b52c0a5d767282369f2748c5ec070b802ed8e23c/Language/Haskell/GhcMod/Monad/Types.hs#L346
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
Language/Haskell/GhcMod/Monad/Types.hs:346:13: Couldn't match expected type ‘StateT GhcModState (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m))) a1 -> IO (StM m (Either GhcModError (a1, GhcModState), GhcModLog))’ with actual type ‘forall a2. StateT GhcModState (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m))) a2 -> IO (StM (StateT GhcModState (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))) a2)’ Relevant bindings include runInBase :: forall a. StateT GhcModState (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m))) a -> IO (StM (StateT GhcModState (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))) a) (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 <simonpj@microsoft.com> 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
comment:2 Changed 3 years ago by
Owner: | set to simonpj |
---|---|
Priority: | high → highest |
Simon, could you give this one a quick glance for triaging?
comment:3 Changed 3 years ago by
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 3 years ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
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 oflbw
, and propagate it into the argumet(\r -> r f)
. Sor
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, andr
gets a monotype, something liker :: 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
Simon
comment:5 Changed 3 years ago by
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 3 years ago by
Yes, it's a change in behaviour from 7.10.1 to 7.10.2; but of course all bug-fixes are!
Simon
Oops, steps to show up the problem, once the relevant version of GHC is built