Refinement bound as var exposes compiler internals

[zackbach]

var foo = is-empty

l :: List%(foo) = [list:]

Running this program gives the following error, which exposes compiler internals.

Either vars in refinements should be disallowed as a well-formedness check (since the semantics would probably be confusing otherwise), or they should be properly supported. I prefer the former.