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 = TrueBut 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 |