Malcolm Sharpe (Aug 23 2022 at 16:52): 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.)
Gaëtan Gilbert (Aug 23 2022 at 17:13):if you do Set Printing All you can see the difference
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?)
Notification Bot (Aug 23 2022 at 18:22):Malcolm Sharpe has marked this topic as resolved.
Gaëtan Gilbert (Aug 23 2022 at 19:51):inferring the return clause of matches is complicated
inferring universes with cumulativity is also complicated
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
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