Conversation
…f_tparams; SMT pre-reduction restricted to delta_tc only
Replaces a debug-style 'EcPath.tostring p' with the user-facing pretty-printer 'pp_axname'.
op_symb resolves a notation by (kind, tyargs, argtys); witnesses do not participate in notation selection, so no TC handling is needed here.
Verifies that 'print' on TC-constrained abstract types, on the typeclass declaration, and on a TC operator does not crash.
- ecHiGoal: SFop's tvi is already an etyarg list and Tvar.f_subst takes etyarg, so witnesses already flow through. - ecHiInductive emptiness / ecInductive positivity: both use List.fst targs (resp. etyarg_sub_exists), which already inspect TC witnesses correctly.
Verifies that 'apply (lemma<:int>)' picks up the right named instance and that omitting the TVI also resolves via unification.
Verifies that operators/lemmas defined over a sectioned 'declare type t <: tc' survive section close as proper TC-polymorphic forms.
Why3 types do not carry TC witnesses; the witnesses are erased here intentionally because they are either inlined by delta_tc pre-reduction or absent on concrete carriers.
Threads env into pf_check_tvi so it can call EcTypeClass.infer on each ground (no Tunivar/Tvar) user-supplied type for every TC constraint declared on the corresponding tparam. Replaces a confusing post-hoc 'int doesn't match int' unification error with a clear: type int does not satisfy typeclass constraint addmonoid at the call site. Polymorphic (Tvar) and unified (Tunivar) cases are left to the unifier as before.
…lti-instance Documents that SMT-over-TC currently works for: concrete instances (via delta_tc pre-reduction), abstract carriers with explicit TC axiom hints, inheritance chains, sectioned 'declare type t <: tc' carriers, and goals mixing two different concrete instances of the same class.
TC instance disambiguation happens at typing time via explicit instance selection; delta_tc pre-reduction inlines concrete instances before Why3 translation; abstract-carrier goals carry their TC axioms as user hints. Translating tparams as plain Why3 type variables (resp. opaque types) is correct for the current design — SMT-over-TC test suite covers concrete, abstract, inheritance, declare-type and multi-instance cases.
Adds [trans_tc_axioms]: for each typeclass constraint on a goal-context type parameter, walks the parent chain via [EcTypeClass.ancestors] and emits each TC's axioms as Why3 axioms tied to the (opaque) tparam type. This closes the gap where smt() (no hints) could not use TC axioms over an abstract carrier — the axioms are registered globally with NoSmt visibility, so the relevance heuristic never picked them up. After this change, smt() over a tparam 'a <: tc gets every axiom of tc and its ancestors, instantiated polymorphically, which Why3 then unifies to the tparam's opaque type. Verified: 113/113 stdlib + 27/27 unit; tests/tc/smt.ec extended with no-hint lemmas over plain TC and a TC-inheritance chain.
After the outline tactic rework, generated proof obligations reference Distr.support via f_in_supp; the test file only required AllCore, so the path was unresolved. Adding Distr to the imports fixes the regression.
- ecTyping.ml:1035 (transtc): use unify_or_fail so a failed TC arg unification raises a typed tyerror instead of escaping UnificationFailure. - ecSection.ml:563 (tg_params): use the existing ty_params alias. - ecSection.ml:1045 (generalize_instance): apply tg_subst to the instance, fixing instances declared inside a section that referenced declared/abstracted types. - ecSubst exposes subst_tcinstance. - ecTheoryReplay tparams_compatible / get_open_oper: drop stale FIXME:TC markers (TC compatibility flows through ty_compatible's etyargs_of_tparams substitution and the unifier's TcCtt arm; the discarded type from open_oper is checked elsewhere via expr_compatible).
Empty etyargs '[...]' on the type and inside concrete TC witnesses produced 'addmonoid[]' / 'int[int_inst[]]' style noise. Now: 'addmonoid' / 'int[int_inst]' for the common nullary / single-instance case.
…rete carriers tests/tc/diamond.ec covers two-branch inheritance with SMT auto-axiom inclusion across multiple ancestors. tests/tc/clone-with-instance.ec covers cloning an abstract theory with a concrete carrier that has a TC instance. This previously failed because subst_tcw produced a 'Abs <concrete-path>' witness that the reducer treated as opaque. ecReduction: add resolve_concrete_tcw — when the witness is 'Abs p' and p is a concrete (non-abstract) type, infer the concrete instance via EcTypeClass.infer at reduction time. Wired into reduce_tc / reduce_tc_op.
tcenv_closed (cardinality check), Tuni.univars-of-ty in create_tcproblem (correctness suffices: a witness depends on its carrier type's univars, and resolution is re-seeded in unify_core's seed phase), the byunivar lookup (cache hint without observable cost), the push API (internal-only), and the select_op return tuple — all marker-only with no observable bug. The single remaining FIXME:TC at ecSubst.ml:226 covers the unreachable tuple/fun alias-body branch (instance declarations on tuple/fun types are rejected upstream), kept for future audit if upstream loosens.
Covers a two-parameter ['a, 'b] embed typeclass with carrier 'c, a polymorphic-over-multi-param lemma, and a concrete instance for (int * bool) constructed via 'instance (int, bool) embed as pair_inst with (int * bool)'. Documents that explicit positional tvi (<:'a, 'b, 'c>) is required for bare op resolution because parametric carriers cannot always be inferred from source/target types alone.
…aints
Constraints can reference earlier tparams (e.g. 'c <: ('a, 'b) embed). Without substituting the user-supplied bindings 'a := int, 'b := bool first, the [infer] call sees an open ('a, 'b) embed and rightly fails to find an instance, even when one exists.
The fix threads an [etyarg Mid.t] accumulator through the per-tparam checks, applying it via [EcCoreSubst.Tvar.subst_tc] before each [infer]. tests/tc/multi-param.ec exercises this with a polymorphic-over-multi-param lemma applied at a concrete (int, bool) embed instance.
When a typeclass body has an axiom or operator type whose typing leaves free type/typeclass variables (e.g. 'axiom foo : zero = zero' with [zero] from a grandparent class), the unienv close emitted a raw [EcUnify.UninstanciateUni] anomaly. Now it raises a typed [hierror] at the offending axiom/operator location with a hint to pin the carrier via '<:tc>'. tests/tc/grandparent-op.ec covers: explicit '<:carrier>' workaround, and the carrier-typed-argument workaround.
Adds doc/typeclasses.md describing what is currently implemented (declaration, multi-parameter, instances, polymorphic ops/lemmas, sections, cloning, reduction, SMT integration, diamond inheritance, pretty-printing), known limitations (bare-op parametric-carrier inference, tuple/fun instance carriers, reverse-rewrite matcher), and a map from features to source files and test cases.
doc/typeclasses-inference.md catalogues every shape of TcCtt problem the unifier resolves, identifies Mode #3 (univar carrier with ground TC args) as the bare-op gap, and lays out the strategy framework that Phases 2 and 3 will implement.
…hange) Splits the existing TcCtt resolution logic into three named local helpers — strat_tvar_via_tvtc, strat_abs_via_decl, strat_infer_by_carrier — corresponding to catalog modes #5, #6, and #1/#2 in doc/typeclasses-inference.md. Behavior is identical: same dispatch order, same failures, same pickup of [Tvar a]/[Tconstr p] cases, same parking of univar carriers. The refactor exists so Phase 3 can drop a By-args strategy in without disturbing the existing logic.
Adds Mode #3 from doc/typeclasses-inference.md: when a TcCtt has a Tunivar carrier, walk all instances and pick the unique one whose tc_args match (Tunivars in the goal are wildcards for matching). On a unique match, push TyUni equations binding goal Tunivars to the candidate's substituted patterns and the carrier to tci_type; the deferred witness is then produced by Mode #1 on re-fire. Also restores deref_tc inside eq_tc which Phase 2's refactor inadvertently dropped — needed because tvtc stores TC constraints with Tunivars that get merged in [uf] later. Lax matching: TyMatch.doit_type now treats Tunivar on the [ty] side as a wildcard (matches any pattern). Safe because the downstream [check_tcinstance] post-match still requires every instance tparam to be bound, so partial matches are rejected at the final witness-construction step. Closes the bare-op gap for parametric-carrier multi-param TCs: [multi-param-bare-ops.ec](tests/tc/multi-param-bare-ops.ec) covers four shapes: bare both sides, in a lemma, fixed result type only, fixed source type only. multi-param.ec simplified to use bare ops where applicable.
Replaces the 'bare-op parametric-carrier inference fails' limitation with the narrower 'polymorphic-body still needs explicit tvi' note. Adds tests/tc/multi-param-bare-ops.ec to the test inventory.
- config/tests.config: new test-tc-ko scenario backed by tests/tc-ko/, files there must fail to compile. test-unit excludes the directory. - ecUnify: new exception AmbiguousTcInstance; the By-args strategy raises it when multiple candidate instances disagree on the carrier ([tci_type] differs across candidates). - ecTyping: TypeClassAmbiguous tyerror variant; unify_or_fail catches AmbiguousTcInstance and converts. - ecUserMessages: top-level printer for AmbiguousTcInstance and the typed TypeClassAmbiguous variant. Replaces the previous generic 'free type/typeclass variables' close-time message with a clear list of candidate instance paths. - tests/tc-ko/: three regression tests for negative-typing diagnostics: - bad-tvi.ec — pf_check_tvi rejects [<:int>] for a 'a <: addmonoid tparam - underconstrained-axiom.ec — typeclass body axiom with a free carrier - ambiguous-instance.ec — two distinct instances of (int, bool) embed All 113/113 stdlib + 32/32 unit + 3/3 tc-ko pass.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.