Some mechanism for eliminating "absurd" patterns
This is to help with type-level programming and doing dependent-like programming in Haskell.
data TEq :: * -> * -> * where TEq :: TEq a a -- This declaration fails to compile because bringing (Int ~ Bool) -- into scope on the RHS is unsound. broken :: TEq Int Bool -> Int broken TEq = 1 -- Proposal: -- "!" replaces "=" in function declaration to say "this pattern is absurd" proposal :: TEq Int Bool -> r proposal TEq ! -- If, for some reason the pattern match succeeds, -- (basically, someone broke type safety with unsafeCoerce) -- the result could be something like calling: -- error "absurd pattern at FILE:LINE"
I'm not sure that "!" works with Haskell's syntax, but it does call attention to the pattern.
The idea is that anywhere that putting "= some_rhs" would cause the compiler to fail because it can prove that the type environment is unsound in some fashion, you could use "!" to give a valid function definition.
The same extension would be used for case statements, of course.
See also #2006 (closed), which is related in spirit if not in implementation.