Reify and option effect interact in weird ways #4004
Description
When using reify with an effect with a simple option monad, there is a very weird behavior if there is a non-trivial wp. The option pattern matching returns an "incomplete patterns" error.
The smallest reproduction I could come up with is still quite long, sorry about that, but the key part is just at the end. Running reify with a trivial wp works fine, anything else fails.
It's very similar to these old reports #1743 #2085 that use the old effect system. However the same problem appears in the main repo in examples/layeredeffects/RunST.fst that uses indexed effect.
This was also discussed in zulip