Почему Agda иногда жалуется на код, который пишет сам, когда вы используете разделение регистра? - PullRequest
Новая
       18

Почему Agda иногда жалуется на код, который пишет сам, когда вы используете разделение регистра?

3 голосов
/ 05 марта 2019

Я не уверен, что является минимальной репликацией этой проблемы, но этот Gist копирует ее. Обратите внимание на функцию preservation в конце файла: 

preservation : ∀ n Γ t t' T → t ~ t' → Γ ⊢ t ∷ T → Γ ⊢ t' ∷ T
preservation n Γ t t' T eq an = ?

Если мы попросим Agda разделить регистр на eq, он напишет этот код: 

preservation : ∀ n Γ t t' T → t ~ t' → Γ ⊢ t ∷ T → Γ ⊢ t' ∷ T
preservation n Γ .(app (lam _ _) _) .(subst (λ v → _) _) T ~β an = {!   !}
preservation n Γ .(app _ _) .(app _ _) T (~app eq eq₁) an = {!   !}
preservation n Γ .(lam _ _) .(lam _ _) T (~lam eq eq₁) an = {!   !}
preservation n Γ t .t T ~refl an = {!   !}
preservation n Γ t t' T (~sym eq) an = {!   !}
preservation n Γ t t' T (~trans eq eq₁) an = {!   !}

Что делает невозможным компиляцию из-за следующей ошибки: 

Failed to solve the following constraints:
  [543] subst (λ v → _331 n Γ T an v) (_t_332 n Γ T an)
          = subst (λ v → .x) .f
          : Term (_n_321 n)
when checking that the given dot pattern subst (λ v → _) _ matches
the inferred value subst (λ v → .x) .f

Это часто случается и очень раздражает. Интересно, что если я проведу рефакторинг типа ~, чтобы больше не использовать импликации, то попытка снова выполнить разделение регистра снова работает! Похоже, это как-то связано с неявными аргументами. Почему это происходит, и можно ли этого избежать?

...