Understanding unsolved metavariables and yellow highlighting in agda

Question

In the agda docs, I read that when "some meta-variable other than the goals cannot be solved the code will be highlighted in yellow"

I'm trying to understand this in a somewhat degenerate case.

If I define a regular product type then a stupid program works fine.

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

However, if I use a product as a special case of a dependent product, I get the yellow highlighting for stupid''''. Specifically, the fst and and the second 3 are highlighed yellow. Why do all the other stupid*'s work except for stupid''''? Are there any general tips for debugging yellow highlighting errors in 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

user3237465 user3237465 · Accepted Answer · 2020-05-18T21:16:14

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

This is because Agda can't infer the type of (3 , 3) to supply it to fst.

"But that's just Nat * Nat!"

Not necessarily, it can be

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

or any other weird type that gives Nat as a type of the second element whenever the first element is 3 and does something completely different in all other cases.

And Agda's unification machinery always either finds a unique solution or gives up.

You've asked Agda to solve the following unification problem:

_T 3 =?= Nat

and clearly there are way too many different _Ts that return Nat when the argument is 3.

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

Because in all the other ones there's no ambiguity:

in stupid the type of the second element does not depend on the first element (due to the definition of prod)
in other cases you explicitly specify the type of the argument (via a standalone declaration)

Understanding unsolved metavariables and yellow highlighting in agda

1 Answers