[GHC] #7888: Impredicativity flag needed more often
#7888: Impredicativity flag needed more often ----------------------------------------------+----------------------------- Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Component: Compiler (Type checker) Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: Incorrect warning at compile-time | Blockedby: Blocking: | Related: ----------------------------------------------+----------------------------- I don't know if this is a bug or a deliberate change, but HEAD requires -XImpredicativeTypes for this program while 7.6.3 does not. {{{ {-# LANGUAGE RankNTypes #-} f :: (forall a. a) -> b f = undefined }}} -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7888> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#7888: Impredicativity flag needed more often ----------------------------------------------+----------------------------- Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Component: Compiler (Type checker) Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: Incorrect warning at compile-time | Blockedby: Blocking: | Related: ----------------------------------------------+----------------------------- Comment(by simonpj@…): commit a18ea4f20b73e1b3ef5cda2389c713152eb9576e {{{ Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Wed May 15 09:51:25 2013 +0100 Make 'undefined' have the magical type 'forall (a:OpenKind).a' This fixes Trac #7888, where the user wanted to use 'undefined' in a context that needed ((forall a. a->a) -> Int). We allow OpenKind unification variables to be instantiate with polytypes (or unboxed types), hence the change. 'error' has always been like this; this change simply extends the special treatment to 'undefined'. It's still magical; you can't define your own wrapper for 'error' and get the same behaviour. Really just a convenience hack. compiler/coreSyn/MkCore.lhs | 48 ++++++++++++++++++++++++++++++++------- compiler/prelude/PrelNames.lhs | 5 ---- 2 files changed, 39 insertions(+), 14 deletions(-) }}} -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7888#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#7888: Impredicativity flag needed more often ------------------------------------------------+--------------------------- Reporter: monoidal | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: Incorrect warning at compile-time | Difficulty: Unknown Testcase: typecheck/should_compile/T7888 | Blockedby: Blocking: | Related: ------------------------------------------------+--------------------------- Changes (by simonpj): * status: new => closed * difficulty: => Unknown * resolution: => fixed * testcase: => typecheck/should_compile/T7888 Comment: There really is a reason for this. The elaborated definition would be {{{ f :: forall b. (forall a. a) -> b = /\b. undefined @((forall a. a) -> b) }}} So we need to instantiate `undefined` at a polytype, which isn't usually allowed. But it is for `error` and there's no reason not to allow `undefined` too. See the commit comments above. Both for `error` and `undefined`, it's a bit of a hack. Simon -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7888#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC