Some mechanism for eliminating "absurd" patterns

[ryani]

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, which is related in spirit if not in implementation.