I saw the same problem with fscheck's implication operator (I work with Galen, who reported this problem to you). I was trying to do a similar thing for a slightly different purpose.

Howard

Hiser, I admit that explicit laziness is too verbose in some cases, especially when implementing the implication operator discussed above. As for your example - well, nothing can really go bad in such a simple case. Frankly speaking, this expression is subject to compile-time optimization yielding a constant value (I don't know whether F# currently performs such optimisations).
But in general it would be impossible for a compiler to distinguish between "safe" and "unsafe" expressions where "safety" means side effects independence. Even extending the language with an additional entity such as "pure" functions would not help much because F# targets .NET framework which has been designed without functional languages in mind.

So the language designer has to decide whether to allow implicit lazy value coercion in all cases or not.
Laziness itself is a nice programming technique making a programming language more expressive. And F# does not tend to be as side-effects intolerant as Haskell which makes it much more suitable for practical programming. But the combination of laziness and side effects may be quite confusing especially when it goes beyond several simple functions. Avoiding potentially unsafe constructs could be a matter of convention but the compiler cannot make any guarantees. Of course, making laziness explicit does not guarantee that everything is correct but it does really help to keep the side effects in mind when you have to deal with them.
Moreover, implicit type conversion (note that 'a and 'a lazy are different types) is not the "F# way" and it is contrary to the language design. I'm not quite sure but I guess it might break the type inference system.

Implementing logical operators is one of the cases where explicit laziness is very annoying and eager evaluation semantics is undesirable. A common practice is to make boolean operators lazy by the compiler itself. For example, in C++ boolean `or` operator (||) does not evaluate its second argument if the first one is true. But if you define the same operator for your own data type it will always evaluate both arguments. So does F#. Examining the generated IL code shows that these operators are actually implemented by code expansion rather than a separate function so that 'a || b' expression is translated into 'if a then true else b'. That leads to one more reason to avoid laziness when implementing the discussed implication operator: in F# laziness adds a significant performance penalty in comparison with a simple function call. And that's not suitable for simple functions because dealing with lazy value (actually a discriminated union type) would take much more time than the function logic itself. I think that the only solution could be some code generation technique like lisp-style macros. The F# manual says that inline functions are implemented by code expansion but this does not result in simple code substitution - otherwise function semantics might be different depending on the inlining and that could be very confusing (just imagine different behaviour of debug and release builds).
So I think we currently can't expect some nice and easy way to deal seamlessly with laziness.