[GHC] #9456: Weird behavior with polymorphic function involving existential quantification and GADTs
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Operating System: Keywords: | Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: GHC Difficulty: Unknown | rejects valid program Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- This program is rejected by GHC 7.8.2: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} With the following type error: {{{ foo.hs:15:11: Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for g :: a -> a at foo.hs:14:12-17 Expected type: a -> a Actual type: a0 -> a0 Relevant bindings include g :: a -> a (bound at foo.hs:15:7) f :: a0 -> a0 (bound at foo.hs:10:7) In the expression: f In an equation for ‘g’: g = f }}} Perplexingly, however, you can get it to compile either by adding a type signature to f: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f :: x -> x f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} Or by disabling the GADTs extension: {{{ {-# LANGUAGE ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} Or by getting rid of the asTypeOf: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f x = let _ = Box x in x g :: a -> a g = f return () }}} Or by defining ‘box’ differently: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do let box = Box () let f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} And perhaps some other factors that I haven't tested yet. It appears to me that all of these should be valid programs. Real world source: https://github.com/andygill/io- reactive/blob/master/Control/Concurrent/Reactive.hs It happens here due to the usage of (putMVar box ret), which makes the function requestit in line 77 not as polymorphic as it should be, unless you add a type signature. The putMVar serves the same role as the `asTypeOf` in my smaller example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Description changed by haasn: Old description:
This program is rejected by GHC 7.8.2:
{{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do box <- return (Box ())
let f x = let _ = Box x `asTypeOf` box in x
g :: a -> a g = f
return () }}}
With the following type error:
{{{ foo.hs:15:11: Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for g :: a -> a at foo.hs:14:12-17 Expected type: a -> a Actual type: a0 -> a0 Relevant bindings include g :: a -> a (bound at foo.hs:15:7) f :: a0 -> a0 (bound at foo.hs:10:7) In the expression: f In an equation for ‘g’: g = f }}}
Perplexingly, however, you can get it to compile either by adding a type signature to f:
{{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do box <- return (Box ())
let f :: x -> x f x = let _ = Box x `asTypeOf` box in x
g :: a -> a g = f
return () }}}
Or by disabling the GADTs extension:
{{{ {-# LANGUAGE ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do box <- return (Box ())
let f x = let _ = Box x `asTypeOf` box in x
g :: a -> a g = f
return () }}}
Or by getting rid of the asTypeOf:
{{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do box <- return (Box ())
let f x = let _ = Box x in x
g :: a -> a g = f
return () }}}
Or by defining ‘box’ differently:
{{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do let box = Box ()
let f x = let _ = Box x `asTypeOf` box in x
g :: a -> a g = f
return () }}}
And perhaps some other factors that I haven't tested yet.
It appears to me that all of these should be valid programs.
Real world source: https://github.com/andygill/io- reactive/blob/master/Control/Concurrent/Reactive.hs
It happens here due to the usage of (putMVar box ret), which makes the function requestit in line 77 not as polymorphic as it should be, unless you add a type signature. The putMVar serves the same role as the `asTypeOf` in my smaller example.
New description: This program is rejected by GHC 7.8.2: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} With the following type error: {{{ foo.hs:15:11: Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for g :: a -> a at foo.hs:14:12-17 Expected type: a -> a Actual type: a0 -> a0 Relevant bindings include g :: a -> a (bound at foo.hs:15:7) f :: a0 -> a0 (bound at foo.hs:10:7) In the expression: f In an equation for ‘g’: g = f }}} Perplexingly, however, you can get it to compile either by adding a type signature to f: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f :: x -> x f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} Or by disabling the GADTs extension: {{{ {-# LANGUAGE ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} Or by getting rid of the asTypeOf: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f x = let _ = Box x in x g :: a -> a g = f return () }}} Or by defining ‘box’ differently: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do let box = Box () let f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} And perhaps some other factors that I haven't tested yet. It appears to me that all of these should be valid programs. Real world source: https://github.com/andygill/io- reactive/blob/master/Control/Concurrent/Reactive.hs It happens here due to the usage of “writeChan chan $ Done ret”, which makes the function requestit in line 77 not as polymorphic as it should be, unless you add a type signature. The putMVar serves the same role as the `asTypeOf` in my smaller example. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Description changed by haasn: Old description:
This program is rejected by GHC 7.8.2:
{{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do box <- return (Box ())
let f x = let _ = Box x `asTypeOf` box in x
g :: a -> a g = f
return () }}}
With the following type error:
{{{ foo.hs:15:11: Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for g :: a -> a at foo.hs:14:12-17 Expected type: a -> a Actual type: a0 -> a0 Relevant bindings include g :: a -> a (bound at foo.hs:15:7) f :: a0 -> a0 (bound at foo.hs:10:7) In the expression: f In an equation for ‘g’: g = f }}}
Perplexingly, however, you can get it to compile either by adding a type signature to f:
{{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do box <- return (Box ())
let f :: x -> x f x = let _ = Box x `asTypeOf` box in x
g :: a -> a g = f
return () }}}
Or by disabling the GADTs extension:
{{{ {-# LANGUAGE ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do box <- return (Box ())
let f x = let _ = Box x `asTypeOf` box in x
g :: a -> a g = f
return () }}}
Or by getting rid of the asTypeOf:
{{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do box <- return (Box ())
let f x = let _ = Box x in x
g :: a -> a g = f
return () }}}
Or by defining ‘box’ differently:
{{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where
data Box = forall a. Box a
foo :: Monad m => m () foo = do let box = Box ()
let f x = let _ = Box x `asTypeOf` box in x
g :: a -> a g = f
return () }}}
And perhaps some other factors that I haven't tested yet.
It appears to me that all of these should be valid programs.
Real world source: https://github.com/andygill/io- reactive/blob/master/Control/Concurrent/Reactive.hs
It happens here due to the usage of “writeChan chan $ Done ret”, which makes the function requestit in line 77 not as polymorphic as it should be, unless you add a type signature. The putMVar serves the same role as the `asTypeOf` in my smaller example.
New description: This program is rejected by GHC 7.8.2: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} With the following type error: {{{ foo.hs:15:11: Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for g :: a -> a at foo.hs:14:12-17 Expected type: a -> a Actual type: a0 -> a0 Relevant bindings include g :: a -> a (bound at foo.hs:15:7) f :: a0 -> a0 (bound at foo.hs:10:7) In the expression: f In an equation for ‘g’: g = f }}} Perplexingly, however, you can get it to compile either by adding a type signature to f: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f :: x -> x f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} Or by disabling the GADTs extension: {{{ {-# LANGUAGE ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} Or by getting rid of the asTypeOf: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do box <- return (Box ()) let f x = let _ = Box x in x g :: a -> a g = f return () }}} Or by defining ‘box’ differently: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Foo where data Box = forall a. Box a foo :: Monad m => m () foo = do let box = Box () let f x = let _ = Box x `asTypeOf` box in x g :: a -> a g = f return () }}} And perhaps some other factors that I haven't tested yet. It appears to me that all of these should be valid programs. Real world source: https://github.com/andygill/io- reactive/blob/master/Control/Concurrent/Reactive.hs It happens here due to the usage of “writeChan chan $ Req fun ret”, which makes the function requestit in line 77 not as polymorphic as it should be, unless you add a type signature. The putMVar serves the same role as the `asTypeOf` in my smaller example. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by bernalex): 7.8.3 rejects it as well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by rwbarton): This is all expected behavior—for some value of "expected"! See https://www.haskell.org/ghc/docs/latest/html/users_guide/other-type- extensions.html#mono-local-binds. Your original program does not typecheck because - the `GADTs` language flag implies `MonoLocalBinds` - `f` does not have a user-supplied type signature - `f` cannot be floated to top-level because it refers to `box`, and... - `box` cannot be floated to top-level either because it is not bound by a `let` and therefore the type of `f` is not generalized, and so it cannot be used polymorphically by `g`. Your four other programs each differ in one of these four features. Granted, this is all not very obvious; do you have any suggestion for a better error message? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by haasn): It would be great if the error message could somehow mention that this type signature was less polymorphic than it could be, and that perhaps the user wants to add NoMonoLocalBinds or an explicit type signature. Is that a case that can be detected? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by rwbarton): (I noticed the GADTs section of the User's Guide was out of date regarding the flags turned on by `-XGADTs`, fixed in b287bc9bd0afaa26fcd3fe53a49bf86deeb868d8.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Reid is, as ever, spot on. I think it might not be hard for the error message to say {{{ foo.hs:15:11: Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for g :: a -> a at foo.hs:14:12-17 Expected type: a -> a Actual type: a0 -> a0 Relevant bindings include g :: a -> a (bound at foo.hs:15:7) f :: a0 -> a0 (bound at foo.hs:10:7) NB: let-bound f is monomorphic because of MonoLocalBinds <------------ In the expression: f In an equation for ‘g’: g = f }}} That is, annotate the "relevant bindings" that we did not attempt to generalise. It would be much harder to annotate only bindings that ''would'' generalise, but didn't. For example {{{ foo v = do let f x = v g :: a -> a g = f }}} Here `f` can't be generalised regardless of `MonoLocalBinds` because it mentions `v`. The other difficulty is that adding `-XNoMonoLocalBinds` if you have `-XGADTs` is extremely dodgy. (It should probably elicit a stern warning, although it does not at the moment.) So implicitly encouraging people to switch it off rather than fix the program properly is a bad idea. Perhaps the message should say: {{{ NB: Let-bound f was not generalised Possible solution: give it a type signature }}} Users, what do you think. Check out the [http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type- extensions.html#typing-binds user manual section] (7.13.9.3). Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by haasn): My greatest concern with manually applying type signatures is that, as seen in my real world use case, adding an explicit type signature would require changing more than just that function, due to ScopedTypeVariables being needed. But, barring some way to tell GHC to explicitly “generalize (just) this function”, and assuming that adding -XNoMonoLocalBinds when it would otherwise be implied is a Bad Thing, then I'd be content with the user just being told to generalize manually. I do think adding a big fat warning label about something not generalizing is important, because I personally did not even know this restriction existed - and I would not have guessed adding a type signature fixes anything because I was operating under the impression that GHC already infers the most general rank-1 type for things that are not on the top level. I believe a false positive for things that could not generalize either way is an acceptable trade-off, as long as the message is not *too* obnoxious. In this particular case, I believe a good error message could also mention the fact that the type variable ‘a0’ is forced to be monomorphic, which is ultimately why ‘a’ can't be matched with ‘a0’ (which seems counter- intuitive given just the first line of the error message), but perhaps mentioning that the binding for ‘f :: a0 -> a0’ is monomorphic would suffice. Up to you. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9456: Weird behavior with polymorphic function involving existential quantification and GADTs -------------------------------------+------------------------------------- Reporter: haasn | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: GADTs, Resolution: | TypeErrorMessages Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: GADTs => GADTs, TypeErrorMessages -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9456#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC