[GHC] #10644: Option GADTs invalidates a rank-2 function.

#10644: Option GADTs invalidates a rank-2 function. -------------------------------------+------------------------------------- Reporter: bales | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Keywords: | Operating System: Linux Architecture: x86_64 | Type of failure: GHC rejects (amd64) | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- This module typechecks WITHOUT the extension GADTs and doesn't typecheck WITH the extension GADTs Since it has nothing to do with GADTs, the consequence of using the option is surprising. I witnessed this behaviour on GHC versions 7.6.3, 7.8.3, 7.8.4, 7.10.1 {{{#!hs {-# LANGUAGE RankNTypes , GADTs #-} module GADTMonomorphism where problem :: (forall x . () -> x) -> (a,b) problem f = (p, p) where p = f () }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10644 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10644: Option GADTs specialises a polymorphic value in local bindings -------------------------------------+------------------------------------- Reporter: bales | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10644#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10644: Option GADTs specialises a polymorphic value in local bindings -------------------------------------+------------------------------------- Reporter: bales | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Resolution: invalid | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment: This is just a consequence of `MonoLocalBinds`, as specified in [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/other- type-extensions.html#mono-local-binds 7.13.9.3 of the user manual]. GADTs switches on `MonoLocalBinds`, so the definition of `p` is not generalised, and that in turn leads to the error you encountered. You might reasonably think that GADTs have nothing do to with generalisation, but alas they do, as the papers mentioned in the manual describe. I'm not saying it's brilliant behaviour, just that I don't know how to do better. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10644#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC