Are rules permitted in requires/instantiation?

[boyland]

The syntax permits rules on non-abstract judgments in the requires part of an abstract module, But doing so apparently makes the module non-instantiable. For example:

module set
requires
  
  abstract syntax e
  judgment elem-equal: e = e

  -------- eleme
  e = e
  
  // ...

This syntax is accepted, but if one instantiates the module, say:

module natset = set[n, Nat.equal, ... ]

then one gets the confusing error attached to the whole instantiation

A module argument must be a syntax, judgment, rule, or theorem, but an undefined identifier was provided.

Apparently a rule is not a ModuleComponent contra the message that seems to say that rules are OK. But the error makes me think that rule instantiation was not adequately tested. So I am loathe to just have Rule implement ModuleComponent without more care as to what it means to be a ModuleComponent.

It also brings up the overall point that perhaps it doesn't make sense for the instantiation to have to provide actual value for non-abstract "requires" components. As mentioned in issue #135, if we decided against having actuals for non-abstract requires, this will be a breaking change and must be implemented before 1.6.0 is released.