Skip to content

`Cancelable` instances for all elements of option/gmap

Robbert Krebbers requested to merge robbert/cancelable into master

Although the instances in this MR surely make sense, I am not so sure I like them very much: they overlap with already existing instances for specific elements, and could cause a lot of backtracking on deeply nested algebraic structures.

Global Instance cancelable_Some a :
  IdFree a → Cancelable a → Cancelable (Some a).
Global Instance option_cancelable ma :
  (∀ a, IdFree a) → (∀ a, Cancelable a) → Cancelable ma.

As I suggested in the comments in this MR, it may be better to have a type class of CmraCancelable that states that all elements of a camera are cancelable. However, on second thoughts I don't think that actually solves the backtracking problem.

Anyone an idea how to solve this? Should we care? We have the same problem for Discrete, e.g.:

Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
Global Instance option_ofe_discrete : OfeDiscrete A → OfeDiscrete optionC.
Global Instance None_discrete : Discrete (@None A).
Global Instance Some_discrete x : Discrete x → Discrete (Some x).
Edited by Robbert Krebbers

Merge request reports