Stream: Coq users

Topic: Problem with CPDT's dependent list examples


view this post on Zulip 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".

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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. matches are prime candidates because of dependent types.

view this post on Zulip Mycroft92 (Jan 23 2023 at 10:14):

Thanks, that indeed makes sense.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Meven Lennon-Bertrand (Jan 23 2023 at 11:52):

What are the two strategies exactly?

view this post on Zulip Meven Lennon-Bertrand (Jan 23 2023 at 11:52):

Constant return predicate and abstracting over everything possible?

view this post on Zulip Gaëtan Gilbert (Jan 23 2023 at 11:53):

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

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC