(3 :: Int) == $$(...)

may typecheck when

$$(...) == (3 :: Int)

does not. I don't imagine this problem can be solved in general, but I'm rather curious whether it might be possible to solve for "pure" splices, with types that look like

forall m. Quote m => Code m a

Would it be possible to get full bidirectional inference for these if they were somehow marked specially by the user? For instance, if I wrote

$$$e

that could mean e should be interpreted as having some type

PCode a

where

newtype PCode a = PCode (forall m. Quote m => a)