That’s a cool paper! I guess you could even make it safe if you make the EBool type opaque and only expose functions to construct it. Pattern matching on EBool would lead to exotic terms, which break the compilation. That does seem more straightforward than PHOAS which is usually my go to approach to make HOAS safe.
Ah, I feel like you might be able to do the same with an applicative interface. I have posted about that idea before:
I wish I had the time to really put that to the test. I really wonder if there is a gap between monad and applicative where arrows do add something. It feel a bit like P vs NP, but then Applicative vs Arrow.