type constraint error for out-of-order prime subterm multiplicands

[WeeknightMVP]

// PrimeCommMult.cry
module PrimeCommMult where

interface submodule I where
  type m : #
  type k : #  // moving above `m` removes the error
  type constraint (prime (k*m + 1))  // [error] (if order of multiplicands doesn't match above)

submodule F where
  import interface submodule I

submodule S where
  import interface submodule I
  import submodule F { interface I }

Cryptol> :l PrimeCommMult.cry
Loading module Cryptol
Loading module PrimeCommMult

[error] at PrimeCommMult.cry:1:1--14:21:
  Failed to validate user-specified signature.
    when checking the module's parameters,
    we need to show that
      for any type PrimeCommMult::S::I::k, PrimeCommMult::S::I::m
      assuming
        • prime (1 + PrimeCommMult::S::I::m * PrimeCommMult::S::I::k)
      the following constraints hold:
        • prime (1 + PrimeCommMult::S::I::k * PrimeCommMult::S::I::m)
            arising from
            module instantiation at PrimeCommMult.cry:7:19--7:36
            at PrimeCommMult.cry:14:3--14:21

The error occurs if the prime constraint is expressed with interface fields in a different order (multiplication commutativity does not apply). If 1 is generalized to another parameter a and the constraint to prime (m*k + a) or prime (a + m*k), the constraint is resolved (if m and k are in order) regardless of where type a : # is added to the interface (addition commutativity applies).

[WeeknightMVP]

Revisiting, the error appears to be based on the order of the parameters in the interface, not the order of arguments in the constraint. The examples produce an error regardless of the order of prime operands, and after swapping k and m in the interface, work regardless of the order of prime operands.