Polarity-pragma-for-module-parameter.agda:5,14-15
The following names are not declared in the same scope as their
polarity pragmas (they could for instance be out of scope, imported
from another module, or declared in a super module): A
