Hi, I'm probably overlooking something basic, but why won't Coq accept this definition?

```
From Coq Require Import Lists.List.
Check (fun A (P : A -> Prop) (x : A) (xs : list A) (ps : Forall P (x :: xs)) => match ps with | Forall_cons _ p _ => p end)
```

It gives the error:

Incorrect elimination of "ps" in the inductive type "Forall":

the return type has sort "Type" while it should be "SProp" or "Prop".

Elimination of an inductive object of sort Prop

is not allowed on a predicate in sort Type

because proofs can be eliminated only to build proofs.

But `p`

should have type `P x`

of sort `Prop`

, not `Type`

That's for extraction. Prop is not extracted, so if you were allowed to make the return value of a program (something in Type) depend from a spec formula (something in Prop), there would be holes in your extracted programs.

Right, but I am under the impression that my return type is actually in Prop. Why is that not allowed?

the error is a small inversion limitation (or bug? related to the error you get on `Check True = nat.`

)

using a copy of Forall in Type we see

```
Inductive ForallT {A : Type} (P : A -> Prop) : list A -> Type :=
ForallT_nil : ForallT P nil
| ForallT_cons : forall (x : A) (l : list A), P x -> ForallT P l -> ForallT P (x :: l)
.
Arguments ForallT_cons [_ _] _ [_].
Check (fun A (P : A -> Prop) (x : A) (xs : list A) (ps : ForallT P (x :: xs)) => match ps with ForallT_cons _ p _ => p end).
(*
fun (A : Type) (P : A -> Prop) (x : A) (xs : list A) (ps : ForallT P (x :: xs)) =>
match
ps as ps0 in (ForallT _ l)
return
(match l as x0 return (ForallT P x0 -> Type) with
| nil => fun _ : ForallT P nil => IDProp
| x1 :: x0 => fun _ : ForallT P (x1 :: x0) => P x1
end ps0)
with
| ForallT_nil _ => idProp
| ForallT_cons _ p _ => p
end
*)
```

the issue is the generated `-> Type`

which would work if it was `-> Prop`

I don't know if it's possible to generate `-> Prop`

, not it would be good to have a better error

Thanks for the explanation, that's unfortunate. I don't get anything surprising with `check True = nat`

though:

The term "nat" has type "Set" while it is expected to have type

"Prop" (universe inconsistency: Cannot enforce Set = Prop).

And additionally: is there a way to see the expanded Gallina term that Coq cannot type check? That would make it much easier for me to understand these subtleties.

some find that error surprising, considering `Check nat = True`

works fine

I don't think there's a way to get that term

Ah yes, now I do find it surprising :) Thanks

another similar surprising error is `Check forall P, P -> exists x, P.`

@Gaëtan Gilbert Instead of poking where it hurts, there is also the plan to solve this with variable sorts in unification... Any progress on that front?

Last updated: Sep 15 2024 at 13:02 UTC