Checker false positive: typed when-params not registered as bindings (allium.rule.undefinedBinding)

[yenda]

Summary

allium check reports allium.rule.undefinedBinding for a rule that references a typed when-param (param: Type) in its body. The same body reference against an untyped when-param (param) checks clean. Typed when-params appear not to be registered as bindings, so every body reference to one is flagged as undefined.

Minimal repro

-- allium: 3

entity Account {
    name: String
}

entity Greeting {
    label: String
}

-- TYPED when-param: `account: Account`. Body references `account`.
rule TypedParam {
    when: AccountSeen(account: Account)
    ensures: Greeting.created(label: account.name)
}

-- UNTYPED when-param for contrast: `account`. Same body reference.
rule UntypedParam {
    when: AccountSeen2(account)
    ensures: Greeting.created(label: account.name)
}

Expected

Both rules check clean. account: Account declares a typed trigger param named account of type Account, which should be in scope for the rule body exactly as the untyped form is. The language reference documents the typed form for state-transition, temporal and creation triggers (var: Type), and it is the natural way to give an external-stimulus param an explicit type.

Actual

TypedParam errors; UntypedParam does not:

error allium.rule.undefinedBinding :: Rule 'TypedParam' references 'account'
  but no matching binding exists in context, trigger params, default
  instances, or local lets.

UntypedParam produces no undefinedBinding diagnostic. The only difference between the two rules is the : Account type annotation on the param.

Environment

• allium 3.2.4 (language versions: 1, 2, 3)
• Reproduces with both -- allium: 2 and -- allium: 3 markers.

Impact

Specs that annotate external-stimulus trigger params with explicit types (for readability / type-checking) accrue one false-positive error per body reference. There is no clean workaround short of dropping the type annotation, which loses the type information the checker could otherwise use.