[GHC] #15050: ScopedTypeVariables could allow more programs

[GHC]

#15050: ScopedTypeVariables could allow more programs
-------------------------------------+-------------------------------------
           Reporter:  nomeata        |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider
 {{{
 data P a = P
 data T1 a where
   MkT1 :: forall a.              P a               -> T1 a
   MkT2 :: forall a.              P a               -> T1 (a,a)
   MkT3 :: forall a b. b ~ Int => P a -> P b        -> T1 a
   MkT4 :: forall a b.            P a -> P b        -> T1 a
   MkT5 :: forall a b c. b ~ c => P a -> P b -> P c -> T1 a
 }}}

 I can write this function
 {{{
 foo :: T1 (Int, Int) -> ()
 foo (MkT1 (P::P (Int,Int)))    = ()
 foo (MkT2 (P::P x))            = (() :: x ~ Int => ())
 foo (MkT3 P (P::P Int))        = ()
 foo (MkT4 P (P::P b))          = ()
 foo (MkT5 P (P::P b) (P::P b)) = ()
 }}}
 but this these two equations fail
 {{{
 foo (MkT1 (P::P (Int,x)))      = (() :: x ~ Int => ())
 foo (MkT1 (P::P x))            = (() :: x ~ (Int,Int) => ())
 }}}

 I am especially surprised by the second one, given that the very similar
 equation with `MkT2` works.

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