[GHC] #6075: Incorrect interpretation of scoped type variable declaration in GADT pattern match

[GHC]

#6075: Incorrect interpretation of scoped type variable declaration in GADT
pattern match
-------------------------------+--------------------------------------------
  Reporter:  goldfire          |          Owner:                           
      Type:  bug               |         Status:  closed                   
  Priority:  normal            |      Milestone:                           
 Component:  Compiler          |        Version:  7.5                      
Resolution:  invalid           |       Keywords:  ScopedTypeVariables GADTs
        Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple         
   Failure:  None/Unknown      |     Difficulty:  Unknown                  
  Testcase:                    |      Blockedby:                           
  Blocking:                    |        Related:                           
-------------------------------+--------------------------------------------
Changes (by simonpj):

  * status:  new => closed
  * difficulty:  => Unknown
  * resolution:  => invalid


Comment:

 The errror mesage (with GHC 7.4) is this:
 {{{
 T6075.hs:27:3:
     Couldn't match type `a -> b' with `Int'
     Inaccessible code in
       a pattern with constructor GInt :: GADT Int, in a case alternative
     In the pattern: GInt
     In a case alternative: GInt -> show (create :: Int)
 }}}
 And that seems right to me.  Consider the
 [http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.17
 semantics of pattern matching in the Haskell report].  To 3.17.2 add the
 informal rule
  * Matching the pattern `(p :: ty)` against a value `v` requires `v` to
 have type `ty` (or else a static error results), and then matches `p`
 against `v`.

 To 3.17.3 add a rule for type signatures
 {{{
 case v of { (p :: type) -> e1; _ -> e2 }
  =
 case (v :: type) of { p -> e1; _ -> e2 }
 }}}
 (This rule does not take account of bringing lexical type variables into
 scope, but is otherwise right.)

 In short, patterns are matched outside in, so we don't get to see that the
 pattern has type `GADT (a->b)` until ''after'' we've matched `GArrow`, but
 the type signature applies ''before''.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6075#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler