Basic type-checking for predicate use, pred/fun syntax location use site fix

[tnelson]

This PR adds basic typechecking for pred use. E.g.,

sig A { f1: lone B }
sig B { f2: lone A } 
pred p1[a: A] {
    p2[a] // mistake: meant to write a.f1
}
pred p2[b: B] { some b.f2 }

test expect { should_error: {some x: A | p1[x]} is sat }

This will produce an error saying that p2 was applied incorrectly, with blame location at the a. (Note that DrRacket will not report the blame location properly; it is given in the error message, and will be picked up in VSCode.)

This PR also fixes the use-site source location recording for:

• pred uses
• fun uses
• quantifier variables.