[GHC] #9456: Weird behavior with polymorphic function involving existential quantification and GADTs

[GHC]

#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