Recursion on two inductive values is spuriously found divergent sometimes

[zephyrtronium]

Given a list-of-pairs type

pub type pmf<s, v>
  Event(s: s, v: v, next: pmf<s, v>)
  End

This function is inferred div and doesn't compile:

pub fun (*)(a: pmf<s, v>, b: pmf<s, v>, ?s/cmp: (a: s, b: s) -> order, ?v/(*): (new: v, old: v) -> e v): e pmf<s, v>
  match a
    End -> End
    Event(sa, va, nexta) -> match b
      End -> End
      Event(sb, vb, nextb) -> match sa.cmp(sb)
        Lt -> nexta * Event(sb, vb, nextb)
        Eq -> Event(sa, va * vb, nexta * nextb)
        Gt -> Event(sa, va, nexta) * nextb

This function is total (outside the polymorphic effect):

pub fun (*)(a: pmf<s, v>, b: pmf<s, v>, ?s/cmp: (a: s, b: s) -> order, ?v/(*): (new: v, old: v) -> e v): e pmf<s, v>
  match a
    End -> End
    Event(sa, va, nexta) -> match b
      End -> End
      Event(sb, vb, nextb) -> match sa.cmp(sb)
        Lt -> nexta * b
        Eq -> Event(sa, va * vb, nexta * nextb)
        Gt -> Event(sa, va, nexta) * nextb

The only change is reusing b instead of constructing Event in the Lt branch.