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.)
if you do Set Printing All
you can see the difference
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?)
Malcolm Sharpe has marked this topic as resolved.
inferring the return
clause of matches is complicated
inferring universes with cumulativity is also complicated
btw you can also do if b return Set then bool else bool
instead of a cast
see also https://github.com/coq/coq/issues/16068
Last updated: Oct 03 2023 at 21:01 UTC