Weird behavior with polymorphic function involving existential quantification and GADTs

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.

changed weight to 5

added Tbug Trac import typechecker labels

changed the description

1. 8.3 rejects it as well.

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?

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?

(I noticed the GADTs section of the User's Guide was out of date regarding the flags turned on by -XGADTs, fixed in b287bc9b.)

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 user manual section (7.13.9.3).

Simon

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.

Trac metadata

Trac field	Value
TypeOfFailure	ValidProgramRejected → IncorrectWarning

added GADTs label

added error messages label and removed GADTs label

added Pnormal label