[GHC] #7156: "Pattern match on GADT" error for non-GADT

[GHC]

#7156: "Pattern match on GADT" error for non-GADT
---------------------------------------------------------------+------------
    Reporter:  ryani                                           |       Owner:                  
        Type:  bug                                             |      Status:  new             
    Priority:  normal                                          |   Milestone:                  
   Component:  Compiler (Type checker)                         |     Version:  7.0.4           
    Keywords:  GADTs, TypeFamilies, ExistentialQuantification  |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple                                |     Failure:  None/Unknown    
  Difficulty:  Unknown                                         |    Testcase:                  
   Blockedby:                                                  |    Blocking:                  
     Related:                                                  |  
---------------------------------------------------------------+------------

Comment(by ryani):

 I expect that if you can define a data type with particular extensions,
 you should be able to pattern match on that data type successfully.  Or
 else, what's the point of defining it?  This is a failure in a single
 module, not two modules defined with different extensions, which surprised
 me!

 There extensions being used here, EqualityConstraints (via TypeFamilies)
 and ExistentialQuantification, are well known to be equivalent in power to
 GADTs in defining types.  But, I guess there is extra type system
 machinery to deal with the {{{ T a -> a }}} vs {{{ T a -> () }}} problem
 that is currently only enabled with GADTs?

 It seems like equality constraints require that same machinery; at least
 if they are able to be brought into scope via pattern matching.

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