[Haskell-cafe] Signature for non-empty filter

[Henning Thielemann]

Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
   (filter (\x -> x==1 && x==2))
  will always compute an empty list. Using an appropriate signature for
the function it shall be rejected at compile time, because it is probably
a mistake - probably (filter (\x -> x==1 || x==2) xs) was meant. I assume
that the type must contain somehow an example input for which the function
value is non-trivial. If Haskell's type system is not strong enough, what
about dependently typed languages like Cayenne or Epigram? (I know,
theorem provers have no problem with such types.)