Does Agda design records and data types differently for verification purposes?

Question

Here is an example of some games defining Agda games (2.4.2), and binary operation in 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 _∧_ : ∀ {ij} → 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/gx) (game play/h) ; (inj₂ y) → _∧_ {i} {<j} (game play/g) (play/hy) } 

This code type check and completion. However, if I replaced the definition of Game with the definition of a record, for example:

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

Agda no longer considers the definition of _∧_ complete, even if the value of any i or j decreases with every recursive call. To my knowledge, these two Game definitions should be equivalent; What makes Agda successfully stop checking the first, but not the last?