了解未解决的元变量和以黄色表示的黄色突出显示

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

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

而且，Agda的统一机制总是找到独特的解决方案，或者放弃。

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

_T 3 =?= Nat

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

为什么stupid*以外的所有其他stupid''''工作，>

因为其他所有内容都没有歧义：

• 在stupid中，第二个元素的类型不取决于第一个元素（由于[C​​0]的定义）
• 在其他情况下，您通过独立声明显式指定参数的类型]