in context `Require Vector.`

, what happens for each check?

```
Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t _ (S m) return True with
|Vector.cons _ h _ _ => h
end).
Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t _ _ return True with
|Vector.cons _ h _ _ => h
end).
Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t _ _ with
|Vector.cons _ h _ _ => h
end).
Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t@{} _ _ with
|Vector.cons _ h _ _ => h
end).
Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t True _ with
|Vector.cons _ h _ _ => h
end).
```

I think the 5th one fails because of the constant argument `True`

. And I suppose (otherwise you would not ask) that the 4th one fails due to the nonsensical universe constraint.

what do you mean nonsensical? `Check Vector.t@{}.`

works fine

I mean that it is the same as for the 5th case. Universes have no impact on the matching, so they do not make sense there, same as constant argument.

Universes have no impact on the matching

unfortunately that's not really true at least from the kernel point of view

Do you mean that it would make sense to match on a universe and then use it in the `return`

clause?

not match on it, but consider how `fun x => match x in bool with _ => tt end`

constraints the type of `x`

, parameters and univs in the `in`

clause could also constraint the discriminee

But matching with a pure wildcard is such a degenerate case. Not sure it is worth making things more complicated just for it.

the data is there in the kernel so we should have a way to print it. then it's natural to also parse it.

Actually, I am surprised it is there in the first place. I would have expected only the binders to appear in the kernel `in`

clause, not the full inductive type.

About the return clause, the kernel sees the instance, the parameters and that's about it (the names are also there but not relevant).

Last updated: Feb 01 2023 at 15:04 UTC