#3483: Some mechanism for eliminating "absurd" patterns
-----------------------------+----------------------------------------------
Reporter: ryani | Owner:
Type: feature request | Status: new
Priority: normal | Component: Compiler
Version: 6.10.4 | Severity: normal
Keywords: | Testcase:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
-----------------------------+----------------------------------------------
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3483>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
