ychr-0.1.0.0: typechecker/typechecker.chr

:- module('$typechecker', [
    constraint_sig/2,
    function_sig/2,
    function_sigs/2,
    function_bounds/2,
    constraint_bounds/2,
    con_sig/2,
    check_constraint_use/3,
    check_function_use/4,
    check_function_use_with_ambient/5,
    check_constructor_use/4,
    check_unify/3,
    check_guard_bool/2,
    check_guard_getarg/5,
    check_bound/4,
    ambient_sig/3,
    active_scope/1,
    end_scope/1,
    errors/1,
    collect/1
]).

:- use_module(library(prelude)).
:- use_module(library(lists)).

% Type-representation algebraic type. Mirrors the value-level encoding
% emitted by src/YCHR/Internal/TypeCheck.hs (encodeTypeExpr): base types are
% 0-arity constructors, type constructors and function types are
% compound terms. The first field of `tcon` is `any` because a type
% constructor name may be either an atom (`bool`) or a qualified
% atom (e.g. `prelude:bool`). Qualified type names that originate in
% this CHR source — as opposed to being passed in by the Haskell
% driver — must be wrapped in `quote/1` so the renamer treats them as
% opaque data rather than as cross-module references subject to
% value-level visibility checks. See language.md §The `quote/1`
% quoting form.
% `rigid(N)` is a *rigid* type variable: a fresh identity allocated
% by the driver while checking a polymorphic declaration's own
% equations or rule bodies. Unlike unbound CHR variables (which are
% *flexible* and consistent with every declared type per the gradual
% guarantee), a rigid tvar is only consistent with itself and `any`.
% This is what closes the soundness gap where a polymorphic body
% calling an overloaded function at its own type parameter would
% silently type-check without a `requiring` clause.
:- chr_type ty ---> int
                  ; float
                  ; string
                  ; any
                  ; tcon(any, list(ty))
                  ; fun(list(ty), ty)
                  ; rigid(int).

% Polymorphic two-field record reused for both function signatures
% (sig_t(list(ty), ty)) and constructor signatures
% (sig_t(ty, list(ty))).
:- chr_type sig_t(A, B) ---> sig(A, B).

% Accumulated diagnostics. Ctx is the integer source-location handle
% emitted by the Haskell driver; Code is an atom; Detail is
% heterogeneous (`pair(T1, T2)`, atoms, names).
:- chr_type error ---> error(int, any, any).

% Atoms used as the Code field of `error/3`. Declared so the renamer
% recognizes them as data constructors; the value-level type stays `any`.
% `bound_unsatisfied` is emitted CHR-side from `check_bound` when no
% declared signature of the bound's named function is consistent with
% the substituted bound. The other bounded-polymorphism error codes
% (unbound bound variable, unknown bound function, bound cycle,
% extend-on-bounded) are produced by the Haskell resolver and never
% flow through this CHR program.
:- chr_type error_code ---> inconsistent
                          ; no_matching_overload
                          ; bound_unsatisfied.

% Literal values used as the Detail field of `error/3`. Detail is
% heterogeneous (atoms, pairs, constraint-name variables); only the
% literal constructors appearing in `report_error` calls need entries.
:- chr_type error_detail ---> pair(any, any)
                            ; overloaded.

% A named bound signature inside a `requiring` clause: the bound
% function's flat-atom name together with the argument-types and
% return-type of its required signature. The fields share logical
% variables with the enclosing declaration's primary signature; both
% are bundled in `function_bounds` / `constraint_bounds` so a single
% `copy_term` freshens them consistently at each use site. Storing
% the args/ret flat (rather than wrapped in `sig_t`) keeps the type
% checker's pattern inference simple, and matches the shape the
% discharge rule consumes.
:- chr_type bound_named ---> nbound(any, list(ty), ty).

:- chr_constraint
    constraint_sig(any, list(ty)),
    function_sig(any, sig_t(list(ty), ty)),
    function_sigs(any, list(sig_t(list(ty), ty))),
    function_bounds(any, list(bound_named)),
    constraint_bounds(any, list(bound_named)),
    con_sig(any, sig_t(ty, list(ty))),
    check_constraint_use(any, list(ty), int),
    check_function_use(any, list(ty), ty, int),
    check_function_use_with_ambient(any, list(sig_t(list(ty), ty)), list(ty), ty, int),
    check_constructor_use(any, list(ty), ty, int),
    check_unify(ty, ty, int),
    check_guard_bool(ty, int),
    check_guard_getarg(ty, ty, any, int, int),
    check_arg_list(list(ty), list(ty), int),
    tc_unify(ty, ty, int),
    tc_unify_list(list(ty), list(ty), int),
    resolve_overload(any, list(sig_t(list(ty), ty)), list(ty), ty, int),
    check_bound(any, list(ty), ty, int),
    discharge_bound_check(list(sig_t(list(ty), ty)), any, list(ty), ty, int),
    emit_bounds(list(bound_named), int),
    ambient_sig(int, any, sig_t(list(ty), ty)),
    active_scope(int),
    end_scope(int),
    report_error(int, any, any),
    errors(list(error)),
    collect(list(error)).

:- function (sig_fst(sig_t(A, B)) -> A), (sig_snd(sig_t(A, B)) -> B).
sig_fst(sig(X, _)) -> X.
sig_snd(sig(_, Y)) -> Y.

:- function
    (all_nonvar_list(list(any)) -> bool),
    (filter_consistent(list(sig_t(list(ty), ty)), list(ty)) -> list(sig_t(list(ty), ty))),
    (sig_args_consistent(list(ty), list(ty)) -> bool),
    (type_consistent(ty, ty) -> bool).

all_nonvar_list([]) -> true.
all_nonvar_list([X|_]) | var(X) -> false.
all_nonvar_list([_|Xs]) -> all_nonvar_list(Xs).

filter_consistent([], _) -> [].
filter_consistent([Sig|Rest], ArgTypes) | sig_args_consistent(sig_fst(Sig), ArgTypes) ->
    [Sig | filter_consistent(Rest, ArgTypes)].
filter_consistent([_|Rest], ArgTypes) -> filter_consistent(Rest, ArgTypes).

sig_args_consistent([], []) -> true.
sig_args_consistent([D|Ds], [A|As]) | type_consistent(D, A) -> sig_args_consistent(Ds, As).
sig_args_consistent(_, _) -> false.

type_consistent(_, A) | var(A) -> true.
type_consistent(any, _) -> true.
type_consistent(_, any) -> true.
type_consistent(X, X) -> true.
type_consistent(_, _) -> false.

% ==========================================================================
% Bounded polymorphism helpers (pure functions, no var binding)
% ==========================================================================

% Existential consistency: deep, non-binding consistency between two
% type-structures. Unlike `tc_unify` this never binds any variable,
% so it is safe to call from `check_bound`'s discharge guard when we
% need to know "does any candidate signature exist that is consistent
% with the substituted bound?" without modifying the surrounding
% solver state.
:- function
    (existential_consistent(ty, ty) -> bool),
    (existential_consistent_list(list(ty), list(ty)) -> bool),
    (sig_one_consistent(sig_t(list(ty), ty), list(ty), ty) -> bool),
    (sig_existential(list(sig_t(list(ty), ty)), list(ty), ty) -> bool).

existential_consistent(T, _) | var(T) -> true.
existential_consistent(_, T) | var(T) -> true.
existential_consistent(any, _) -> true.
existential_consistent(_, any) -> true.
existential_consistent(int, int) -> true.
existential_consistent(float, float) -> true.
existential_consistent(string, string) -> true.
% Same-rigid succeeds; different-rigid (rigid(N), rigid(M) with N≠M)
% falls through to the `(_, _) -> false` fallthrough below, so two
% distinct rigid identities are deliberately inconsistent. This is
% what makes the existence-check semantics in `discharge_bound_via_ambient`
% reject an ambient_sig that doesn't share the call site's rigid σ.
existential_consistent(rigid(N), rigid(N)) -> true.
existential_consistent(tcon(C, A1), tcon(C, A2)) -> existential_consistent_list(A1, A2).
existential_consistent(fun(A1, R1), fun(A2, R2))
    | existential_consistent_list(A1, A2) -> existential_consistent(R1, R2).
existential_consistent(_, _) -> false.

existential_consistent_list([], []) -> true.
existential_consistent_list([X|Xs], [Y|Ys])
    | existential_consistent(X, Y) -> existential_consistent_list(Xs, Ys).
existential_consistent_list(_, _) -> false.

% A single declared signature is consistent with the substituted bound
% when its argument list and return type are pairwise existentially
% consistent.
sig_one_consistent(sig(DeclArgs, DeclRet), SubArgs, SubRet)
    | existential_consistent_list(DeclArgs, SubArgs)
    -> existential_consistent(DeclRet, SubRet).
sig_one_consistent(_, _, _) -> false.

% True when at least one declared signature in the list is consistent
% with the substituted bound. Implements the existence semantics of
% `check_bound`: any matching candidate discharges the bound, without
% committing to a particular candidate.
sig_existential([], _, _) -> false.
sig_existential([Sig|_], SubArgs, SubRet)
    | sig_one_consistent(Sig, SubArgs, SubRet) -> true.
sig_existential([_|Rest], SubArgs, SubRet) -> sig_existential(Rest, SubArgs, SubRet).

% Ground-substitution check: true when every leaf of @SubArgs@ and
% @SubRet@ is a concrete type (no free type variable). When this is
% false the bound stays residual — per the gradual guarantee, a check
% that lacks the information to fail is not a failure.
:- function
    (sub_ground(list(ty), ty) -> bool),
    (ty_concrete(ty) -> bool),
    (ty_concrete_list(list(ty)) -> bool).

sub_ground(Args, Ret) | ty_concrete_list(Args) -> ty_concrete(Ret).
sub_ground(_, _) -> false.

ty_concrete(T) | var(T) -> false.
ty_concrete(any) -> true.
ty_concrete(int) -> true.
ty_concrete(float) -> true.
ty_concrete(string) -> true.
ty_concrete(tcon(_, Args)) -> ty_concrete_list(Args).
ty_concrete(fun(Args, Ret)) | ty_concrete_list(Args) -> ty_concrete(Ret).
% A rigid tvar is treated as concrete for the purpose of
% `sub_ground`. It is structurally ground (a fully-specified term)
% even though it stands for an abstract type — the gradual guarantee
% applies to /flexible/ unbound vars, not rigid identities. Without
% this, `check_bound` at a rigid σ would stay residual forever and
% the bound's discharge (`discharge_bound_via_ambient`) would never
% fire.
ty_concrete(rigid(_)) -> true.
ty_concrete(_) -> false.

ty_concrete_list([]) -> true.
ty_concrete_list([T|Rest]) | ty_concrete(T) -> ty_concrete_list(Rest).
ty_concrete_list(_) -> false.

% ==========================================================================
% Declaration matching
% ==========================================================================

% Bounded constraint usage: copy_term the declaration packed with its
% bounds so the bound's logical variables stay shared with the head
% arguments' types. After unifying the argument list, emit one
% `check_bound` per bound at the freshly-renamed substitution. This
% rule is listed before `constraint_match` so the more-specific
% three-head pattern is preferred when both rules match.
bounded_constraint_match @
    constraint_sig(Name, DeclTypes), constraint_bounds(Name, Bounds) \
        check_constraint_use(Name, ArgTypes, Ctx) <=>
    Fresh is copy_term(quote(sig(DeclTypes, Bounds))),
    FreshTypes is sig_fst(Fresh),
    FreshBounds is sig_snd(Fresh),
    check_arg_list(FreshTypes, ArgTypes, Ctx),
    emit_bounds(FreshBounds, Ctx).

% Constraint usage: copy_term the declaration, check args pairwise.
% The Haskell driver registers a constraint_sig for every constraint
% declared in the program (including untyped ones, which default to
% all-any), and the renamer rejects any rule referencing an undeclared
% constraint — so every check_constraint_use always has a matching
% constraint_sig.
constraint_match @
    constraint_sig(Name, DeclTypes) \
        check_constraint_use(Name, ArgTypes, Ctx) <=>
    FreshTypes is copy_term(quote(DeclTypes)),
    check_arg_list(FreshTypes, ArgTypes, Ctx).

% Bounded function usage: same shape as `function_match` plus a
% bound-discharge phase. Listed before `function_match` for the same
% reason `bounded_constraint_match` precedes `constraint_match`.
% Bounded functions are single-signature only (the spec restricts
% `requiring` to :- function / :- open_function, never :- class /
% :- open_class), so there is no bounded counterpart to
% `overloaded_function_match`.
bounded_function_match @
    function_sig(Name, Sig), function_bounds(Name, Bounds) \
        check_function_use(Name, ArgTypes, RetTypeVar, Ctx) <=>
    Fresh is copy_term(quote(sig(Sig, Bounds))),
    FreshSig is sig_fst(Fresh),
    FreshBounds is sig_snd(Fresh),
    FreshArgTypes is sig_fst(FreshSig),
    FreshRetType is sig_snd(FreshSig),
    check_arg_list(FreshArgTypes, ArgTypes, Ctx),
    tc_unify(RetTypeVar, FreshRetType, Ctx),
    emit_bounds(FreshBounds, Ctx).

% Function usage: copy_term preserves arg/ret sharing
function_match @
    function_sig(Name, Sig) \
        check_function_use(Name, ArgTypes, RetTypeVar, Ctx) <=>
    Fresh is copy_term(quote(Sig)),
    FreshArgTypes is sig_fst(Fresh),
    FreshRetType is sig_snd(Fresh),
    check_arg_list(FreshArgTypes, ArgTypes, Ctx),
    tc_unify(RetTypeVar, FreshRetType, Ctx).

% Overloaded function: filter matching sigs and resolve.
% filter_consistent treats var args as consistent with any declared type.
% If all args are vars, all sigs match → ambiguous → succeed silently.
% If some args are nonvar and narrow to one sig, that sig is applied.
% Unknown-function detection is short-circuited by the Haskell driver:
% 'typeOfCompound' checks the function-name set before emitting
% 'check_function_use', so this rule (and 'function_match') only fires
% for declared functions. Residual 'check_function_use' constraints
% from overloaded functions whose args never resolve are harmless —
% they represent genuinely polymorphic/ambiguous usage in gradual typing.
overloaded_function_match @
    function_sigs(Name, Sigs) \
        check_function_use(Name, ArgTypes, RetTypeVar, Ctx) <=>
    Matching is filter_consistent(Sigs, ArgTypes),
    resolve_overload(Name, Matching, ArgTypes, RetTypeVar, Ctx).

% ==========================================================================
% Bounded polymorphism: ambient signatures at call sites
% ==========================================================================
%
% Inside the equations of a bounded function (or the body/guard of a
% rule whose head mentions a bounded constraint), calls to the bound's
% named functions see the bound's required signature(s) as additional
% candidates alongside the function's ordinary declared signatures.
% The driver determines which calls qualify and emits
% `check_function_use_with_ambient(Name, AmbSigs, Args, Ret, Ctx)`
% (and the analogous body-tell form for bounded constraints) when the
% target name has at least one ambient signature in the surrounding
% scope. AmbSigs is the complete list of ambient signatures for that
% name across every currently active scope; the driver computes this
% list at call time so the rules below do not need to gather across
% stored ambient_sig constraints.

% With ambient + single declared sig: prepend ambients, treat as
% overload candidates.
check_with_ambient_single @
    function_sig(Name, DeclSig) \
        check_function_use_with_ambient(Name, AmbSigs, ArgTypes, RetTypeVar, Ctx) <=>
    AllSigs is append(AmbSigs, [DeclSig]),
    Matching is filter_consistent(AllSigs, ArgTypes),
    resolve_overload(Name, Matching, ArgTypes, RetTypeVar, Ctx).

% With ambient + overloaded declared sigs.
check_with_ambient_multi @
    function_sigs(Name, DeclSigs) \
        check_function_use_with_ambient(Name, AmbSigs, ArgTypes, RetTypeVar, Ctx) <=>
    AllSigs is append(AmbSigs, DeclSigs),
    Matching is filter_consistent(AllSigs, ArgTypes),
    resolve_overload(Name, Matching, ArgTypes, RetTypeVar, Ctx).

% No declared sig — the ambient sigs are the only candidates.
check_with_ambient_only @
    check_function_use_with_ambient(Name, AmbSigs, ArgTypes, RetTypeVar, Ctx) <=>
    Matching is filter_consistent(AmbSigs, ArgTypes),
    resolve_overload(Name, Matching, ArgTypes, RetTypeVar, Ctx).

% ==========================================================================
% Bounded polymorphism: bound emission and discharge
% ==========================================================================

% Walk a freshly-copy_term'd bounds list, emitting one residual
% `check_bound` constraint per entry. The bound's argument list and
% return type carry the call-site's fresh substitution (because the
% surrounding match rule copy_term'd them together with the function's
% signature), so the discharge rules see a substitution that is
% consistent with the call.
:- function
    (nbound_name(bound_named) -> any),
    (nbound_args(bound_named) -> list(ty)),
    (nbound_ret(bound_named) -> ty).
nbound_name(nbound(N, _, _)) -> N.
nbound_args(nbound(_, A, _)) -> A.
nbound_ret(nbound(_, _, R)) -> R.

emit_bounds_done @ emit_bounds([], _) <=> true.
emit_bounds_step @ emit_bounds([B | Rest], Ctx) <=>
    GName is nbound_name(B),
    BArgs is nbound_args(B),
    BRet is nbound_ret(B),
    check_bound(GName, BArgs, BRet, Ctx),
    emit_bounds(Rest, Ctx).

% `check_bound` is a residual: it stays in the store until the
% substitution becomes ground enough to either find a consistent
% declared signature (discharge silently) or rule them all out
% (`bound_unsatisfied`). The `sub_ground` guard implements the
% "ground enough" condition; partial substitutions leave the bound
% in place, matching the gradual-guarantee silent-success rule.
%
% Both the single-sig and overloaded-sig variants reuse
% `discharge_bound_check`, which is a worker constraint that
% sees a list of candidate signatures and runs an existence check.

% Per spec §Use-site checking step 4: "When this check happens during
% the equation checking of an enclosing bounded function, 'declared
% signature' includes the ambient signatures contributed by the
% enclosing function's bound." An ambient_sig that is consistent with
% the substituted bound discharges it silently — this is what keeps
% recursive uses of a bounded function polymorphic at the enclosing
% tvars, and what makes the equation-time bound check (emitted by the
% driver alongside the ambient sig in `emitAmbientAndBound`)
% trivially satisfy itself under rigid type variables.
%
% Listed before `discharge_bound_overloaded`/`discharge_bound_single`
% so an ambient match takes precedence; if no ambient_sig is
% consistent, those rules fall through to the declared-signature path.
%
% The `ambient_sig` head pattern intentionally ignores the scope id:
% any active ambient_sig with the matching name is a candidate. Stale
% ambients are removed by `end_scope` before any out-of-scope bound
% check can fire (each `check_bound` is emitted with a scope_id that
% gets torn down at the same end_scope call). The trivial-discharge
% property at function equation time relies on the fact that
% `emitAmbientAndBound` uses /one/ tvars map per call, so the
% ambient_sig and the check_bound it emits share rigid identity by
% construction.
discharge_bound_via_ambient @
    ambient_sig(_, GName, AmbSig) \ check_bound(GName, SubArgs, SubRet, Ctx) <=>
        sub_ground(SubArgs, SubRet),
        sig_one_consistent(AmbSig, SubArgs, SubRet) | true.

discharge_bound_overloaded @
    function_sigs(GName, DeclSigs) \ check_bound(GName, SubArgs, SubRet, Ctx) <=>
        sub_ground(SubArgs, SubRet) |
    discharge_bound_check(DeclSigs, GName, SubArgs, SubRet, Ctx).

discharge_bound_single @
    function_sig(GName, DeclSig) \ check_bound(GName, SubArgs, SubRet, Ctx) <=>
        sub_ground(SubArgs, SubRet) |
    discharge_bound_check([DeclSig], GName, SubArgs, SubRet, Ctx).

% No declared signature for the bound's named function. The
% Haskell-side `unknown_bound_function` check already rejects bounds
% whose target is not declared, so this rule is a defensive
% catch-all: with `sub_ground` true and no declared sig found
% (neither single nor overloaded), the bound cannot be satisfied.
discharge_bound_no_decl @
    check_bound(GName, SubArgs, SubRet, Ctx) <=>
        sub_ground(SubArgs, SubRet) |
    report_error(Ctx, bound_unsatisfied, GName).

% Existence check: discharge silently if any declared signature is
% consistent; otherwise emit `bound_unsatisfied`. Two rules with
% mutually exclusive guards; textual order picks the success case
% first when both could fire, matching the spec's "succeed if any
% candidate is consistent" semantics.
discharge_bound_check_ok @
    discharge_bound_check(Sigs, _, SubArgs, SubRet, _) <=>
        sig_existential(Sigs, SubArgs, SubRet) | true.

discharge_bound_check_fail @
    discharge_bound_check(_, GName, _, _, Ctx) <=>
    report_error(Ctx, bound_unsatisfied, GName).

% ==========================================================================
% Bounded polymorphism: scope teardown
% ==========================================================================
%
% When the driver finishes type-checking a bounded function's
% equation or a rule whose head mentions a bounded constraint, it
% tells `end_scope(S)`. These rules remove every `ambient_sig(S, _, _)`
% and the matching `active_scope(S)` so the scope's ambient
% signatures do not leak into subsequent equations or rules.
end_scope_ambient @
    end_scope(S) \ ambient_sig(S, _, _) <=> true.

end_scope_active @
    end_scope(S) \ active_scope(S) <=> true.

end_scope_done @
    end_scope(_) <=> true.

% Constructor usage: copy_term preserves parent/field sharing
constructor_match @
    con_sig(ConName, Sig) \
        check_constructor_use(ConName, ArgTypes, ResultTypeVar, Ctx) <=>
    Fresh is copy_term(quote(Sig)),
    FreshParent is sig_fst(Fresh),
    FreshFields is sig_snd(Fresh),
    check_arg_list(FreshFields, ArgTypes, Ctx),
    tc_unify(ResultTypeVar, FreshParent, Ctx).

% Defensive fallback: unknown constructor -> any. The Haskell driver
% (typeOfCompound, typeOfAtom, checkGuard's GuardMatch) gates
% check_constructor_use on the constructor being a known declaration,
% so this rule is unreachable in practice. It is kept (and routed
% through tc_unify rather than raw `=`) so a future driver path that
% emits check_constructor_use for an unknown constructor is sound when
% ResultTypeVar is already bound to a concrete type.
unknown_constructor @
    check_constructor_use(_, _, ResultTypeVar, Ctx) <=>
    tc_unify(ResultTypeVar, any, Ctx).

% ==========================================================================
% Argument list checking
% ==========================================================================

check_arg_cons @
    check_arg_list([D|Ds], [A|As], Ctx) <=>
    tc_unify(A, D, Ctx),
    check_arg_list(Ds, As, Ctx).

check_arg_nil @
    check_arg_list([], [], _) <=> true.

% Note: mismatched list lengths (one side exhausted before the other)
% are left unsolved rather than reported as errors. This can happen
% legitimately when a constraint or function is overloaded by arity:
% the declaration-matching rules match by name only, so a wrong-arity
% declaration may be tried first, leaving a residual check_arg_list
% that simply stays inert. The correct-arity declaration will match
% separately. Constructors, which cannot be overloaded by arity, have
% their arity checked driver-side by validateConstructorArities before
% the CHR session runs; wrong-arity constructor uses never reach
% check_constructor_use.

% ==========================================================================
% Delegation rules
% ==========================================================================

delegate_unify @
    check_unify(T1, T2, Ctx) <=> tc_unify(T1, T2, Ctx).

delegate_guard_bool @
    check_guard_bool(T, Ctx) <=>
    tc_unify(T, tcon(quote(prelude:bool), []), Ctx).

delegate_guard_getarg @
    con_sig(ConName, Sig) \
        check_guard_getarg(ResultType, TermType, ConName, FieldIndex, Ctx) <=>
    Fresh is copy_term(quote(Sig)),
    FreshParent is sig_fst(Fresh),
    FreshFields is sig_snd(Fresh),
    tc_unify(TermType, FreshParent, Ctx),
    FieldType is nth(FieldIndex, FreshFields),
    tc_unify(ResultType, FieldType, Ctx).

% Unknown constructor in guard getarg -> result is any. Routed through
% tc_unify so the rule is sound when ResultType is already bound to a
% non-`any` type from an earlier constraint (strict `=` would crash).
unknown_guard_getarg @
    check_guard_getarg(ResultType, _, _, _, _) <=>
    tc_unify(ResultType, any, 0).

% ==========================================================================
% tc_unify (type propagation and consistency)
% ==========================================================================

% --- any handling (must come first) ---

% (1) Nonvar any on left -> succeed, don't touch right side
tc_unify_any_left @
    tc_unify(T1, _, _) <=> nonvar(T1), T1 == any | true.

% (2) Both nonvar, any on right -> succeed
tc_unify_any_right @
    tc_unify(T1, T2, _) <=> nonvar(T1), nonvar(T2), T2 == any | true.

% (3) Var on left, any on right -> bind var to any
tc_unify_var_any @
    tc_unify(T1, T2, _) <=> var(T1), nonvar(T2), T2 == any | T1 = any.

% --- base types ---

tc_unify_int @
    tc_unify(int, int, _) <=> true.

tc_unify_float @
    tc_unify(float, float, _) <=> true.

tc_unify_string @
    tc_unify(string, string, _) <=> true.

% --- type constructors: same name, check args ---

tc_unify_tcon @
    tc_unify(tcon(C, Args1), tcon(C, Args2), Ctx) <=>
    tc_unify_list(Args1, Args2, Ctx).

% --- function types ---
%
% [C-Fun] requires the same parameter count on both sides. The guarded
% rule fires only when the argument lists have equal length and then
% checks the field types pairwise; the unguarded fallback fires on an
% arity mismatch and reports the two whole function types as
% inconsistent. Without the arity guard a mismatch would reach
% `tc_unify_list` with lists of unequal length, which matches no
% `tc_unify_list` rule and silently stays an inert residual.

:- function (same_arity(list(ty), list(ty)) -> bool).

same_arity([], []) -> true.
same_arity([_|Xs], [_|Ys]) -> same_arity(Xs, Ys).
same_arity(_, _) -> false.

tc_unify_fun @
    tc_unify(fun(A1, R1), fun(A2, R2), Ctx) <=>
    same_arity(A1, A2) |
    tc_unify_list(A1, A2, Ctx),
    tc_unify(R1, R2, Ctx).

tc_unify_fun_arity @
    tc_unify(fun(A1, R1), fun(A2, R2), Ctx) <=>
    report_error(Ctx, inconsistent, pair(fun(A1, R1), fun(A2, R2))).

% --- rigid type variables ---
%
% Same-rigid: succeed silently. Different-rigid or rigid-vs-concrete
% falls through to tc_unify_error and reports an inconsistency. A
% flexible var meeting a rigid is handled by the var rules below
% (the flex side binds to the rigid term).

tc_unify_rigid @
    tc_unify(rigid(N), rigid(N), _) <=> true.

% --- var rules ---

tc_unify_var_nonvar @
    tc_unify(T1, T2, _) <=> var(T1), nonvar(T2) | T1 = T2.

tc_unify_nonvar_var @
    tc_unify(T1, T2, _) <=> nonvar(T1), var(T2) | T2 = T1.

tc_unify_var_var @
    tc_unify(T1, T2, _) <=> var(T1), var(T2) | T1 = T2.

% --- fallback: inconsistency ---

tc_unify_error @
    tc_unify(T1, T2, Ctx) <=> nonvar(T1), nonvar(T2) |
    report_error(Ctx, inconsistent, pair(T1, T2)).

% ==========================================================================
% tc_unify_list
% ==========================================================================

tc_unify_list_nil @
    tc_unify_list([], [], _) <=> true.

tc_unify_list_cons @
    tc_unify_list([H1|T1], [H2|T2], Ctx) <=>
    tc_unify(H1, H2, Ctx),
    tc_unify_list(T1, T2, Ctx).

% ==========================================================================
% Overload resolution
% ==========================================================================

% Exactly one matching signature: apply it
resolve_one @
    resolve_overload(_, [Sig], ArgTypes, RetTypeVar, Ctx) <=>
    FreshArgs is sig_fst(Sig),
    FreshRet is sig_snd(Sig),
    check_arg_list(FreshArgs, ArgTypes, Ctx),
    tc_unify(RetTypeVar, FreshRet, Ctx).

% No matching signature: error. The function name is reported so the
% diagnostic can identify which call site failed; "no_matching_overload"
% with the literal name on the detail side keeps the decoder simple.
resolve_none @
    resolve_overload(Name, [], _, _, Ctx) <=>
    report_error(Ctx, no_matching_overload, Name).

% Multiple matching signatures: ambiguous, succeed silently
resolve_ambiguous @
    resolve_overload(_, [_, _ | _], _, _, _) <=> true.

% ==========================================================================
% Error accumulation
% ==========================================================================

accumulate_error @
    report_error(Ctx, Code, Detail), errors(Es) <=>
    errors([error(Ctx, Code, Detail) | Es]).

collect_errors @
    collect(E), errors(Es) <=> E = Es.