I don't think any top-level Ids should have OtherCon [] unfoldings? If they do, can you give a repro case? OtherCon [] unfoldings usually mean "I know this variable is evaluated, but I don't know what its value is. E.g
data T = MkT !a !a
f (MkT x y) = ...
here x and y have OtherCon [] unfoldings. They are definitely not bottom!
You may want stronger invariants on the output of CorePrep than we have hitherto sought. Can you explain what they are? And why you want the output of CorePrep not CoreTidy?
Thanks
Simon