#16033: Rank-n typechecking regression between GHC 8.4 and 8.6 -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.6.3 checker) | Resolution: | Keywords: RankNTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by RyanGlScott: Old description:

The following program typechecks on GHC 7.0.4 through 8.4.4:

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

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

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 -> c’ with ‘forall b. b -> z’ Expected type: a -> forall b. b -> z Actual type: a -> b0 -> c • When checking that the pattern signature: forall a. a -> forall b. b -> z fits the type of its context: forall a. a -> forall b. b -> c In the pattern: _ :: forall a. a -> forall b. b -> z In an equation for ‘f’: f (_ :: forall a. a -> forall b. b -> z) = () • Relevant bindings include f :: (forall a. a -> forall b. b -> c) -> () (bound at Bug.hs:7:1) | 7 | f (_ :: forall a. a -> forall b. b -> z) = () | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}}

New description: The following program typechecks on GHC 7.0.4 through 8.4.4: {{{#!hs {-# 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) = () | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16033#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16033: Rank-n typechecking regression between GHC 8.4 and 8.6 -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.6.3 checker) | Resolution: | Keywords: RankNTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): This bug also affects rank-//n// //contexts// as well, as the following typechecks in GHC 8.4.4 and earlier, but not in GHC 8.6.3: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} module Bug where f :: (forall a. a -> Show a => c) -> () f (x :: forall a. a -> Show a => c) = () }}} {{{ $ /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 ‘c1’ with ‘Show a => c’ ‘c1’ is a rigid type variable bound by the type signature for: f :: forall c1. (forall a. a -> Show a => c1) -> () at Bug.hs:6:1-42 Expected type: a -> Show a => c Actual type: a -> c1 • When checking that the pattern signature: forall a. a -> Show a => c fits the type of its context: forall a. a -> Show a => c1 In the pattern: x :: forall a. a -> Show a => c In an equation for ‘f’: f (x :: forall a. a -> Show a => c) = () • Relevant bindings include f :: (forall a. a -> Show a => c1) -> () (bound at Bug.hs:7:1) | 7 | f (x :: forall a. a -> Show a => c) = () | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16033#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16033: Rank-n typechecking regression between GHC 8.4 and 8.6 -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.6.3 checker) | Resolution: fixed | Keywords: RankNTypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T16033 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => typecheck/should_compile/T16033 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16033#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler