Stream: Coq users

Topic: ✔ Puzzling error with dependent types


view this post on Zulip Malcolm Sharpe (Aug 23 2022 at 16:52):

This error complains that two types are different, but they look exactly the same.

In environment
b : bool
The term "has_opt b" has type "option (if b then bool else bool)"
while it is expected to have type "option (if b then bool else bool)".

It is produced by the following code:

Definition no_opt (b : bool) :=
  if b return (if b then bool else bool) then true else true.

Definition has_opt (b : bool) :=
  if b return option (if b then bool else bool) then Some true else Some true.

Fail Lemma has_quant : forall b, Some (no_opt b) = has_opt b.

I think this is the simplest code to reproduce the error. (If I remove the quantifier, for example, the error no longer occurs.) What's going on?

(I am using version 8.15.2, by the way.)

view this post on Zulip Gaëtan Gilbert (Aug 23 2022 at 17:13):

if you do Set Printing All you can see the difference

view this post on Zulip Malcolm Sharpe (Aug 23 2022 at 17:45):

Thanks. That gave me enough hints to update the definition of has_opt to this working definition:

Definition has_opt (b : bool) :=
  if b return option ((if b then bool else bool) : Set) then Some true else Some true.

I don't know why it was that it got the strange type in the first place, though. (I guess I should be reading about universes?)

view this post on Zulip Notification Bot (Aug 23 2022 at 18:22):

Malcolm Sharpe has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Aug 23 2022 at 19:51):

inferring the return clause of matches is complicated
inferring universes with cumulativity is also complicated

view this post on Zulip Gaëtan Gilbert (Aug 23 2022 at 19:52):

btw you can also do if b return Set then bool else bool instead of a cast

view this post on Zulip Gaëtan Gilbert (Aug 23 2022 at 19:53):

see also https://github.com/coq/coq/issues/16068


Last updated: Oct 03 2023 at 21:01 UTC