[GHC] #12883: Unexpected constraint when using ExistentialQuantification

[GHC]

#12883: Unexpected constraint when using ExistentialQuantification
-------------------------------------+-------------------------------------
           Reporter:  danilo2        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Hello!
 Consider this simple code:

 {{{
 data Elem t = Typeable t => Elem Int

 tst1 :: forall a. Elem a -> TypeRep
 tst1 (Elem _) = typeRep (Proxy :: Proxy a)

 }}}

 It works and it should work. `Elem` is created only to be sure that if
 we've got a value of type `Elem t` we don't have to check that `t` is
 `Typeable`. <offtopic> By the way, exystential newtypes would be so
 awesome in GHC! </offtopic>

 And now a strange thing. If we create another function:

 {{{
 tst2 :: forall a. Elem a -> TypeRep
 tst2 _ = typeRep (Proxy :: Proxy a)
 }}}

 GHC throws error that there is no `Typeable a` constraint. The only
 difference between `tst1` and `tst2` is different pattern binding.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12883>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler