#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: 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 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