[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 (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