typechecking - 了解 agda 中 Unresolved 元变量和黄色突出显示

Question

在 agda 文档中，我读到当“无法解决目标以外的某些元变量时，代码将以黄色突出显示”

我试图在一个有点退化的案例中理解这一点。

如果我定义一个常规产品类型，那么一个愚蠢的程序就可以正常工作。

data _==_ {l}{X : Set l}(x : X) : X -> Set where
  refl : x == x

data prod (A B : Set) : Set where
  _,,_ : A → B → prod A B

fst' : {A B : Set} → prod A B → A
fst' (x ,, x₁) = x

stupid : fst' (3 ,, 3) == 3
stupid = refl

但是，如果我将某个产品用作依赖产品的特例，我会得到 stupid'''' 的黄色突出显示。具体来说，fst 和第二个 3 以黄色高亮显示。为什么除了 stupid'''' 之外的所有其他 stupid* 都能正常工作？是否有调试 agda 中黄色突出显示错误的一般提示？

record Sg {l}(S : Set l)(T : S -> Set l) : Set l where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg public

_*_ : forall {l} -> Set l -> Set l -> Set l
S * T = Sg S \ _ -> T

infixr 40 _,_
infixr 20 _*_

threethree : Nat * Nat
threethree = 3 , 3

three : Nat
three = fst threethree

stupid'' : three == 3
stupid'' = refl

stupid''' : fst (threethree) == 3
stupid''' = refl

--here's the yellow highlighting
stupid'''' : fst (3 , 3) == 3
stupid'''' = refl

Answer 1

--here's the yellow highlighting
stupid'''' : fst (3 , 3) == 3
stupid'''' = refl

这是因为 Agda 无法推断 (3 , 3) 的类型以将其提供给 fst。

“但这只是 Nat * Nat!”

不一定，可以

Sg Nat \n -> if n == 3 then Nat else Bool

或任何其他奇怪的类型，只要第一个元素是 3 就将 Nat 作为第二个元素的类型，并且在所有其他情况下做完全不同的事情。

而 Agda 的统一机制总是要么找到唯一的解决方案，要么放弃。

你要求 Agda 解决以下合一问题:

_T 3 =?= Nat

显然，当参数为 3 时，有太多不同的 _T 返回 Nat。

Why do all the other stupid*'s work except for stupid''''

因为在所有其他的中没有歧义:

• 在stupid中第二个元素的类型不依赖于第一个元素(由于prod的定义)
• 在其他情况下，您明确指定参数的类型(通过独立声明)