Unexpected crash

[vbgl]

The following program makes easycrypt crash.

Current main version (hash add9232): anomaly: File "src/ecUtils.ml", line 233, characters 24-30: Assertion failed
Latest release (2022.04): anomaly: File "src/ecUtils.ml", line 226, characters 24-30: Assertion failed

require import AllCore.

type t.
op d : t distr.

module M = {
  proc f() = {
    var k;
    k <$ d;
  }
}.

lemma correct_scheme &q : Pr[ M.f() @ &q : true ] = 1%r.
proof.
  byphoare.
  proc.
  auto => />.
abort.

[strub]

Note: require Distr solves the issue.

[oskgo]

Managed to trigger the same assertion:

require FinType.

op m (f: 'a -> 'b): 'b.

theory T.
clone FinType.FinType as FT.

type wrapper = [wrap of FT.t].

op foo: wrapper = m wrap.

end T.
clone T as T1.

clone T as T2 with
theory FT <- T1.FT,
type wrapper = T1.wrapper,
op foo <= T1.foo.

The fun part is that op m (f: 'a -> 'b): 'b = witness. makes it work.