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

18 Aug 2014

      #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