Does Agda treat records and datatypes differently for the purposes of termination-checking?

Question

Here is an example of some Agda (2.4.2) code defining games and a binary operation on games.

module MWE where

open import Data.Sum
open import Size

data Game (i : Size) : Set₁ where
  game : {Move : Set} → {<i : Size< i} → (play : Move → Game <i) → Game i

_∧_ : ∀ {i j} → Game i → Game j → Game ∞
_∧_ {i} {j} (game {Move/g} {<i} play/g) (game {Move/h} {<j} play/h)
  = game {∞} {Move/g ⊎ Move/h}
      λ { (inj₁ x) → _∧_ {<i} {j} (play/g x) (game play/h)
        ; (inj₂ y) → _∧_ {i} {<j} (game play/g) (play/h y) }

This code type- and termination-checks. However, if I replace the definition of Game with a record definition, like so:

record Game (i : Size) : Set₁ where
  inductive
  constructor game
  field
    {Move} : Set
    {<i} : Size< i
    play : Move → Game <i

Agda no longer believes the definition of _∧_ to be terminating, even though the value of either i or j decreases in each recursive call. As far as I am aware, these two definitions of Game should be equivalent; what causes Agda to successfully termination-check the former, but not the latter?

Anonym

I suggest to ask on the Agda users mailing list. – Elasticize

Wild guess: I'd suspect that Size -based termination-check isn't used when checking whether record is decreasing argument. – Jackiejackinoffice

Shouldn't it be sufficient that one of the size arguments {i} and {j} themselves is decreasing? Not every argument to a function has to decrease in the recursive call. – Anonym