GADT type checking too liberal

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.

Trac metadata

Trac field	Value
Version	6.10.4
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture