[GHC] #9420: Impredicative type instantiation without -XImpredicativeTypes
#9420: Impredicative type instantiation without -XImpredicativeTypes -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Consider this module: {{{ {-# LANGUAGE RankNTypes #-} module Bug where rank2 :: ((forall a. a -> a) -> b) -> () rank2 _ = () foo :: () -> () foo x = x quux :: (forall a. a -> a) -> Int quux _ = 5 bar = foo . rank2 $ quux }}} The `(.)` in the definition of `bar` requires an impredicative instantiation -- that is, one of its type variables is instantiated to a forall-type. Yet, the module compiles without `-XImpredicativeTypes`. To confirm this behavior, the following is an excerpt from `-ddump-simpl`: {{{ Bug.bar = break<7>() (break<6>() GHC.Base.. @ () @ () @ ((forall a_a1Tj. a_a1Tj -> a_a1Tj) -> GHC.Types.Int) Bug.foo (Bug.rank2 @ GHC.Types.Int)) Bug.quux }}} Note the third type argument to `(.)`. Fixing this would be a breaking change that could affect users. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9420 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9420: Impredicative type instantiation without -XImpredicativeTypes -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): See also #4347, #4295, #7264, #8808, #9420 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9420#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9420: Impredicative type instantiation without -XImpredicativeTypes -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.9 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thomie): * component: Compiler => Compiler (Type checker) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9420#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9420: Impredicative type instantiation without -XImpredicativeTypes -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.9 checker) | Keywords: Resolution: | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => ImpredicativeTypes -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9420#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9420: Impredicative type instantiation without -XImpredicativeTypes -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.9 checker) | Keywords: Resolution: fixed | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11319 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => fixed * related: => #11319 Comment: This has been fixed since GHC 8.0.1, since GHC now does properly detect the impredicative instantiation: {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug2.hs, interpreted ) Bug2.hs:14:13: error: • Cannot instantiate unification variable ‘a0’ with a type involving foralls: (forall a. a -> a) -> b0 GHC doesn't yet support impredicative polymorphism • In the second argument of ‘(.)’, namely ‘rank2’ In the expression: foo . rank2 In the expression: foo . rank2 $ quux | 14 | bar = foo . rank2 $ quux | ^^^^^ Bug2.hs:14:21: error: • Cannot instantiate unification variable ‘a0’ with a type involving foralls: (forall a. a -> a) -> Int GHC doesn't yet support impredicative polymorphism • In the second argument of ‘($)’, namely ‘quux’ In the expression: foo . rank2 $ quux In an equation for ‘bar’: bar = foo . rank2 $ quux | 14 | bar = foo . rank2 $ quux | ^^^^ }}} (See also #11319 for the plan to allow such impredicative instantiations via `TypeApplications`.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9420#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC