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.

Trac metadata

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