Pattern Match Success Changes Types

Consider the following function..

demo1 :: (a -> b) -> Either a c -> Either b c
demo1 f (Left  a) = Left (f a)
demo1 _ (Right c) = Right c

My first question is, can programmers safely assume that the compiler is
sufficiently smart to avoid duplicating the expression (Right c) in the
event that the second match above succeeds? One might reasonably hope
that the run time implementation of this function will simply return
the functions second argument in this case.

In general, is it a requirement that Haskell compilers implement an
optimisation which re-uses patterns on the left hand side which also
appear in expressions on the right hand side?

If not, shouldn't this optimisation be mandatory? The reason I suggest
that it should be is apparent when you look at my next example.
A prudent programmer might decide not to rely on this optimisation
and try to write something like this.. 

demo2 :: (a -> b) -> Either a c -> Either b c
demo2 f   (Left  a) = Left (f a)
demo2 _ x@(Right c) = x

Unfortunately the Type Checker rejects the above 'as pattern'.
Hugs 1.3 returns the following error:
*** Expression    : demo2
*** Declared type : (a -> b) -> Either a c -> Either b c
*** Inferred type : (a -> a) -> Either a b -> Either a b

I'm afraid I don't know what other Haskell implementations do, but I've
encountered this problem with every ML compiler I've tried.

This suggests that the Type Checkers used by most compilers are less
than ideal, in that they don't take account of the fact that a successful
match may change the type of an 'as pattern' variable or function argument.
Perhaps there is some fundamental theoretical reason why this can't be
done, but I certainly can't think of one.

So, what is recommended practice for programmers in this situation?

Should programmers use 'as patterns' (assuming the type checker will
allow them) or not?

Which Haskell compilers currently implement the optimisation I mentioned
above? All? Any? None?

'As patterns' look awfully messy and it would be nice to not to have to
use them, but will there be efficiency penalties to pay if they're not

If Haskell requires programmers to program defensively (as far as this
problem is concerned) then shouldn't the Type Checkers allow more
liberal use of 'as patterns'?

Adrian Hey

Post to "haskell": haskell@dcs.gla.ac.uk