为了终止检查,Agda是否会以不同方式处理记录和数据类型？

Question

下面是一些定义游戏和游戏二进制操作的Agda(2.4.2)代码示例.

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) }

此代码类型和终止检查.但是,如果我用Game记录定义替换定义,如下所示:

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

Agda不再相信_?_终止的定义,即使每个递归调用中的值都减少i或j减少.据我所知,这两个定义Game应该是等价的; 是什么导致Agda成功终止 - 检查前者,而不是后者？