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.
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