Currently, an expression which isn't used is discarded as dead code, even though it includes an unsafePerformIO action like Debug.Trace. While this behavior is understandable, this caveat should at least be documented.

Steps to Reproduce

Build and run the following program:

import Debug.Trace

seq : a -> b -> b
seq x y = y

main : IO ()
main = let f = trace "STEP-ONE" () in
       putStrLn $ f `seq` trace "STEP-TWO" "STEP-THREE"

Expected Behavior

As there's no documentation to the contrary, I'd assume all the code would be executed because of Idris' eager evaluation order.

STEP-ONE
STEP-TWO
STEP-THREE

Observed Behavior

I instead get:

STEP-TWO
STEP-THREE

However, if I change the program to the following:

import Debug.Trace

%noinline
seq : a -> b -> b
seq x y = y

main : IO ()
main = let f = trace "STEP-ONE" () in
       putStrLn $ f `seq` trace "STEP-TWO" "STEP-THREE"

I get the answer I would normally expect. I've tried this out on both the Node and Racket backends, and with other unsafe actions like idris_crash.

I think, observed behavior is expected documented behaviour since let x = val in e is documented to be equivalent to (\x => e) val, and on your case this completely eliminates the whole expression of val. It does not matter whether it contains unsafePerformIO or not, the fact that this expression is not computed fully corresponds the language semantics.

this completely eliminates the whole expression of val

Why is that the case? I understand the let binding can be transformed to a lambda-expression, but under traditional eager evaluation semantics, a lambda expression should still fully evaluate its arguments before its body can be run, even when the body doesn't use the arguments. Whether it uses a let binding or a lambda expression shouldn't matter.

under traditional eager evaluation semantics, a lambda expression should still fully evaluate its arguments

Well, that's interesting. I always thought that only functions fully evaluate their arguments, not arbitrary lambda expressions. I always thought that the meaning of a lambda expression is its normal form, and thus applying a lambda expression to an unused argument literally means non-presence of that argument. But maybe I'm wrong in my thoughts, despite I still think my concept is sound.

only functions fully evaluate their arguments, not arbitrary lambda expressions.

The order of argument evaluation in an application should be (observationally) the same for any (eager) expression in the function position. The underlying implementation may use different strategies for different kinds of function expressions, but they should always look the same to the user (for example, always performs the same side effects).