# Error Abstracting over the term leads to a term which is ill-typed when doing a destruct

I'm trying to make a version of nth that cannot fail because it knows that the index is inbounds. So far, so good:

Program Definition nth_safe {A} (l: list A) (n: nat) (IN: (n < length l)%nat) : A :=
match (nth_error l n) with
| Some res => res
| None => _
end.
Next Obligation.
symmetry in Heq_anonymous. apply nth_error_None in Heq_anonymous. lia.
Defined.


But I'm stuck proving something about it:

Lemma nth_safe_nth: forall A (l: list A) (n: nat) d (IN: (n < length l)%nat), nth_safe l n IN = nth n l d.
Proof.
intros A l n d IN. unfold nth_safe. destruct nth_error eqn:E.


This should be a simple proof, but the destruct gives me an error I do not understand:

Abstracting over the term "o" leads to a term
(...)
which is ill-typed.
Reason is: Illegal application: The term "nth_safe_obligation_1" of type
(...)
cannot be applied to the terms
"A" : "Type"
"l" : "list A"
"n" : "nat"
"IN" : "(n < length l)%nat"
"Heq_anonymous" : "None = o0"
The 5th term has type
"None = o0"
which should be coercible to
"None = nth_error l n".;


Admittedly, the error is quite obscure, but the issue is that, while you do not see it, nth_safe_obligation_1 … uses nth_error l n, so destructing the latter makes the former ill-typed. A solution is to simply get rid of this dependency, by forgetting what exactly that proof looks like:

Lemma nth_safe_nth: forall A (l: list A) (n: nat) d (IN: (n < length l)%nat), nth_safe l n IN = nth n l d.
Proof.
intros A l n d IN.
unfold nth_safe.
set (x := nth_safe_obligation_1 _ _ _ _) ; clearbody x ; cbn in x.
destruct nth_error eqn:Heq.
- symmetry.
now apply nth_error_nth.
- apply nth_error_None in Heq.
lia.
Qed.


The magic line is the set…, which abstracts away the proof obligation. After this step, destruct now goes through!

• Thanks! But I don't quite understand why the destruction causes nth_safe_obligation_1 ... to become ill-typed. An nth_error l n term could just be reconstructed from the things I got from the destruction, right? Commented May 8 at 16:13
• This is due to the way destruct works. In essence, when you do destruct t with a goal g, Coq is going to turn g into some convertible (fun x : A. g')~t (ie g would be g'[t/x], and then case-split on t. However, this abstraction of t in g might fail due to dependent types: replacing all occurrences of t in g by a fresh variable x can give you a g' which is ill-typed. As a very simple example, if f : forall a, a = 0 -> …, then f 0 eq_refl is well-typed, but f x eq_refl is not, and so destruct 0 fails. Your issue is a more complicated variant of this. Commented May 9 at 10:29