[GHC] #12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables)

5 May 2016


      #12018: Equality constraint not available in pattern type signature
(GADTs/ScopedTypeVariables)
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  bug            |            Status:  new
           Priority:  lowest         |         Milestone:
          Component:  Compiler       |           Version:  7.10.3
  (Type checker)                     |
           Keywords:  GADTs,         |  Operating System:  Unknown/Multiple
  ScopedTypeVariables                |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 data Exp a where
   Tru :: Ty Bool

 eval :: Exp a -> a
 eval Tru = True
 }}}

 Works fine, as does

 {{{#!hs
 eval :: Exp a -> a
 eval (Tru :: Exp _) = True
 }}}

 But

 {{{#!hs
 eval :: Exp a -> a
 eval (Tru :: Exp Bool) = True
 }}}

 doesn't, is this an intended design of GADTs/ScopedTypeVariables that the
 type equality constraint isn't in scope in the type signature of the
 pattern match, I would like to match on an existential type in my own
 code:

 {{{#!hs
 compile (ArrIx arr index :: Exp (Sca elt)) = do
   ...
 }}}

 It can be worked around by writing:

 {{{#!hs
 eval a@Tru =
   case a :: Exp Bool of
 }}}

 but for my own code it seems I must write

 {{{#!hs
 compile uuu@(ArrIx arr index :: Exp a) = do
   case uuu :: (a ~ Sca elt) => Exp (Sca elt) of
 }}}

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