CODEWITHSUNDEEP
typecheckingagda
user5775230
user5775230

Reputation:

Understanding unsolved metavariables and yellow highlighting in agda

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

Upvotes: 3

Views: 379

Answers (1)

effectfully
effectfully

Reputation: 12715

--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)

Upvotes: 2

Related Questions