Pure variables as patterns are disallowed. Patterns have a distinct
type from expressions so allowing an expression to be substituted
causes complications. In particular we want to know statically how
many targets a goal has, which is not possible if a variable can be
substituted here.