Hi Everyone,

I was working through the CPDT book chapter 9 and I hit a snag. The example code is given below. The book says the example should compile while on 8.16 version I get the below attached error. I understand what coq is throwing as error but my problem is convicing it that `fin 0`

has no members and thus the entire first case is unreachable.

Example:

```
Section ilist.
Variable A : Type.
Inductive ilist : nat -> Type :=
| INil : ilist O
| ICons : forall n, A -> ilist n -> ilist (S n).
Inductive fin : nat -> Set :=
| First : forall n, fin (S n)
| Next : forall n, fin n -> fin (S n).
Fixpoint get n (ls : ilist n) : fin n -> A :=
match ls with
| INil => fun idx =>
match idx in fin n' return (match n' with
| O => A
| S _ => unit
end) with
| First _ => tt
| Next _ _ => tt
end
| ICons _ x ls' => fun idx =>
match idx in fin n' return (fin (pred n') -> A) -> A with
| First _ => fun _ => x
| Next _ idx' => fun get_ls' => get_ls' idx'
end (get ls')
end.
End ilist.
```

The error:

```
Error: In environment
A : Type
get : forall n : nat, ilist n -> fin n -> A
n : nat
ls : ilist n
idx : fin ?n@{n1:=0}
The term
"match
idx in (fin n')
return match n' with
| 0 => A
| S _ => unit
end
with
| First _ => tt
| Next n0 _ => tt
end" has type "match ?n@{n1:=0} with
| 0 => A
| S _ => unit
end" while it is expected to have type
"A".
```

You can probably fix this by annotating the outer match on `ls`

to make sure coq knows `idx`

has type `fin n`

(where `n`

comes from the type of `ls`

)

Janno said:

You can probably fix this by annotating the outer match on

`ls`

to make sure coq knows`idx`

has type`fin n`

(where`n`

comes from the type of`ls`

)

Thanks Janno, I think that did the trick for first case. It still doesn't compile on the second case now. I will try to fix that as well.

It's weird that coq is not reusing the binding that was introduced right there and the fix appears more to be black magic now :sweat_smile:

Reannotating them did the trick: (for the sake of completeness the working solution)

```
Fixpoint get n (ls : ilist n) : fin n -> A :=
match ls in (ilist n) return (fin n -> A) with
| INil => fun idx =>
match idx in fin n' return (match n' with
| O => A
| S _ => unit
end) with
| First _ => tt
| Next _ _ => tt
end
| ICons _ x ls' => fun idx =>
match idx in (fin n') return (ilist (pred n') -> A) with
| First _ => fun _ => x
| Next _ idx' => fun ls' => get _ ls' idx'
end ls'
end.
```

It's often a bit mysterious at first glance but I think it is not too hard to figure out what is going wrong in cases like this. The type of `idx`

in the context contained in the error message reads `fin ?n@{..}`

, i.e. `fin`

applied to a unification variable/existential variable. This means that at the time of the error coq's typechecker has no idea what the parameter to `fin`

is supposed to be. This can happen for various reasons but the workaround is almost always the same: annotate everything, preferably starting from the outside where most type information is available. `match`

es are prime candidates because of dependent types.

Thanks, that indeed makes sense.

Note that once you corrected the problem in the second case, you can actually remove the annotations you added!

This is a common issue with dependent pattern-matching: Coq throws a type error, that you interpret as it not being smart enough to infer the right annotation. You give an explicit annotation. Now it does not complain about the original type error, but about another one, which is a genuine error. You fix that error. Now you can remove your annotation, and Coq happily infers it.

What happens under the hood is that your genuine error is leading the type inference astray, making it unable to infer the "right" annotation for your pattern-matching, because this annotation still causes a type error.

this happens because Coq tries 2 strategies for inferring the annotation when it's not provided, but it only gives the error for 1 if they both fail

so when the "real" error happens with the other strategy fixing it also fixes inference

What are the two strategies exactly?

Constant return predicate and abstracting over everything possible?

IIRC one is equivalent to doing `return _`

and the other I don't know

This also happen, although in simpler contexts, with any type inferring language. In ocaml putting type labels makes error messages more precise.

Last updated: Oct 04 2023 at 20:01 UTC