Add comment.

theories/program_logic/ectx_language.v

@@ -216,6 +216,13 @@ End ectx_language.
 Arguments ectx_lang : clear implicits.
 Coercion ectx_lang : ectxLanguage >-> language.
 
+(* This definition makes sure that the fields of the [language] record do not
+refer to the projections of the [ectxLanguage] record but to the actual fields
+of the [ectxLanguage] record. This is crucial for canonical structure search to
+work.
+
+Note that this trick no longer works when we switch to canonical projections
+because then the pattern match [let '...] will be desugared into projections. *)
 Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
   let '@EctxLanguage E V C St of_val to_val empty comp fill head mix := Λ in
   @Language E V St of_val to_val _

[Ralf Jung]

Even with canonical projections/primitive records, the Eval hnf in used by ssreflect should still work, right?

Canonical Structure foo : fooT := Eval hnf in ...

[Robbert Krebbers]

No, it does not. We need more than just a head normal form, we need some the canonical projections to be turned into head normal form.

If you do what you suggest you will get something like:

{|
  language.val := ectx_language.val Λ;
  ...
|}

For the case of, say, heap_lang, you want ectx_language.val Λ to be turned into heap_lang.val.

[Ralf Jung]

It was my understanding that ssreflect has exactly that issue as well... @janno?

[Ralf Jung]

One example is https://github.com/math-comp/math-comp/blob/2a8af6f6b80c82a5f07cae220427cccc30ef8dac/mathcomp/real_closed/ordered_qelim.v#L76, with EqType defined at https://github.com/math-comp/math-comp/blob/2a8af6f6b80c82a5f07cae220427cccc30ef8dac/mathcomp/algebra/finalg.v#L93.

[Robbert Krebbers]

Note that they explicitly give the value of the canonical projection. We do not want to do that in this case, since we have plenty of them (val, expr, state, ectx).

[Ralf Jung]

Ah, I see. So we'd need some more advanced ltac:(...) magic then.

[Robbert Krebbers]

Probably, if we want to make it work with primitive projections.