[GHC] #10443: Regression in forall typechecking
#10443: Regression in forall typechecking -------------------------------------+------------------------------------- Reporter: alanz | Owner: Type: bug | Status: new Priority: high | Milestone: 7.10.2 Component: Compiler | Version: 7.10.1 (Type checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: | valid program Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- 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 {{{#!hs 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 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10443> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#10443: Regression in forall typechecking -------------------------------------+------------------------------------- Reporter: alanz | Owner: Type: bug | Status: new Priority: high | Milestone: 7.10.2 Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by alanz): Oops, steps to show up the problem, once the relevant version of GHC is built {{{ git clone https://github.com/DanielG/ghc-mod.git cd ghc-mod git checkout b52c0a5d767282369f2748c5ec070b802ed8e23c cabal install }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10443#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#10443: Regression in forall typechecking -------------------------------------+------------------------------------- Reporter: alanz | Owner: simonpj Type: bug | Status: new Priority: highest | Milestone: 7.10.2 Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Changes (by hvr): * owner: => simonpj * priority: high => highest Comment: Simon, could you give this one a quick glance for triaging? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10443#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#10443: Regression in forall typechecking -------------------------------------+------------------------------------- Reporter: alanz | Owner: simonpj Type: bug | Status: new Priority: highest | Milestone: 7.10.2 Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by alanz): I've just noticed that line 294 {{{#!haskell deriving instance Generic Version }}} in `Language.Haskell.GhcMod.Types` needs to be commented out too. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10443#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#10443: Regression in forall typechecking -------------------------------------+------------------------------------- Reporter: alanz | Owner: simonpj Type: bug | Status: closed Priority: highest | Milestone: 7.10.2 Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: invalid | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment: 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 Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10443#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#10443: Regression in forall typechecking -------------------------------------+------------------------------------- Reporter: alanz | Owner: simonpj Type: bug | Status: closed Priority: highest | Milestone: 7.10.2 Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: invalid | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10443#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#10443: Regression in forall typechecking -------------------------------------+------------------------------------- Reporter: alanz | Owner: simonpj Type: bug | Status: closed Priority: highest | Milestone: 7.10.2 Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: invalid | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, it's a change in behaviour from 7.10.1 to 7.10.2; but of course all bug-fixes are! Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10443#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC