## Stream: Coq users

### Topic: Problem with CPDT's dependent list examples

#### Mycroft92 (Jan 23 2023 at 09:56):

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".
``````

#### Janno (Jan 23 2023 at 09:58):

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

#### Mycroft92 (Jan 23 2023 at 10:06):

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.

#### Mycroft92 (Jan 23 2023 at 10:08):

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:

#### Mycroft92 (Jan 23 2023 at 10:12):

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.
``````

#### Janno (Jan 23 2023 at 10:12):

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.

#### Mycroft92 (Jan 23 2023 at 10:14):

Thanks, that indeed makes sense.

#### Meven Lennon-Bertrand (Jan 23 2023 at 11:45):

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

#### Meven Lennon-Bertrand (Jan 23 2023 at 11:46):

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.

#### Meven Lennon-Bertrand (Jan 23 2023 at 11:47):

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.

#### Gaëtan Gilbert (Jan 23 2023 at 11:50):

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

#### Meven Lennon-Bertrand (Jan 23 2023 at 11:52):

What are the two strategies exactly?

#### Meven Lennon-Bertrand (Jan 23 2023 at 11:52):

Constant return predicate and abstracting over everything possible?

#### Gaëtan Gilbert (Jan 23 2023 at 11:53):

IIRC one is equivalent to doing `return _` and the other I don't know

#### Pierre Courtieu (Jan 23 2023 at 12:19):

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

Last updated: Jun 25 2024 at 19:01 UTC