FSet library: subset is an operator rather than a predicate#3
Merged
Conversation
Inclusion is now written “\subset” (instead of “<=”). Strict inclusion is now written “\proper” (instead of “<”).
strub
added a commit
that referenced
this pull request
Apr 30, 2026
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.
strub
added a commit
that referenced
this pull request
Apr 30, 2026
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.
strub
added a commit
that referenced
this pull request
May 1, 2026
A typeclass with no [tc_args] (e.g. [addmonoid]) gets a trivial match from every instance during [candidates_by_args], because there are no patterns to constrain the candidate set. Firing Mode #3 in that case arbitrarily picked one instance and committed the carrier to its [tci_type] — surfacing as e.g. "no matching operator '+' for params [int, 'a]" because typing [idm + x] in a polymorphic-over-addmonoid context aggressively bound idm's carrier to int (from int_inst). Skip the by-args strategy when [tc.tc_args] is empty; the carrier will get bound through the surrounding type unification instead. Effects: tc/instance.ec, tc/explicit-tvi.ec, tc/smt.ec now pass.
strub
added a commit
that referenced
this pull request
Jun 15, 2026
…ysis) fapply_safe received a fully-typed form, so the operator's type arguments are already opened -- there was nothing to re-infer, and f_app_safe (which re-runs unification from a bare path) was only needed for the path-based entry point. Drop the per-head case analysis (Fop / Fapp / Llambda / assert-false): just build the application with f_app (which flattens a curried head) and normalise. f_app needs the result type, computed by peeling one arrow per argument while head-normalising at each step, so arrows hidden behind type abbreviations (e.g. u = int -> t, t = int -> int) are exposed. A non-reducible head (an opaque local, etc.) now normalises to the application f fs instead of hitting `_ -> assert false`. (This removes the fapply_safe anomaly of defect #3; circuit_of_node still needs to reject the resulting opaque application cleanly -- a separate follow-up.)
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
2 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.