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 |