了解 agda 中未解决的元变量和黄色突出显示

Question

在 agda 文档中，我读到 "some meta-variable other than the goals cannot be solved the code will be highlighted in yellow"

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

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

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。

"But that's just Nat * Nat!"

不一定，可以

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

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

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

您要求 Agda 解决以下合一问题：

_T 3 =?= Nat

很明显，当参数为 3.

时，return Nat 有太多不同的 _T

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

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

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

了解 agda 中未解决的元变量和黄色突出显示

Understanding unsolved metavariables and yellow highlighting in agda

typechecking

agda