[GHC] #12557: Regression in type inference with RankNTypes
#12557: Regression in type inference with RankNTypes -------------------------------------+------------------------------------- Reporter: slindley | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | 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: -------------------------------------+------------------------------------- Consider the following code: {{{#!hs foo :: ((forall a.f a) -> f r) -> f r foo g = undefined }}} In GHC 7.10.3: {{{ *Main> :t \g -> foo g \g -> foo g :: ((forall a. f a) -> f r) -> f r }}} In GHC 8.0.1: {{{ *Main> :t \g -> foo g <interactive>:1:11: error: • Couldn't match expected type ‘(forall a. f a) -> f r’ with actual type ‘t’ ‘t’ is a rigid type variable bound by the inferred type of it :: t -> f r at <interactive>:1:1 • In the first argument of ‘foo’, namely ‘g’ In the expression: foo g In the expression: \ g -> foo g • Relevant bindings include g :: t (bound at <interactive>:1:2) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12557 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12557: Regression in type inference with ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: slindley | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | ImpredicativeTypes 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: | -------------------------------------+------------------------------------- Changes (by thomie): * keywords: => ImpredicativeTypes * priority: high => low @@ -4,0 +4,3 @@ + {-# LANGUAGE ImpredicativeTypes #-} + module Test where + New description: Consider the following code: {{{#!hs {-# LANGUAGE ImpredicativeTypes #-} module Test where foo :: ((forall a.f a) -> f r) -> f r foo g = undefined }}} In GHC 7.10.3: {{{ *Main> :t \g -> foo g \g -> foo g :: ((forall a. f a) -> f r) -> f r }}} In GHC 8.0.1: {{{ *Main> :t \g -> foo g <interactive>:1:11: error: • Couldn't match expected type ‘(forall a. f a) -> f r’ with actual type ‘t’ ‘t’ is a rigid type variable bound by the inferred type of it :: t -> f r at <interactive>:1:1 • In the first argument of ‘foo’, namely ‘g’ In the expression: foo g In the expression: \ g -> foo g • Relevant bindings include g :: t (bound at <interactive>:1:2) }}} -- Comment: Your example relies on `-XImpredicativeTypes`. Please note that this language extension is entirely [https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.... #impredicative-polymorphism unsupported]. That said, you can make you example work by running `:set -XImpredicativeTypes` on the GHCi prompt. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12557#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12557: Regression in type inference with ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: slindley | Owner: Type: bug | Status: closed Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: invalid | ImpredicativeTypes 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment: This is a bug in 7.10. Basically, a lambda-bound variable like `\g` above can never get a higher rank type (one involving a forall), unless there is an enclosing type signature so that it's clear ''at the binding site'' what its type should be. I don't know any way to fix this. Do not rely on `-XImpredicativeTypes`; it is an incomplete, inconsistent and generally broken feature that I should probably remove. I just don't know how to do a better job, sorry! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12557#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12557: Regression in type inference with RankNTypes -------------------------------------+------------------------------------- Reporter: slindley | Owner: Type: bug | Status: closed Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: invalid | ImpredicativeTypes 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: | -------------------------------------+------------------------------------- @@ -4,1 +4,1 @@ - {-# LANGUAGE ImpredicativeTypes #-} + {-# LANGUAGE RankNTypes #-} New description: Consider the following code: {{{#!hs {-# LANGUAGE RankNTypes #-} module Test where foo :: ((forall a.f a) -> f r) -> f r foo g = undefined }}} In GHC 7.10.3: {{{ *Main> :t \g -> foo g \g -> foo g :: ((forall a. f a) -> f r) -> f r }}} In GHC 8.0.1: {{{ *Main> :t \g -> foo g <interactive>:1:11: error: • Couldn't match expected type ‘(forall a. f a) -> f r’ with actual type ‘t’ ‘t’ is a rigid type variable bound by the inferred type of it :: t -> f r at <interactive>:1:1 • In the first argument of ‘foo’, namely ‘g’ In the expression: foo g In the expression: \ g -> foo g • Relevant bindings include g :: t (bound at <interactive>:1:2) }}} -- Comment (by slindley): My example doesn't require `-XImpredicativeTypes` only `-XRankNTypes`! As I understand it the 'bug' in 7.10 was that it did infer polymorphic types for lambda-bound variables even with `-XImpredicativeTypes` disabled. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12557#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12557: Regression in type inference with RankNTypes -------------------------------------+------------------------------------- Reporter: slindley | Owner: Type: bug | Status: closed Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: invalid | ImpredicativeTypes 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 slindley): It does look like there's a bug in the error message. The message I want to see here is that t must be monomorphic, not that it is rigid. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12557#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12557: Regression in type inference with RankNTypes -------------------------------------+------------------------------------- Reporter: slindley | Owner: Type: bug | Status: closed Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: invalid | ImpredicativeTypes 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 goldfire): Yes, that error message is unfortunate. But I agree with 8.0 that your code should be rejected. I have filed #12563 requesting an error message improvement. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12557#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC