Thanks! So you are implying that `TCO :: Maybe TCE`?

I am trying to think of a situation where a functional language compiler does not have enough information at compile time, especially when effects are witnessed by types.