Use solely canonical structures for language hierarchy.
As @jung observed in !87 (merged), Coq is unable to infer CtxLanguage
instances. This problem was there before already, and as such, we already duplicated lemmas like wp_bind
a bunch of times. For example, in lifting
we had:
Lemma wp_ectx_bind {E Φ} K e :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
Proof. apply: weakestpre.wp_bind. Qed.
The problem here is that we mixed canonical structures and type classes in a rather odd way for the hierarchy of languages (language
, ectxLanguage
, ectxiLanguage
): language
was a canonical structures, but ectxLanguage
and ectxiLanguage
were type classes.
In this MR, I have repaired this issue: I am now using solely canonical structures for the three layers of the language hierarchy.
FWIW: Similar to the canonical structures for OFEs, cameras, and soon BIs, I have also factored out the laws into a mixin.
Edited by Robbert Krebbers