[GHC] #3651: GADT type checking too liberal

[GHC]

#3651: GADT type checking too liberal
----------------------------------+-----------------------------------------
Reporter:  MartijnVanSteenbergen  |          Owner:                         
    Type:  bug                    |         Status:  new                    
Priority:  normal                 |      Component:  Compiler (Type checker)
 Version:  6.10.4                 |       Severity:  normal                 
Keywords:                         |       Testcase:                         
      Os:  Unknown/Multiple       |   Architecture:  Unknown/Multiple       
----------------------------------+-----------------------------------------
 I would expect the following three functions to fail:

 {{{
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}

 module Unsafe where

 data Z a where
   U :: Z ()
   B :: Z Bool

 unsafe1 :: Z a -> Z a -> a
 unsafe1 B U = ()

 unsafe2 :: a ~ b => Z b -> Z a -> a
 unsafe2 B U = ()

 unsafe3 :: a ~ b => Z a -> Z b -> a
 unsafe3 B U = True
 }}}

 But they are all accepted. In unsafe1 it seems pattern matching on the
 second argument discards any information learned from pattern matching on
 the first, while in the other two functions it seems the equality
 constraints are not checked at all.

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