use lang::types {
  Attribute, Decl, Def, Identifier, InductConstructor, Inductive, Infix, Instance,
  InstanceKey, LocalScope, LocalVar, Module, ModulePath, ModuleRegistry, NamePath,
  NameRef, Param, QualifiedName, Scope, ScopeData, ScopeDef, ScopeError,
  ScopeInstance, Similar, Term, TypeConstraint, Visibility, binder_binder, many, named,
  package_private, param_many, priv_, pub_, sort_n, unnamed,
}
use lang::scope {
  LocalTypeBinding, add_constraint_dict_params, bind_term_vars, build_scope_from_decls,
  build_scope_from_modules, find_constraint_bound_carrier_any, infer_carrier_type,
  list_append, lookup_binding, mk, npath_eq, placeholder_carrier, resolve_def_in_scope_by_name,
  scope_data_add_def, scope_data_add_inductive, scope_data_add_instance,
  scope_data_empty, scope_find_inductive, scope_find_inductive_by_constructor,
  scope_find_local, scope_globals, scope_push_local, scope_resolve_instance,
  scope_resolve_name, term_to_slug,
}
use llvm::strmap {str_map_empty, str_map_insert}

// --- Build scope from empty decl_list ---

#[test]
def test_build_empty_scope : Bool :=
    let empty_id_list : List Identifier := List.empty in
    let empty_path : ModulePath := ModulePath.mp empty_id_list in
    let no_decls : List Decl := List.empty in
    let empty_scope : ScopeData := build_scope_from_decls empty_path no_decls in
    true

// --- Build scope with a def declaration ---

#[test]
def test_build_with_def : Bool :=
    let name : NamePath := NamePath.npath (List.cons (Identifier.id "add") List.empty) in
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let empty_constraints : List TypeConstraint := List.empty in
    let empty_attrs : List Attribute := List.empty in
    let def_decl : Def := Def.mk name Term.hole Term.hole empty_constraints empty_attrs Visibility.package_private List.empty in
    let decl_list : List Decl := List.cons (Decl.def_d def_decl) List.empty in
    let sd : ScopeData := build_scope_from_decls mod_path decl_list in
    true

// --- Build scope with an inductive declaration ---

#[test]
def test_build_with_inductive : Bool :=
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Bool") List.empty) in
    let empty_params : List Param := List.empty in
    let true_cn : InductConstructor := InductConstructor.mk
        (NamePath.npath (List.cons (Identifier.id "true") List.empty))
        empty_params (sort_n 1) in
    let false_cn : InductConstructor := InductConstructor.mk
        (NamePath.npath (List.cons (Identifier.id "false") List.empty))
        empty_params (sort_n 1) in
    let cns : List InductConstructor := List.cons true_cn (List.cons false_cn List.empty) in
    let empty_attrs : List Attribute := List.empty in
    let ind : Inductive := Inductive.mk type_name empty_params (sort_n 1) cns empty_attrs Visibility.package_private in
    let decl_list : List Decl := List.cons (Decl.inductive_d ind) List.empty in
    let sd : ScopeData := build_scope_from_decls mod_path decl_list in
    true

// --- scope_globals extracts ScopeData from Scope ---

#[test]
def test_scope_globals : Bool :=
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let sd : ScopeData := scope_data_empty in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let g : ScopeData := scope_globals s in
    true

// --- scope_find_inductive finds an inductive by name ---

#[test]
def test_scope_find_inductive_found : Bool :=
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Bool") List.empty) in
    let empty_params : List Param := List.empty in
    let true_cn : InductConstructor := InductConstructor.mk
        (NamePath.npath (List.cons (Identifier.id "true") List.empty))
        empty_params (sort_n 1) in
    let cns : List InductConstructor := List.cons true_cn List.empty in
    let empty_attrs : List Attribute := List.empty in
    let ind : Inductive := Inductive.mk type_name empty_params (sort_n 1) cns empty_attrs Visibility.package_private in
    // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use
    // std.map {}` doc comment) — built via `scope_data_add_inductive` on
    // top of `scope_data_empty` rather than a hand-written literal.
    let sd : ScopeData := scope_data_add_inductive scope_data_empty ind in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let result : Result ScopeError Inductive := scope_find_inductive type_name s in
    match result {
        ok found => true,
        err _ => false
    }

// --- scope_find_inductive returns error when not found ---

#[test]
def test_scope_find_inductive_not_found : Bool :=
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let lookup_name : NamePath := NamePath.npath (List.cons (Identifier.id "NoSuch") List.empty) in
    let sd : ScopeData := scope_data_empty in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let result : Result ScopeError Inductive := scope_find_inductive lookup_name s in
    match result {
        ok _ => false,
        err _ => true
    }

// --- scope_push_local creates a new LocalScope ---

#[test]
def test_scope_push_local : Bool :=
    let lv : LocalVar := {
        name := Identifier.id "x",
        typ := Term.hole,
        multiplicity := Multiplicity.many,
    } in
    let empty_parent : Option LocalScope := Option.none in
    let ls : LocalScope := {
        vars := List.empty,
        parent := empty_parent,
    } in
    let pushed : LocalScope := scope_push_local lv ls in
    true

// --- scope_find_local finds a variable in LocalScope ---

#[test]
def test_scope_find_local_found : Bool :=
    let lv : LocalVar := {
        name := Identifier.id "x",
        typ := sort_n 1,
        multiplicity := Multiplicity.many,
    } in
    let empty_parent : Option LocalScope := Option.none in
    let ls : LocalScope := {
        vars := List.cons lv List.empty,
        parent := empty_parent,
    } in
    let result : Option LocalVar := scope_find_local (Identifier.id "x") ls in
    match result {
        Option.some found => true,
        Option.none => false
    }

// --- scope_find_local searches parent chain ---

#[test]
def test_scope_find_local_parent : Bool :=
    let lv1 : LocalVar := {
        name := Identifier.id "x",
        typ := sort_n 1,
        multiplicity := Multiplicity.many,
    } in
    let lv2 : LocalVar := {
        name := Identifier.id "y",
        typ := sort_n 1,
        multiplicity := Multiplicity.many,
    } in
    let empty_parent : Option LocalScope := Option.none in
    let parent : LocalScope := {
        vars := List.cons lv1 List.empty,
        parent := empty_parent,
    } in
    let some_parent : Option LocalScope := Option.some parent in
    let child : LocalScope := {
        vars := List.cons lv2 List.empty,
        parent := some_parent,
    } in
    let result : Option LocalVar := scope_find_local (Identifier.id "x") child in
    match result {
        Option.some found => true,
        Option.none => false
    }

// --- scope_find_local returns none when not found ---

#[test]
def test_scope_find_local_not_found : Bool :=
    let empty_parent : Option LocalScope := Option.none in
    let ls : LocalScope := {
        vars := List.empty,
        parent := empty_parent,
    } in
    let result : Option LocalVar := scope_find_local (Identifier.id "x") ls in
    match result {
        Option.some _ => false,
        Option.none => true
    }

// --- scope_resolve_name finds a def in ScopeData ---

#[test]
def test_scope_resolve_name_found : Bool :=
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "add") List.empty) in
    let def_entry : ScopeDef := {
        name := def_name,
        module := mod_path,
        sig := Term.hole,
        body := Term.hole,
        vis := Visibility.package_private,
    } in
    // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use
    // std.map {}` doc comment) — built via `scope_data_add_def` on top of
    // `scope_data_empty` rather than a hand-written literal.
    let sd : ScopeData := scope_data_add_def scope_data_empty def_entry in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let nref : NameRef := NameRef.nnp def_name in
    let empty_parent : Option LocalScope := Option.none in
    let locals : LocalScope := {
        vars := List.empty,
        parent := empty_parent,
    } in
    let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in
    match result {
        ok found => true,
        err _ => false
    }

// --- scope_resolve_name returns error when not found ---

#[test]
def test_scope_resolve_name_not_found : Bool :=
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let sd : ScopeData := scope_data_empty in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let nref : NameRef := NameRef.nnp (NamePath.npath (List.cons (Identifier.id "no_such") List.empty)) in
    let empty_parent : Option LocalScope := Option.none in
    let locals : LocalScope := {
        vars := List.empty,
        parent := empty_parent,
    } in
    let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in
    match result {
        ok _ => false,
        err _ => true
    }

// --- Builtin Type resolves ---

#[test]
def test_builtin_type_resolves : Bool :=
    let empty_id_list : List Identifier := List.empty in
    let empty_path : ModulePath := ModulePath.mp empty_id_list in
    let no_decls : List Decl := List.empty in
    let sd : ScopeData := build_scope_from_decls empty_path no_decls in
    let s : Scope := {
        module_id := empty_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Type") List.empty) in
    let result : Result ScopeError ScopeDef := resolve_def_in_scope_by_name type_name s in
    match result {
        ok found => true,
        err _ => false
    }

// --- Builtin Type inductive is found ---

#[test]
def test_builtin_type_inductive : Bool :=
    let empty_id_list : List Identifier := List.empty in
    let empty_path : ModulePath := ModulePath.mp empty_id_list in
    let no_decls : List Decl := List.empty in
    let sd : ScopeData := build_scope_from_decls empty_path no_decls in
    let s : Scope := {
        module_id := empty_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Type") List.empty) in
    let result : Result ScopeError Inductive := scope_find_inductive type_name s in
    match result {
        ok found => true,
        err _ => false
    }

// --- build_scope_from_modules with empty modules ---

#[test]
def test_build_from_modules_empty : Bool :=
    let empty_id_list : List Identifier := List.empty in
    let empty_path : ModulePath := ModulePath.mp empty_id_list in
    let empty_modules : ModuleRegistry := {
        modules := List.empty,
    } in
    let sd : ScopeData := build_scope_from_modules empty_path empty_modules in
    true

// --- build_scope_from_modules with one module ---

#[test]
def test_build_from_modules_one_def : Bool :=
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "add") List.empty) in
    let def_entry : ScopeDef := {
        name := def_name,
        module := mod_path,
        sig := Term.hole,
        body := Term.hole,
        vis := Visibility.package_private,
    } in
    let empty_instances : List ScopeInstance := List.empty in
    let empty_infixes : List Infix := List.empty in
    let empty_inductives : List Inductive := List.empty in
    let defs : List ScopeDef := List.cons def_entry List.empty in
    let m : Module := {
        path := mod_path,
        inductives := empty_inductives,
        defs := defs,
        infixs := empty_infixes,
        instances := empty_instances,
    } in
    let loaded : ModuleRegistry := {
        modules := List.cons m List.empty,
    } in
    let sd : ScopeData := build_scope_from_modules mod_path loaded in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let nref : NameRef := NameRef.nnp def_name in
    let empty_parent : Option LocalScope := Option.none in
    let locals : LocalScope := {
        vars := List.empty,
        parent := empty_parent,
    } in
    let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in
    match result {
        ok found => true,
        err _ => false
    }

// --- priv visibility ---

/// `priv` is module-private: the declaring module sees it, no one else
/// does. Built as a pair of tests over the same two-module fixture so the
/// only difference between them is WHICH module is being scoped.
def priv_fixture (vis : Visibility) : ModuleRegistry :=
    let owner : ModulePath := ModulePath.mp [Identifier.id "Owner"] in
    let def_name : NamePath := NamePath.npath [Identifier.id "secret"] in
    let def_entry : ScopeDef := {
        name := def_name,
        module := owner,
        sig := Term.hole,
        body := Term.hole,
        vis := vis,
    } in
    let m : Module := {
        path := owner,
        inductives := ([] : List Inductive),
        defs := List.cons def_entry List.empty,
        infixs := ([] : List Infix),
        instances := ([] : List ScopeInstance),
    } in
    { modules := List.cons m List.empty }

def priv_fixture_resolves_from (vis : Visibility) (consumer : ModulePath) : Bool :=
    let sd : ScopeData := build_scope_from_modules consumer (priv_fixture vis) in
    let s : Scope := {
        module_id := consumer,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let locals : LocalScope := { vars := List.empty, parent := (Option.none : Option LocalScope) } in
    let nref : NameRef := NameRef.nnp (NamePath.npath [Identifier.id "secret"]) in
    match scope_resolve_name nref s locals {
        ok _ => true,
        err _ => false
    }

#[test]
def test_priv_def_is_visible_in_its_own_module : Bool :=
    priv_fixture_resolves_from Visibility.priv_ (ModulePath.mp [Identifier.id "Owner"])

#[test]
def test_priv_def_is_hidden_from_other_modules : Bool :=
    not (priv_fixture_resolves_from Visibility.priv_ (ModulePath.mp [Identifier.id "Other"]))

/// The default (package-private) still crosses module boundaries -- only
/// `priv` is enforced today, and the mote boundary is a later step.
#[test]
def test_package_private_def_still_crosses_modules : Bool :=
    priv_fixture_resolves_from Visibility.package_private (ModulePath.mp [Identifier.id "Other"])

#[test]
def test_pub_def_crosses_modules : Bool :=
    priv_fixture_resolves_from Visibility.pub_ (ModulePath.mp [Identifier.id "Other"])

// --- scope_resolve_instance found ---

#[test]
def test_scope_resolve_instance_found : Bool :=
    let cls_name : NamePath := NamePath.npath (List.cons (Identifier.id "Monad") List.empty) in
    let inst_name : Identifier := Identifier.id "maybeMonad" in
    let empty_constraints : List TypeConstraint := List.empty in
    let empty_args : List Term := List.empty in
    let ins : Instance := Instance.mk inst_name cls_name empty_constraints empty_args Visibility.package_private List.empty List.empty in
    // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use
    // std.map {}` doc comment) — built via `scope_data_add_instance` on
    // top of `scope_data_empty` rather than a hand-written literal.
    let sd : ScopeData := scope_data_add_instance scope_data_empty ins in
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let empty_params : List Param := List.empty in
    let key : InstanceKey := {
        cls := cls_name,
        constraints := empty_constraints,
        args := empty_params,
    } in
    let result : Result ScopeError Instance := scope_resolve_instance cls_name key s in
    match result {
        ok found => true,
        err _ => false
    }

// --- scope_resolve_instance not found ---

#[test]
def test_scope_resolve_instance_not_found : Bool :=
    let cls_name : NamePath := NamePath.npath (List.cons (Identifier.id "Monad") List.empty) in
    let sd : ScopeData := scope_data_empty in
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let empty_params : List Param := List.empty in
    let empty_constraints : List TypeConstraint := List.empty in
    let key : InstanceKey := {
        cls := cls_name,
        constraints := empty_constraints,
        args := empty_params,
    } in
    let result : Result ScopeError Instance := scope_resolve_instance cls_name key s in
    match result {
        ok _ => false,
        err _ => true
    }

// --- list_append appends two lists ---

#[test]
def test_list_append_empty : Bool :=
    let empty : List I64 := List.empty in
    let result : List I64 := list_append empty empty in
    true

// --- list_append with non-empty list ---

#[test]
def test_list_append_non_empty : Bool :=
    let xs : List I64 := List.cons (1 : I64) (List.cons (2 : I64) List.empty) in
    let ys : List I64 := List.cons (3 : I64) (List.cons (4 : I64) List.empty) in
    let result : List I64 := list_append xs ys in
    true

// --- scope_resolve_instance matches by class name ---

#[test]
def test_scope_resolve_instance_matches_class : Bool :=
    let cls_name1 : NamePath := NamePath.npath (List.cons (Identifier.id "Show") List.empty) in
    let cls_name2 : NamePath := NamePath.npath (List.cons (Identifier.id "Monad") List.empty) in
    let inst_show : Instance := Instance.mk (Identifier.id "showBool") cls_name1 List.empty List.empty Visibility.package_private List.empty List.empty in
    let inst_monad : Instance := Instance.mk (Identifier.id "maybeMonad") cls_name2 List.empty List.empty Visibility.package_private List.empty List.empty in
    // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use
    // std.map {}` doc comment) — built via `scope_data_add_instance` on
    // top of `scope_data_empty` rather than a hand-written literal.
    let sd : ScopeData := scope_data_add_instance (scope_data_add_instance scope_data_empty inst_show) inst_monad in
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let empty_params : List Param := List.empty in
    let key : InstanceKey := {
        cls := cls_name2,
        constraints := List.empty,
        args := empty_params,
    } in
    let result : Result ScopeError Instance := scope_resolve_instance cls_name2 key s in
    match result {
        ok ins =>
            match ins {
                mk name cls _ _ _ _ _ => Similar.similar name (Identifier.id "maybeMonad")
            },
        err _ => false
    }

// --- build_scope_from_decls resolves a def through scope_resolve_name ---

#[test]
def test_build_scope_then_resolve_def : Bool :=
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "add") List.empty) in
    let def_decl : Def := Def.mk def_name Term.hole Term.hole List.empty List.empty Visibility.package_private List.empty in
    let decl_list : List Decl := List.cons (Decl.def_d def_decl) List.empty in
    let sd : ScopeData := build_scope_from_decls mod_path decl_list in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let nref : NameRef := NameRef.nnp def_name in
    let empty_parent : Option LocalScope := Option.none in
    let locals : LocalScope := {
        vars := List.empty,
        parent := empty_parent,
    } in
    let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in
    match result {
        ok d => true,
        err _ => false
    }

// --- build_scope_from_decls resolves an inductive constructor ---

#[test]
def test_build_scope_then_resolve_constructor : Bool :=
    let mod_id : Identifier := Identifier.id "Test" in
    let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in
    let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Bool") List.empty) in
    let true_name : NamePath := NamePath.npath (List.cons (Identifier.id "true") List.empty) in
    let empty_params : List Param := List.empty in
    let true_cn : InductConstructor := InductConstructor.mk true_name empty_params (sort_n 1) in
    let cns : List InductConstructor := List.cons true_cn List.empty in
    let empty_attrs : List Attribute := List.empty in
    let ind : Inductive := Inductive.mk type_name empty_params (sort_n 1) cns empty_attrs Visibility.package_private in
    let decl_list : List Decl := List.cons (Decl.inductive_d ind) List.empty in
    let sd : ScopeData := build_scope_from_decls mod_path decl_list in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let nref : NameRef := NameRef.nnp true_name in
    let empty_parent : Option LocalScope := Option.none in
    let locals : LocalScope := {
        vars := List.empty,
        parent := empty_parent,
    } in
    let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in
    match result {
        ok d =>
            match d {
                mk name _ _ _ _ => Similar.similar name true_name
            },
        err _ => false
    }

// --- instance_key_matches compares type args ---

#[test]
def test_instance_key_matches_type_args : Bool :=
    let cls_name : NamePath := NamePath.npath (List.cons (Identifier.id "Show") List.empty) in
    let i64_typ : Term := sort_n 1 in
    let bool_typ : Term := sort_n 1 in
    let show_i64 : Instance := Instance.mk
        (Identifier.id "showI64")
        cls_name
        List.empty
        (List.cons i64_typ List.empty)
        Visibility.package_private List.empty List.empty in
    let show_bool : Instance := Instance.mk
        (Identifier.id "showBool")
        cls_name
        List.empty
        (List.cons bool_typ List.empty)
        Visibility.package_private List.empty List.empty in
    // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use
    // std.map {}` doc comment) — built via `scope_data_add_instance` on
    // top of `scope_data_empty` rather than a hand-written literal.
    // Insertion order reversed vs. the original hand-written list
    // (`show_bool` first, `show_i64` last) — `scope_data_add_instance`
    // prepends to its class's instance list, so this preserves the
    // original `[show_i64, show_bool]` order: `show_i64`/`show_bool`
    // here deliberately share the same level-1 sort arg (see above),
    // so `first_matching_instance`'s scan needs this exact order to
    // still return `show_i64` first, matching this test's intent.
    let sd : ScopeData := scope_data_add_instance (scope_data_add_instance scope_data_empty show_bool) show_i64 in
    let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "Test") List.empty) in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    // Key requesting Show I64 — should find show_i64 instance
    let key_i64 : InstanceKey := {
        cls := cls_name,
        constraints := List.empty,
        args := List.cons (param_many (Identifier.id "A") i64_typ) List.empty,
    } in
    match scope_resolve_instance cls_name key_i64 s {
        ok found =>
            match found {
                mk name _ _ _ _ _ _ => Similar.similar name (Identifier.id "showI64"),
            },
        err _ => false,
    }

#[test]
def test_instance_key_matches_wrong_type_args : Bool :=
    let cls_name : NamePath := NamePath.npath (List.cons (Identifier.id "Show") List.empty) in
    let i64_typ : Term := sort_n 1 in
    let string_typ : Term := sort_n 2 in  // different from type_1
    let show_i64 : Instance := Instance.mk
        (Identifier.id "showI64")
        cls_name
        List.empty
        (List.cons i64_typ List.empty)
        Visibility.package_private List.empty List.empty in
    // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use
    // std.map {}` doc comment) — built via `scope_data_add_instance` on
    // top of `scope_data_empty` rather than a hand-written literal.
    let sd : ScopeData := scope_data_add_instance scope_data_empty show_i64 in
    let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "Test") List.empty) in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    // Key requesting Show String — should NOT find show_i64
    let key_string : InstanceKey := {
        cls := cls_name,
        constraints := List.empty,
        args := List.cons (param_many (Identifier.id "A") string_typ) List.empty,
    } in
    match scope_resolve_instance cls_name key_string s {
        ok _ => false,
        err _ => true,
    }

// --- scope_find_inductive_by_constructor finds inductive by constructor name ---

#[test]
def test_find_inductive_by_constructor_found : Bool :=
    let ind_name : NamePath := NamePath.npath (List.cons (Identifier.id "Maybe") List.empty) in
    let some_np : NamePath := NamePath.npath (List.cons (Identifier.id "some") List.empty) in
    let none_np : NamePath := NamePath.npath (List.cons (Identifier.id "none") List.empty) in
    let some_cn : InductConstructor := InductConstructor.mk some_np List.empty (sort_n 1) in
    let none_cn : InductConstructor := InductConstructor.mk none_np List.empty (sort_n 1) in
    let cns : List InductConstructor := List.cons some_cn (List.cons none_cn List.empty) in
    let ind : Inductive := Inductive.mk ind_name List.empty (sort_n 1) cns List.empty Visibility.package_private in
    // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use
    // std.map {}` doc comment) — built via `scope_data_add_inductive` on
    // top of `scope_data_empty` rather than a hand-written literal.
    let sd : ScopeData := scope_data_add_inductive scope_data_empty ind in
    let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "Test") List.empty) in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    // Look up by "some" constructor — should find Maybe
    match scope_find_inductive_by_constructor some_np s {
        Option.some found =>
            match found {
                mk name _ _ _ _ _ => npath_eq name ind_name,
            },
        Option.none => false,
    }

#[test]
def test_find_inductive_by_constructor_not_found : Bool :=
    let ind_name : NamePath := NamePath.npath (List.cons (Identifier.id "Maybe") List.empty) in
    let some_np : NamePath := NamePath.npath (List.cons (Identifier.id "some") List.empty) in
    let some_cn : InductConstructor := InductConstructor.mk some_np List.empty (sort_n 1) in
    let ind : Inductive := Inductive.mk ind_name List.empty (sort_n 1) [some_cn] List.empty Visibility.package_private in
    // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use
    // std.map {}` doc comment) — built via `scope_data_add_inductive` on
    // top of `scope_data_empty` rather than a hand-written literal.
    let sd : ScopeData := scope_data_add_inductive scope_data_empty ind in
    let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "Test") List.empty) in
    let s : Scope := {
        module_id := mod_path,
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    // Look up by "nope" constructor — should NOT find
    let nope_np : NamePath := NamePath.npath (List.cons (Identifier.id "nope") List.empty) in
    match scope_find_inductive_by_constructor nope_np s {
        Option.some _ => false,
        Option.none => true,
    }

// --- dict-param placeholder regression (gap 7) ---

/// A constrained def whose body calls its own constraint's class method
/// (`Add.add a b` -- the `instance [Add A] HAdd A A A` -> `HAdd_A_A_A_add`
/// shape) qualifies for a leading dictionary parameter. That parameter's
/// own `typ` annotation MUST be `Term.hole` (which `type_check` always
/// succeeds on, returning `expected_type`), never a bound `Term.var 0`:
/// `check_def_with_scope` checks a def's body against `Term.hole`, so
/// `type_check_lam`'s non-`pi` branch re-checks each lambda's own written
/// param type against the current `local_types` stack -- and the
/// outermost dict lambda is checked with that stack EMPTY, so a
/// `Term.var 0` placeholder reported a spurious out-of-range `bound_var`
/// (the `HAdd_A_A_A_add` self-hosted-check gap). Mirrors the Rust
/// reference's own dictionary/projected-method placeholder
/// (`CoreTerm::Hole`, `core_check_module`).
#[test]
def test_dict_param_type_is_hole : Bool :=
    let add_cls : NamePath := NamePath.npath (List.cons (Identifier.id "Add") List.empty) in
    let constraint : TypeConstraint := TypeConstraint.mk add_cls (List.cons (Identifier.id "A") List.empty) in
    let constraints : List TypeConstraint := List.cons constraint List.empty in
    // The body's `Add.add` reference is what `qualifying_dict_constraints`
    // needs (`def_references_class` scans for a `var` whose name starts
    // with `"Add."`) to qualify the constraint for a leading dict param.
    let add_add_ref : Term := Term.var (-1) (DebugName.named (Identifier.id "Add.add")) in
    let body : Term := Term.app add_add_ref (Term.var (-1) (DebugName.named (Identifier.id "a"))) in
    let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "HAdd_A_A_A_add") List.empty) in
    let empty_attrs : List Attribute := List.empty in
    let df : Def := Def.mk def_name Term.hole body constraints empty_attrs Visibility.package_private List.empty in
    match add_constraint_dict_params df {
        Def.mk {typ := _new_typ, term := new_term, ..} =>
            match new_term {
                Term.lam _dbg param_typ _body =>
                    match param_typ { Term.hole => true, _ => false, },
                _ => false,
            },
    }

// --- Module-qualified references (`NameRef.nqn`) ---
//
// These are the first tests anywhere to exercise `nqn`. The parser builds
// one, but `lower_parse.mo` renders it to a flat `DebugName` string and
// every checker call site rebuilt it as a bare `nid` -- so
// `resolve_name_in_scope`'s `nqn` arm was unreachable and a qualified
// reference always reported `unknown variable`.

/// A `nqn` resolves by matching (module, name) as a PAIR: a def declared
/// bare (`process_id` in `std::process`) carries no prefix in its own
/// registered name, so the flattened-key lookup misses and the by-module
/// fallback is what has to answer.
#[test]
def test_scope_resolve_qualified_name : Bool :=
    let mod_path : ModulePath := ModulePath.mp
        (List.cons (Identifier.id "std") (List.cons (Identifier.id "process") List.empty)) in
    let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "process_id") List.empty) in
    let def_entry : ScopeDef := {
        name := def_name,
        module := mod_path,
        sig := Term.hole,
        body := Term.hole,
        vis := Visibility.package_private,
    } in
    let sd : ScopeData := scope_data_add_def scope_data_empty def_entry in
    let s : Scope := {
        module_id := ModulePath.mp (List.cons (Identifier.id "Main") List.empty),
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let qn : QualifiedName := { qmod := mod_path, qname := def_name } in
    let empty_parent : Option LocalScope := Option.none in
    let locals : LocalScope := { vars := List.empty, parent := empty_parent } in
    match scope_resolve_name (NameRef.nqn qn) s locals {
        ok found => true,
        err _ => false
    }

/// The MODULE half must be load-bearing: a qualified reference naming the
/// right def in the WRONG module must not resolve, or the qualifier is
/// decoration and a typo silently becomes a working reference.
#[test]
def test_scope_qualified_wrong_module_does_not_resolve : Bool :=
    let mod_path : ModulePath := ModulePath.mp
        (List.cons (Identifier.id "std") (List.cons (Identifier.id "process") List.empty)) in
    let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "process_id") List.empty) in
    let def_entry : ScopeDef := {
        name := def_name,
        module := mod_path,
        sig := Term.hole,
        body := Term.hole,
        vis := Visibility.package_private,
    } in
    let sd : ScopeData := scope_data_add_def scope_data_empty def_entry in
    let s : Scope := {
        module_id := ModulePath.mp (List.cons (Identifier.id "Main") List.empty),
        scope := sd,
        parent := Option.none,
        incomplete_match_ok := false,
    } in
    let wrong : ModulePath := ModulePath.mp
        (List.cons (Identifier.id "std") (List.cons (Identifier.id "nosuch") List.empty)) in
    let qn : QualifiedName := { qmod := wrong, qname := def_name } in
    let empty_parent : Option LocalScope := Option.none in
    let locals : LocalScope := { vars := List.empty, parent := empty_parent } in
    match scope_resolve_name (NameRef.nqn qn) s locals {
        ok _ => false,
        err _ => true
    }

// --- A placeholder is a WEAK carrier, never a dropped one ---
//
// `infer_carrier_type`'s `Term.var` arm reads a local's declared type out of
// the env. An un-annotated binding's desugared binder holds a placeholder --
// a hole, or the bare sort W1.1's lowering made of an un-annotated lambda
// parameter -- and a placeholder names no head -- so `term_matches_carrier`
// cannot fail against one and it matches EVERY instance, which makes it
// worse than useless whenever it outranks a real carrier.
//
// It is still handed on, because it is sometimes the ONLY evidence a call
// has. MEASURED: refusing it here (answering `Option.none` in that arm)
// turned `init/src/foldable_tests.mo`'s `Foldable.foldr (fn x acc => x + acc)
// 0 [] == 0` into `no instance found for `Foldable.foldr`` -- the
// un-annotated lambda's placeholder-typed binder is the only carrier
// candidate the empty `[]` leaves behind, so with it dropped nothing matched
// `instance Foldable List`. The PRECEDENCE problem is what
// `demote_uninformative_carriers` solves at the call sites, by moving a
// placeholder behind every real carrier instead of removing it -- see
// `placeholder_carrier`'s own doc comment in `lang/scope.mo`.

#[test]
def test_placeholder_carrier_sorts_and_holes : Bool :=
    placeholder_carrier (sort_n 1) && placeholder_carrier (sort_n 0) &&
    placeholder_carrier Term.hole

#[test]
def test_placeholder_carrier_named_types : Bool :=
    Bool.not (placeholder_carrier (Term.var 0 (DebugName.named (Identifier.id "I64")))) &&
    Bool.not (placeholder_carrier (Term.app (Term.var 0 (DebugName.named (Identifier.id "List"))) (Term.var 0 (DebugName.named (Identifier.id "I64")))))

/// The env an un-annotated `let` leaves behind, for one name.
def placeholder_env (nm : Identifier) (ty : Term) : List LocalTypeBinding :=
    List.cons (LocalTypeBinding.mk nm ty) List.empty

def local_var (nm : Identifier) : Term :=
    Term.var 0 (DebugName.named nm)

/// A placeholder-typed local is still OFFERED as a carrier -- dropping it
/// would lose the `Foldable.foldr ... []` resolution above.
#[test]
def test_placeholder_local_yields_a_carrier : Bool :=
    match infer_carrier_type (placeholder_env (Identifier.id "filtered") (sort_n 1)) List.empty str_map_empty List.empty (local_var (Identifier.id "filtered")) {
        Option.some _ => true,
        Option.none => false,
    }

/// Control: a local whose declared type names something still offers itself
/// as a carrier, with its arguments intact.
#[test]
def test_named_local_still_yields_a_carrier : Bool :=
    match infer_carrier_type (placeholder_env (Identifier.id "xs") (Term.var 0 (DebugName.named (Identifier.id "I64")))) List.empty str_map_empty List.empty (local_var (Identifier.id "xs")) {
        Option.some c => match c {
            Term.var _ dbg => match dbg {
                DebugName.named nm => Similar.similar nm (Identifier.id "I64"),
                DebugName.unnamed => false,
            },
            _ => false,
        },
        Option.none => false,
    }

// --- The constraint's own variable resolves at the BOUND carrier ---
//
// `resolve_ordinary_constrained_call` has no instance head of its own, so it
// passes `bindings = List.empty` to `constraint_carriers`, which then answers
// `[carrier]` -- the WHOLE carrier. Resolving `[BEq A]` at the whole carrier
// `List I64` re-matches `instance [BEq A] BEq (List A)`, and a dict name is
// mangled from the INSTANCE's declared args, so the element slot of a
// `List I64` comparison received `__Dict_BEq_List_A` and the driver read a
// raw `I64` in `monad_get_tag`. That is the B3 SIGSEGV in
// `std/src/list_tests3a.mo`. `find_constraint_bound_carrier_any` resolves the
// constraint at the carrier the matched instance's own head BINDS that
// variable to instead (`A := I64`, so `__Dict_BEq_I64`).

def var_named (nm : String) : Term := Term.var 0 (DebugName.named (Identifier.id nm))

def list_of (t : Term) : Term := Term.app (var_named "List") t

def only_instance (ins : Instance) : List Instance := List.cons ins List.empty

def beq_cls : NamePath :=
    NamePath.npath (List.cons (Identifier.id "BEq") List.empty)

/// `instance [BEq A] BEq (List A)`, in the shape the parser produces it.
def beq_list_instance : Instance :=
    Instance.mk (Identifier.id "BEq_List_A") beq_cls
        (List.cons (TypeConstraint.mk beq_cls (List.cons (Identifier.id "A") List.empty)) List.empty)
        (List.cons (list_of (var_named "A")) List.empty)
        Visibility.package_private
        [param_many (Identifier.id "A") (sort_n 1)]
        List.empty

/// `instance [Show A] Show A` -- a candidate that binds `A` back to `A` is
/// no progress at all, so nothing may be read from it.
def show_a_instance : Instance :=
    Instance.mk (Identifier.id "Show_A")
        (NamePath.npath (List.cons (Identifier.id "Show") List.empty))
        (List.cons (TypeConstraint.mk (NamePath.npath (List.cons (Identifier.id "Show") List.empty)) (List.cons (Identifier.id "A") List.empty)) List.empty)
        (List.cons (var_named "A") List.empty)
        Visibility.package_private
        [param_many (Identifier.id "A") (sort_n 1)]
        List.empty

def bound_carrier_slug (ins : Instance) (cls : NamePath) (vars : List Identifier) (c : Term) : String :=
    match find_constraint_bound_carrier_any (only_instance ins) cls vars (List.cons c List.empty) {
        Option.some p => match p {
            Pair.pair bound _matched => term_to_slug bound,
        },
        Option.none => "<none>",
    }

/// The measured B3 shape: `List I64` against `instance [BEq A] BEq (List A)`
/// binds `A := I64`, so the constraint resolves at `I64`, NOT at the whole
/// `List I64` that mentions it.
#[test]
def test_constraint_bound_carrier_is_the_bound_element : Bool :=
    String.beq (bound_carrier_slug beq_list_instance beq_cls (List.cons (Identifier.id "A") List.empty) (list_of (var_named "I64"))) "I64"

/// A candidate that binds the constraint's variable BACK to itself makes no
/// progress, so it is skipped rather than resolved at.
#[test]
def test_constraint_bound_carrier_skips_no_progress : Bool :=
    String.beq (bound_carrier_slug show_a_instance (NamePath.npath (List.cons (Identifier.id "Show") List.empty)) (List.cons (Identifier.id "A") List.empty) (var_named "A")) "<none>"

/// A candidate that matches no instance at all yields nothing.
#[test]
def test_constraint_bound_carrier_requires_a_match : Bool :=
    String.beq (bound_carrier_slug beq_list_instance beq_cls (List.cons (Identifier.id "A") List.empty) (var_named "I64")) "<none>"

/// ...and so does a constraint with no candidate to read from.
#[test]
def test_constraint_bound_carrier_needs_a_candidate : Bool :=
    match find_constraint_bound_carrier_any (only_instance beq_list_instance) beq_cls (List.cons (Identifier.id "A") List.empty) List.empty {
        Option.some _ => false,
        Option.none => true,
    }

// --- The def-type table is `forall`-wrapped, so a HEAD read off it must
// --- unquantify first.
//
// `collect_def_types` registers every def type `elaborate_def`-wrapped
// (`registered_def_type`), which is what gives the callee-signature
// channel the `Forall` binders it reads. The arm of `infer_carrier_type`
// that reads a bare HEAD off that same value (`type_head_name_local`) sees
// nothing in a `forall`, so it answered NO carrier where the raw type
// answered one. MEASURED: the promoted `FromListLiteral_List_empty` -- the
// callee that arm's own comment names as its load-bearing case -- left the
// enclosing `Foldable.foldr (fn x acc => x + acc) 0 []` with nothing to
// infer `Foldable`'s own carrier from, and it reported `no instance found`.
// The bare empty-list literal was the only casualty: an ascription, a typed
// `let`, `List.empty`, a non-empty literal and a bare `none` all take other
// arms.

/// The shape this table holds for a def that quantifies over its own
/// variable -- what `registered_def_type` guarantees.
def quantified_def_typ : Term :=
    Term.pi (binder_binder (Identifier.id "A")) Term.hole (list_of (var_named "A"))

/// The carrier `infer_carrier_type` reads off a 0-arg def REFERENCE
/// (`empty`, what `[]` desugars to), as a slug.
def def_ref_carrier_slug (typ : Term) : String :=
    match infer_carrier_type List.empty List.empty (str_map_insert "empty" typ str_map_empty) List.empty (var_named "empty") {
        Option.some c => term_to_slug c,
        Option.none => "<none>",
    }

#[test]
def test_def_ref_carrier_reads_through_a_quantified_type : Bool :=
    String.beq (def_ref_carrier_slug quantified_def_typ) "List"

#[test]
def test_def_ref_carrier_reads_a_bare_type_too : Bool :=
    String.beq (def_ref_carrier_slug (list_of (var_named "A"))) "List"

// --- bind_term_vars: an applied shape pairs with the applied carrier ---

/// `StateT I64 Id I64` fully applied -- the carrier the `instance [Monad
/// M] Monad (StateT S M)` call site in `init/src/transformers_tests.mo`
/// dispatches at.
def statet_applied : Term :=
    Term.app (Term.app (Term.app (var_named "StateT") (var_named "I64")) (var_named "Id")) (var_named "I64")

/// The same, asymmetric, so a pin can tell LEADING from TRAILING pairing:
/// the element type differs from the parameters'.
def statet_asym : Term :=
    Term.app (Term.app (Term.app (var_named "StateT") (var_named "I64")) (var_named "Id")) (var_named "U8")

/// The binding `bind_term_vars` records for `nm`, as a slug.
def bound_slug (wildcards : List Identifier) (shape : Term) (actual : Term) (nm : String) : String :=
    match lookup_binding (bind_term_vars wildcards shape actual List.empty) (Identifier.id nm) {
        Option.some t => term_to_slug t,
        Option.none => "<none>",
    }

/// MEASURED (`transformers_tests.mo`, driver exited -1): the instance's own
/// arg is a PARTIAL application of the carrier's head, so its variables
/// align with the carrier's FIRST args. Pairing the spines from the
/// outside bound `M := I64` (the ELEMENT type), which sent `[Monad M]`'s
/// dictionary lookup to `I64` -- where only prelude's wildcard-headed
/// bridge matches, so the promoted `StateT` method got the bridge's
/// dictionary and died on entry. `spine_matches` (the match side) was
/// already left-aligned; this is the binding side.
#[test]
def test_bind_term_vars_left_aligns_a_partial_application : Bool :=
    let shape := Term.app (Term.app (var_named "StateT") (var_named "S")) (var_named "M") in
    let wildcards : List Identifier := [Identifier.id "S", Identifier.id "M"] in
    String.beq (bound_slug wildcards shape statet_applied "S") "I64"
        && String.beq (bound_slug wildcards shape statet_applied "M") "Id"

/// A hole HEAD names a type constructor -- the carrier's head applied to
/// the params the shape's own arg does not name -- so its arg pairs with
/// the carrier's LAST. Both halves are pinned (the head loses `U8`, the
/// arg gains it), which is what a leading/trailing mix-up breaks.
#[test]
def test_bind_term_vars_binds_a_hole_head_to_the_carrier_prefix_and_its_arg_to_the_tail : Bool :=
    let shape := Term.app (var_named "M") (var_named "A") in
    let wildcards : List Identifier := [Identifier.id "M", Identifier.id "A"] in
    String.beq (bound_slug wildcards shape statet_asym "M") "StateT_I64_Id"
        && String.beq (bound_slug wildcards shape statet_asym "A") "U8"

/// The bridge's own shape: two hole args, one carrier param between them
/// and the head (`M I I` against `StateT I64 Id U8`). `I` is recorded
/// twice; the later record wins (`lookup_binding` scans the prepended
/// list front-first), so the pin's `U8` also says the pair ran to the end.
#[test]
def test_bind_term_vars_walks_a_hole_heads_args_along_the_carrier_tail : Bool :=
    let shape := Term.app (Term.app (var_named "M") (var_named "I")) (var_named "I") in
    let wildcards : List Identifier := [Identifier.id "M", Identifier.id "I"] in
    String.beq (bound_slug wildcards shape statet_asym "M") "StateT_I64"
        && String.beq (bound_slug wildcards shape statet_asym "I") "U8"

/// The equal-arity case is unchanged either way -- `instance [BEq A] BEq
/// (List A)` against `List I64`.
#[test]
def test_bind_term_vars_aligns_equal_arity_spines : Bool :=
    String.beq (bound_slug [Identifier.id "A"] (list_of (var_named "A")) (list_of (var_named "I64")) "A") "I64"