Anomaly in reduction when using subtypes

[oskgo]

MRE:

pragma +implicits.
require Subtype.
type 'a T'.

section.
declare type a.
type T = a T'.
subtype qT as ST = { x : T | true }.
realize inhabited by done.
axiom reprK: cancel witness ST.insubd.
end section.

lemma mset_eq: true.
rewrite -(reprK witness).

The repro is super fragile. Removing pragma +implicits fixes it, so does inlining the subtype, not using a type parameter, inlining ST.insubd, not using as ST or moving reprK out of the section..

To clarify; the intended behaviour here is for the rewrite to fail. I wasn't able to find a version where a rewrite that should succeed fails instead.

Backtrace

Raised at EcLib__EcCoreSubst.Tvar.init in file "src/ecCoreSubst.ml", line 732, characters 4-44
Called from EcLib__EcCoreSubst.Tvar.f_subst in file "src/ecCoreSubst.ml", line 736, characters 33-45
Called from EcLib__EcReduction.reduce_op in file "src/ecReduction.ml", line 708, characters 7-39
Called from EcLib__EcReduction.reduce_delta in file "src/ecReduction.ml", line 913, characters 15-56
Called from EcLib__EcReduction.reduce_head_top_force in file "src/ecReduction.ml", line 1184, characters 8-53
Called from EcLib__EcReduction.reduce_head_args in file "src/ecReduction.ml", line 1246, characters 9-47
Called from EcLib__EcReduction.reduce_head_sub in file "src/ecReduction.ml", line 1207, characters 15-45
Called from EcLib__EcReduction.reduce_head_top_force in file "src/ecReduction.ml", line 1195, characters 10-34
Called from EcLib__EcReduction.h_red in file "src/ecReduction.ml", line 1693, characters 4-41
Called from EcLib__EcReduction.h_red_opt in file "src/ecReduction.ml", line 1697, characters 11-28
Called from EcLib__EcProofTyping.lazy_destruct in file "src/ecProofTyping.ml", line 262, characters 12-62
Called from EcLib__EcProofTerm.get_implicits.doit in file "src/ecProofTerm.ml", line 242, characters 10-36
Called from EcLib__EcProofTerm.process_full_pterm in file "src/ecProofTerm.ml", line 855, characters 17-60
Called from EcLib__EcHiGoal.process_rewrite1_r.do1 in file "src/ecHiGoal.ml", line 966, characters 19-60
Called from EcLib__EcCoreGoal.FApi.t_try_base in file "src/ecCoreGoal.ml", line 782, characters 17-24
Called from EcLib__EcCoreGoal.FApi.t_ors_pmap.doit in file "src/ecCoreGoal.ml", line 862, characters 20-36
Called from EcLib__EcCoreGoal.reloc in file "src/ecCoreGoal.ml", line 286, characters 7-12
Called from EcLib__EcCoreGoal.FApi.on_sub1i_goals.do1 in file "src/ecCoreGoal.ml", line 568, characters 15-42
Called from EcLib__EcUtils.List.mapi_fold.(fun) in file "src/ecUtils.ml", line 533, characters 21-29
Called from Stdlib__List.mapi in file "list.ml", line 93, characters 15-21
Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25
Called from EcLib__EcUtils.List.mapi_fold in file "src/ecUtils.ml", lines 532-534, characters 13-8
Called from EcLib__EcCoreGoal.FApi.t_onalli in file "src/ecCoreGoal.ml", line 603, characters 18-53
Called from BatList.fold_lefti.loop in file "src/batList.ml", line 1038, characters 30-41
Called from EcLib__EcCoreGoal.FApi.on_sub1i_goals.do1 in file "src/ecCoreGoal.ml", line 568, characters 15-42
Called from EcLib__EcUtils.List.mapi_fold.(fun) in file "src/ecUtils.ml", line 533, characters 21-29
Called from Stdlib__List.mapi in file "list.ml", line 93, characters 15-21
Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25
Called from EcLib__EcUtils.List.mapi_fold in file "src/ecUtils.ml", lines 532-534, characters 13-8
Called from EcLib__EcCoreGoal.FApi.t_onalli in file "src/ecCoreGoal.ml", line 603, characters 18-53
Called from EcLib__EcHiTacticals.process in file "src/ecHiTacticals.ml", line 345, characters 11-42
Called from EcLib__EcHiTacticals.process1_seq.aux in file "src/ecHiTacticals.ml", line 112, characters 24-44
Called from EcLib__EcHiTacticals.process in file "src/ecHiTacticals.ml", line 364, characters 12-35
Called from EcLib__EcScope.Tactics.process_r in file "src/ecScope.ml", line 859, characters 15-40
Called from EcLib__EcCommands.process_tactics in file "src/ecCommands.ml", line 638, characters 21-64
Called from EcLib__EcCommands.process in file "src/ecCommands.ml", line 816, characters 23-32
Called from EcLib__EcUtils.timed in file "src/ecUtils.ml", line 48, characters 13-16
Called from EcLib__EcCommands.process in file "src/ecCommands.ml", line 984, characters 27-70
Called from Ec.main.(fun) in file "src/ec.ml", line 800, characters 36-88

[critical] [Test.ec:23] anomaly: File "src/ecCoreSubst.ml", line 732, characters 4-10: Assertion failed

[fdupress]

Do you get a warning on reprK? Maybe now is the time to turn it into an error... (But we should also root cause this.)

[oskgo]

Yes. I get a warning on the axiom in the section. There's a repro without an axiom in the section too though;

pragma +implicits.
require Subtype.
type 'a T'.

section.
declare type a.
type T = a T'.
subtype qT as ST = { x : T | true }.
realize inhabited by done.
op insubd = ST.insubd.
end section.

axiom reprK: cancel witness insubd<:'a>.

lemma mset_eq: true.
rewrite -(reprK witness).

For some reason this only works if I add op insubd = ST.insubd.

[fdupress]

Clarification for future readers "this only works" means "this only reproduces the anomaly."

qT should be parametric outside of the section. (Or the subtype forbidden.)

[oskgo]

That's not the problem here. @strub has put in some work to make sure that you can make subtypes parametric by using sections (#1002). This might be an unresolved edge case from that work, but I don't think we need to change the approach.

[fdupress]

The comment stems from print qT. after section close outputting type qT. (I would expect type 'a qT.)

We also get the global warnings on all the subtype axioms, which is probably not what we want if this is meant to be the main mechanism for making subtypes parametric.

But we do need to root cause which internal invariant (assumed by reduction) this is violating so we can try and fix the entry point, and separately figure out how we clean #1002 up.

[oskgo]

The comment stems from print qT. after section close outputting type qT. (I would expect type 'a qT.)

I'm getting type 'a qT from print qT as expected. Are you on the latest main? qT not being parametric should have been fixed by #1002.

[fdupress]

If I could react with a facepalm, I would. Sorry. Interestingly, I am getting the same anomaly prior to #1002 , which may inadvertently help root cause this.

[oskgo]

I also found a repro where the rewrite is supposed to succeed. It seems like it's triggered by a branch where it fails.

require Subtype.
type 'a T.

section.
declare type a.
subtype qT as ST = { x : a T | true }.
realize inhabited by done.
op insubd   : a T  -> qT = ST.insubd.
end section.

op repr: unit qT -> unit T.

lemma L (y x: unit T): (repr (insubd y) = y) =>
repr (insubd x) = x /\ repr (insubd y) = y.
move => yP.
rewrite yP.

I think this is going to block migrating the FSet and MSet theories to explicit quotients.