iter ct.1.1: validator scaffolding + Type::Con canonical-form rules
Adds BareCrossModuleTypeRef / BadCrossModuleTypeRef / QualifiedClassName to WorkspaceLoadError plus the validate_canonical_type_names function that enforces the canonical-form rule on every Type::Con name reachable from any def (including Term::Lam.param_tys / .ret_ty and Term::LetRec.ty). Term::Ctor.type_name and class-name fields land in Tasks 2 + 3; the validator is not yet wired into load_workspace (Task 6). Seven RED-first unit tests cover the cases enumerated in spec section Testing strategy plus a Lam-embedded-type smuggle-prevention test. main.rs gains diagnostic arms for the three new variants to keep the exhaustive match compiling.
This commit is contained in:
@@ -1153,6 +1153,55 @@ fn workspace_error_to_diagnostic(
|
||||
"module": name,
|
||||
})),
|
||||
),
|
||||
// ct.1 (canonical-type-names): bare `Type::Con` that does not
|
||||
// resolve to a primitive or a local TypeDef of the owning
|
||||
// module. `candidates` lists qualified suggestions scanned
|
||||
// from imports.
|
||||
W::BareCrossModuleTypeRef { module, name, candidates } => Some(
|
||||
ailang_check::Diagnostic::error(
|
||||
"bare-cross-module-type-ref",
|
||||
format!(
|
||||
"module `{module}` contains bare type name `{name}` that does not resolve to a local type; \
|
||||
candidates from imports: {candidates:?}"
|
||||
),
|
||||
)
|
||||
.with_ctx(serde_json::json!({
|
||||
"module": module,
|
||||
"name": name,
|
||||
"candidates": candidates,
|
||||
})),
|
||||
),
|
||||
// ct.1: qualified `<owner>.<type>` where `<owner>` is not a
|
||||
// known module or `<owner>` has no `TypeDef <type>`.
|
||||
W::BadCrossModuleTypeRef { module, name } => Some(
|
||||
ailang_check::Diagnostic::error(
|
||||
"bad-cross-module-type-ref",
|
||||
format!(
|
||||
"module `{module}` references qualified type `{name}` but the owner module is not known \
|
||||
or does not declare a type by that name"
|
||||
),
|
||||
)
|
||||
.with_ctx(serde_json::json!({
|
||||
"module": module,
|
||||
"name": name,
|
||||
})),
|
||||
),
|
||||
// ct.1: a class-reference field contains a `.` — class names
|
||||
// are not module-qualified in this milestone.
|
||||
W::QualifiedClassName { module, name, field } => Some(
|
||||
ailang_check::Diagnostic::error(
|
||||
"qualified-class-name",
|
||||
format!(
|
||||
"module `{module}` contains qualified class name `{name}` in field `{field}`; \
|
||||
class names are not module-qualified in this milestone"
|
||||
),
|
||||
)
|
||||
.with_ctx(serde_json::json!({
|
||||
"module": module,
|
||||
"name": name,
|
||||
"field": field,
|
||||
})),
|
||||
),
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -31,7 +31,7 @@
|
||||
//! # Ok::<(), ailang_core::workspace::WorkspaceLoadError>(())
|
||||
//! ```
|
||||
|
||||
use crate::ast::{ClassDef, Def, InstanceDef, Module, Type};
|
||||
use crate::ast::{ClassDef, Def, InstanceDef, Module, Term, Type};
|
||||
use crate::canonical;
|
||||
use crate::{load_module, Error as CoreError};
|
||||
use std::collections::{BTreeMap, BTreeSet, HashSet};
|
||||
@@ -289,6 +289,53 @@ pub enum WorkspaceLoadError {
|
||||
/// collide silently. Reject explicitly.
|
||||
#[error("module name {name:?} is reserved (auto-injected by the loader)")]
|
||||
ReservedModuleName { name: String },
|
||||
|
||||
/// ct.1 (canonical-type-names): a `Type::Con` whose `name` is
|
||||
/// neither a primitive nor a local TypeDef of the owning module
|
||||
/// was encountered. Under the canonical-form rule, bare =
|
||||
/// local; a bare cross-module ref is a schema violation.
|
||||
/// `candidates` lists the qualified forms found by scanning the
|
||||
/// owning module's imports in declaration order.
|
||||
#[error(
|
||||
"module `{module}` contains bare type name `{name}` that does not resolve to a local type. \
|
||||
AILang's `.ail.json` requires cross-module type references to be qualified. \
|
||||
Candidates from imports: {candidates:?}. Run `ail migrate-canonical-types` to fix legacy fixtures."
|
||||
)]
|
||||
BareCrossModuleTypeRef {
|
||||
module: String,
|
||||
name: String,
|
||||
candidates: Vec<String>,
|
||||
},
|
||||
|
||||
/// ct.1: a qualified `Type::Con` of the form `<owner>.<type>`
|
||||
/// was encountered, but `<owner>` is not a known module in the
|
||||
/// workspace, or `<owner>` is known but declares no TypeDef
|
||||
/// named `<type>`.
|
||||
#[error(
|
||||
"module `{module}` references qualified type `{name}` but the owner module is not known \
|
||||
or does not declare a type by that name"
|
||||
)]
|
||||
BadCrossModuleTypeRef {
|
||||
module: String,
|
||||
name: String,
|
||||
},
|
||||
|
||||
/// ct.1: a class-reference field (`InstanceDef.class`,
|
||||
/// `SuperclassRef.class`, `Constraint.class`, or
|
||||
/// `ClassDef.name`) contains a `.` — under this milestone class
|
||||
/// names are NOT module-qualified (see DESIGN spec §"Out of
|
||||
/// scope: Class names"). The schema rejects qualified forms so
|
||||
/// half-migrated files cannot silently load.
|
||||
#[error(
|
||||
"module `{module}` contains qualified class name `{name}` in field `{field}`. \
|
||||
Class names are not module-qualified in this milestone; \
|
||||
keep the bare form."
|
||||
)]
|
||||
QualifiedClassName {
|
||||
module: String,
|
||||
name: String,
|
||||
field: &'static str,
|
||||
},
|
||||
}
|
||||
|
||||
/// Hash over the canonical bytes of a complete module.
|
||||
@@ -718,6 +765,269 @@ fn walk_kind_mismatch(t: &Type, param: &str) -> Result<(), ()> {
|
||||
}
|
||||
}
|
||||
|
||||
/// ct.1: the five primitive type names that are always bare under
|
||||
/// the canonical-form rule. Kept in sync with `Type::int`,
|
||||
/// `Type::bool_`, `Type::str_`, `Type::unit`, `Type::float` in
|
||||
/// `crate::ast`.
|
||||
fn is_primitive_type_name(name: &str) -> bool {
|
||||
matches!(name, "Int" | "Bool" | "Str" | "Unit" | "Float")
|
||||
}
|
||||
|
||||
/// ct.1: enforce the canonical-form rule on every `Type::Con` and
|
||||
/// `Term::Ctor.type_name` reference in every loaded module. Runs
|
||||
/// after prelude injection and before class-schema validation, so a
|
||||
/// stale bare cross-module ref fires the canonical-form diagnostic
|
||||
/// rather than a downstream one.
|
||||
///
|
||||
/// Rule per spec §Architecture:
|
||||
/// 1. Qualified `<owner>.<type>`: `<owner>` must be a known module,
|
||||
/// `<type>` must be one of its TypeDefs. Else `BadCrossModuleTypeRef`.
|
||||
/// 2. Bare primitive (`Int`/`Bool`/`Str`/`Unit`/`Float`): accepted.
|
||||
/// 3. Bare non-primitive: must be a TypeDef in the owning module.
|
||||
/// Else `BareCrossModuleTypeRef` with `candidates` = qualified
|
||||
/// forms found by scanning the owning module's imports.
|
||||
pub(crate) fn validate_canonical_type_names(
|
||||
modules: &BTreeMap<String, Module>,
|
||||
) -> Result<(), WorkspaceLoadError> {
|
||||
// Pre-pass: for each module, build a `BTreeSet<String>` of local
|
||||
// TypeDef names. Used for both the owning-module local lookup
|
||||
// and the per-import owner lookup.
|
||||
let mut local_types: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
|
||||
for (mod_name, m) in modules {
|
||||
let mut s = BTreeSet::new();
|
||||
for def in &m.defs {
|
||||
if let Def::Type(t) = def {
|
||||
s.insert(t.name.clone());
|
||||
}
|
||||
}
|
||||
local_types.insert(mod_name.clone(), s);
|
||||
}
|
||||
|
||||
for (mod_name, m) in modules {
|
||||
// Imports in declaration order — used for both the
|
||||
// qualified-`<owner>` known-module check and the bare-non-primitive
|
||||
// candidates list.
|
||||
let import_names: Vec<&str> = m.imports.iter().map(|i| i.module.as_str()).collect();
|
||||
|
||||
// Walk every Type in this module's defs and check each Type::Con name.
|
||||
for def in &m.defs {
|
||||
walk_def_types(def, &mut |t: &Type| {
|
||||
if let Type::Con { name, .. } = t {
|
||||
check_type_con_name(
|
||||
name, mod_name, &local_types, &import_names,
|
||||
)?;
|
||||
}
|
||||
Ok(())
|
||||
})?;
|
||||
}
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
|
||||
/// ct.1: apply the canonical-form rule to one `Type::Con.name`
|
||||
/// (also reused for `Term::Ctor.type_name` in Task 2).
|
||||
fn check_type_con_name(
|
||||
name: &str,
|
||||
owning_module: &str,
|
||||
local_types: &BTreeMap<String, BTreeSet<String>>,
|
||||
import_names: &[&str],
|
||||
) -> Result<(), WorkspaceLoadError> {
|
||||
if let Some((prefix, suffix)) = name.split_once('.') {
|
||||
// Rule 1: qualified.
|
||||
let owner_types = local_types
|
||||
.get(prefix)
|
||||
.ok_or_else(|| WorkspaceLoadError::BadCrossModuleTypeRef {
|
||||
module: owning_module.to_string(),
|
||||
name: name.to_string(),
|
||||
})?;
|
||||
if !owner_types.contains(suffix) {
|
||||
return Err(WorkspaceLoadError::BadCrossModuleTypeRef {
|
||||
module: owning_module.to_string(),
|
||||
name: name.to_string(),
|
||||
});
|
||||
}
|
||||
return Ok(());
|
||||
}
|
||||
// Bare.
|
||||
if is_primitive_type_name(name) {
|
||||
return Ok(()); // Rule 2.
|
||||
}
|
||||
// Rule 3: must be local.
|
||||
if local_types
|
||||
.get(owning_module)
|
||||
.map(|s| s.contains(name))
|
||||
.unwrap_or(false)
|
||||
{
|
||||
return Ok(());
|
||||
}
|
||||
// Bare cross-module — collect candidates from imports in declaration order.
|
||||
// Prelude is implicit: scan it last as a fallback candidate (mirrors
|
||||
// iter 23.2.4's implicit-prelude behaviour in codegen).
|
||||
let mut candidates: Vec<String> = Vec::new();
|
||||
for imp in import_names {
|
||||
if local_types
|
||||
.get(*imp)
|
||||
.map(|s| s.contains(name))
|
||||
.unwrap_or(false)
|
||||
{
|
||||
candidates.push(format!("{imp}.{name}"));
|
||||
}
|
||||
}
|
||||
if !import_names.contains(&"prelude")
|
||||
&& local_types
|
||||
.get("prelude")
|
||||
.map(|s| s.contains(name))
|
||||
.unwrap_or(false)
|
||||
{
|
||||
candidates.push(format!("prelude.{name}"));
|
||||
}
|
||||
Err(WorkspaceLoadError::BareCrossModuleTypeRef {
|
||||
module: owning_module.to_string(),
|
||||
name: name.to_string(),
|
||||
candidates,
|
||||
})
|
||||
}
|
||||
|
||||
/// ct.1: walk every `Type` reachable from a single `Def`, calling
|
||||
/// `f` on each. Recurses into `Type::Fn.params/ret`, `Type::Con.args`,
|
||||
/// `Type::Forall.constraints/body`, plus the obvious top-level fields
|
||||
/// of each `Def` variant AND every Type annotation embedded in a Term
|
||||
/// (`Term::Lam.param_tys`, `Term::Lam.ret_ty`, `Term::LetRec.ty`) —
|
||||
/// because those are Type-position occurrences too. Term::Ctor name
|
||||
/// walking is a separate concern handled in Task 2 since that field
|
||||
/// is a `String`, not a `Type`.
|
||||
fn walk_def_types<F>(def: &Def, f: &mut F) -> Result<(), WorkspaceLoadError>
|
||||
where
|
||||
F: FnMut(&Type) -> Result<(), WorkspaceLoadError>,
|
||||
{
|
||||
match def {
|
||||
Def::Fn(fd) => {
|
||||
walk_type(&fd.ty, f)?;
|
||||
walk_term_embedded_types(&fd.body, f)
|
||||
}
|
||||
Def::Const(cd) => {
|
||||
walk_type(&cd.ty, f)?;
|
||||
walk_term_embedded_types(&cd.value, f)
|
||||
}
|
||||
Def::Type(td) => {
|
||||
for c in &td.ctors {
|
||||
for fty in &c.fields {
|
||||
walk_type(fty, f)?;
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
Def::Class(cd) => {
|
||||
for cm in &cd.methods {
|
||||
walk_type(&cm.ty, f)?;
|
||||
if let Some(body) = &cm.default {
|
||||
walk_term_embedded_types(body, f)?;
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
Def::Instance(id) => {
|
||||
walk_type(&id.type_, f)?;
|
||||
for im in &id.methods {
|
||||
walk_term_embedded_types(&im.body, f)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// ct.1: walk a `Term` and call `f` on every Type annotation embedded
|
||||
/// in it (Lam.param_tys, Lam.ret_ty, LetRec.ty). Recurses through
|
||||
/// every Term sub-position. Does NOT fire on `Term::Ctor.type_name`
|
||||
/// (that's a `String`, not a `Type`; handled by `walk_def_terms` in
|
||||
/// Task 2).
|
||||
fn walk_term_embedded_types<F>(t: &Term, f: &mut F) -> Result<(), WorkspaceLoadError>
|
||||
where
|
||||
F: FnMut(&Type) -> Result<(), WorkspaceLoadError>,
|
||||
{
|
||||
match t {
|
||||
Term::Lit { .. } | Term::Var { .. } => Ok(()),
|
||||
Term::App { callee, args, .. } => {
|
||||
walk_term_embedded_types(callee, f)?;
|
||||
for a in args { walk_term_embedded_types(a, f)?; }
|
||||
Ok(())
|
||||
}
|
||||
Term::Let { value, body, .. } => {
|
||||
walk_term_embedded_types(value, f)?;
|
||||
walk_term_embedded_types(body, f)
|
||||
}
|
||||
Term::LetRec { ty, body, in_term, .. } => {
|
||||
walk_type(ty, f)?;
|
||||
walk_term_embedded_types(body, f)?;
|
||||
walk_term_embedded_types(in_term, f)
|
||||
}
|
||||
Term::If { cond, then, else_ } => {
|
||||
walk_term_embedded_types(cond, f)?;
|
||||
walk_term_embedded_types(then, f)?;
|
||||
walk_term_embedded_types(else_, f)
|
||||
}
|
||||
Term::Do { args, .. } => {
|
||||
for a in args { walk_term_embedded_types(a, f)?; }
|
||||
Ok(())
|
||||
}
|
||||
Term::Ctor { args, .. } => {
|
||||
for a in args { walk_term_embedded_types(a, f)?; }
|
||||
Ok(())
|
||||
}
|
||||
Term::Match { scrutinee, arms } => {
|
||||
walk_term_embedded_types(scrutinee, f)?;
|
||||
for arm in arms {
|
||||
walk_term_embedded_types(&arm.body, f)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
Term::Lam { param_tys, ret_ty, body, .. } => {
|
||||
for pt in param_tys { walk_type(pt, f)?; }
|
||||
walk_type(ret_ty, f)?;
|
||||
walk_term_embedded_types(body, f)
|
||||
}
|
||||
Term::Seq { lhs, rhs } => {
|
||||
walk_term_embedded_types(lhs, f)?;
|
||||
walk_term_embedded_types(rhs, f)
|
||||
}
|
||||
Term::Clone { value } => walk_term_embedded_types(value, f),
|
||||
Term::ReuseAs { source, body } => {
|
||||
walk_term_embedded_types(source, f)?;
|
||||
walk_term_embedded_types(body, f)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// ct.1: recursive walk of a `Type`, calling `f` at every node.
|
||||
fn walk_type<F>(t: &Type, f: &mut F) -> Result<(), WorkspaceLoadError>
|
||||
where
|
||||
F: FnMut(&Type) -> Result<(), WorkspaceLoadError>,
|
||||
{
|
||||
f(t)?;
|
||||
match t {
|
||||
Type::Con { args, .. } => {
|
||||
for a in args {
|
||||
walk_type(a, f)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
Type::Fn { params, ret, .. } => {
|
||||
for p in params {
|
||||
walk_type(p, f)?;
|
||||
}
|
||||
walk_type(ret, f)
|
||||
}
|
||||
Type::Forall { body, constraints, .. } => {
|
||||
for c in constraints {
|
||||
walk_type(&c.type_, f)?;
|
||||
}
|
||||
walk_type(body, f)
|
||||
}
|
||||
Type::Var { .. } => Ok(()),
|
||||
}
|
||||
}
|
||||
|
||||
/// Iter 22b.1: extract the head-constructor name of a type, for the
|
||||
/// "where is this type defined" lookup and for diagnostic-message
|
||||
/// rendering.
|
||||
@@ -1386,4 +1696,193 @@ mod tests {
|
||||
other => panic!("expected MissingSuperclassInstance, got {other:?}"),
|
||||
}
|
||||
}
|
||||
|
||||
fn module_with_type_def(name: &str, type_name: &str) -> Module {
|
||||
serde_json::from_value(serde_json::json!({
|
||||
"schema": crate::SCHEMA,
|
||||
"name": name,
|
||||
"imports": [],
|
||||
"defs": [
|
||||
{ "kind": "type", "name": type_name, "ctors": [] }
|
||||
],
|
||||
})).unwrap()
|
||||
}
|
||||
|
||||
fn single_module_with_type_con(name: &str, type_con: &str) -> BTreeMap<String, Module> {
|
||||
let m: Module = serde_json::from_value(serde_json::json!({
|
||||
"schema": crate::SCHEMA,
|
||||
"name": name,
|
||||
"imports": [],
|
||||
"defs": [{
|
||||
"kind": "fn",
|
||||
"name": "f",
|
||||
"type": { "k": "fn", "params": [], "ret": { "k": "con", "name": type_con }, "effects": [] },
|
||||
"params": [],
|
||||
"body": { "t": "lit", "lit": { "kind": "unit" } }
|
||||
}],
|
||||
})).unwrap();
|
||||
let mut map = BTreeMap::new();
|
||||
map.insert(name.to_string(), m);
|
||||
map
|
||||
}
|
||||
|
||||
fn single_module_with_local_type_and_ref(name: &str, type_name: &str) -> BTreeMap<String, Module> {
|
||||
let m: Module = serde_json::from_value(serde_json::json!({
|
||||
"schema": crate::SCHEMA,
|
||||
"name": name,
|
||||
"imports": [],
|
||||
"defs": [
|
||||
{ "kind": "type", "name": type_name, "ctors": [] },
|
||||
{ "kind": "fn", "name": "f",
|
||||
"type": { "k": "fn", "params": [], "ret": { "k": "con", "name": type_name }, "effects": [] },
|
||||
"params": [],
|
||||
"body": { "t": "lit", "lit": { "kind": "unit" } } }
|
||||
],
|
||||
})).unwrap();
|
||||
let mut map = BTreeMap::new();
|
||||
map.insert(name.to_string(), m);
|
||||
map
|
||||
}
|
||||
|
||||
fn module_with_import_and_type_con(name: &str, import: &str, type_con: &str) -> Module {
|
||||
serde_json::from_value(serde_json::json!({
|
||||
"schema": crate::SCHEMA,
|
||||
"name": name,
|
||||
"imports": [{ "module": import }],
|
||||
"defs": [{
|
||||
"kind": "fn",
|
||||
"name": "f",
|
||||
"type": { "k": "fn", "params": [], "ret": { "k": "con", "name": type_con }, "effects": [] },
|
||||
"params": [],
|
||||
"body": { "t": "lit", "lit": { "kind": "unit" } }
|
||||
}],
|
||||
})).unwrap()
|
||||
}
|
||||
|
||||
/// ct.1: a `Type::Con` whose `name` is a primitive (`Int` / `Bool` /
|
||||
/// `Str` / `Unit` / `Float`) must be accepted bare. The five
|
||||
/// primitive names are the only legal bare-non-local Type::Con names
|
||||
/// under the canonical-form rule.
|
||||
#[test]
|
||||
fn ct1_validator_accepts_primitive_type_cons() {
|
||||
let modules = single_module_with_type_con("m", "Int");
|
||||
validate_canonical_type_names(&modules).expect("Int must be accepted");
|
||||
let modules = single_module_with_type_con("m", "Float");
|
||||
validate_canonical_type_names(&modules).expect("Float must be accepted");
|
||||
}
|
||||
|
||||
/// ct.1: a bare Type::Con whose `name` matches a local TypeDef in
|
||||
/// the same module must be accepted (the canonical-form rule: bare =
|
||||
/// local).
|
||||
#[test]
|
||||
fn ct1_validator_accepts_bare_local_type_con() {
|
||||
let modules = single_module_with_local_type_and_ref("m", "Foo");
|
||||
validate_canonical_type_names(&modules)
|
||||
.expect("local Foo must be accepted");
|
||||
}
|
||||
|
||||
/// ct.1: a bare Type::Con whose `name` is neither a primitive nor a
|
||||
/// local TypeDef must fire `BareCrossModuleTypeRef`. With no imports,
|
||||
/// the candidates list is empty.
|
||||
#[test]
|
||||
fn ct1_validator_rejects_bare_xmod_no_imports() {
|
||||
let modules = single_module_with_type_con("m", "Ordering");
|
||||
let err = validate_canonical_type_names(&modules)
|
||||
.expect_err("Ordering must be rejected");
|
||||
match err {
|
||||
WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => {
|
||||
assert_eq!(module, "m");
|
||||
assert_eq!(name, "Ordering");
|
||||
assert!(candidates.is_empty(),
|
||||
"no imports => no candidates; got {candidates:?}");
|
||||
}
|
||||
other => panic!("expected BareCrossModuleTypeRef, got {other:?}"),
|
||||
}
|
||||
}
|
||||
|
||||
/// ct.1: a bare Type::Con whose `name` resolves to one imported
|
||||
/// module's TypeDef must fire `BareCrossModuleTypeRef` with that
|
||||
/// qualified form in `candidates` (so the diagnostic can suggest the
|
||||
/// fix).
|
||||
#[test]
|
||||
fn ct1_validator_rejects_bare_xmod_with_import_candidate() {
|
||||
let mut modules = BTreeMap::new();
|
||||
modules.insert("other".to_string(), module_with_type_def("other", "Ordering"));
|
||||
modules.insert("m".to_string(), module_with_import_and_type_con("m", "other", "Ordering"));
|
||||
let err = validate_canonical_type_names(&modules)
|
||||
.expect_err("Ordering must be rejected with candidate");
|
||||
match err {
|
||||
WorkspaceLoadError::BareCrossModuleTypeRef { name, candidates, .. } => {
|
||||
assert_eq!(name, "Ordering");
|
||||
assert_eq!(candidates, vec!["other.Ordering".to_string()]);
|
||||
}
|
||||
other => panic!("expected BareCrossModuleTypeRef, got {other:?}"),
|
||||
}
|
||||
}
|
||||
|
||||
/// ct.1: a qualified Type::Con `<owner>.<type>` where `<owner>` is a
|
||||
/// known module AND `<type>` is one of its TypeDefs must be accepted.
|
||||
#[test]
|
||||
fn ct1_validator_accepts_qualified_xmod_ref() {
|
||||
let mut modules = BTreeMap::new();
|
||||
modules.insert("other".to_string(), module_with_type_def("other", "Ordering"));
|
||||
modules.insert("m".to_string(), module_with_import_and_type_con("m", "other", "other.Ordering"));
|
||||
validate_canonical_type_names(&modules)
|
||||
.expect("other.Ordering must be accepted");
|
||||
}
|
||||
|
||||
/// ct.1: a qualified Type::Con `<owner>.<type>` where `<owner>` is
|
||||
/// NOT a known module must fire `BadCrossModuleTypeRef`. Symmetric
|
||||
/// case: `<owner>` known but no TypeDef `<type>` in it.
|
||||
#[test]
|
||||
fn ct1_validator_rejects_bad_qualified_ref() {
|
||||
let modules = single_module_with_type_con("m", "Mystery.Type");
|
||||
let err = validate_canonical_type_names(&modules)
|
||||
.expect_err("Mystery.Type must be rejected");
|
||||
match err {
|
||||
WorkspaceLoadError::BadCrossModuleTypeRef { module, name } => {
|
||||
assert_eq!(module, "m");
|
||||
assert_eq!(name, "Mystery.Type");
|
||||
}
|
||||
other => panic!("expected BadCrossModuleTypeRef, got {other:?}"),
|
||||
}
|
||||
}
|
||||
|
||||
/// ct.1: a Type::Con embedded inside a `Term::Lam.param_tys` is a
|
||||
/// Type-position occurrence, just inside a Term tree. The validator
|
||||
/// must walk into Lam-internal types so an LLM author can't smuggle
|
||||
/// a bare cross-module ref past it by hiding it in a lambda
|
||||
/// annotation.
|
||||
#[test]
|
||||
fn ct1_validator_walks_lam_embedded_types() {
|
||||
let m: Module = serde_json::from_value(serde_json::json!({
|
||||
"schema": crate::SCHEMA,
|
||||
"name": "m",
|
||||
"imports": [],
|
||||
"defs": [{
|
||||
"kind": "fn",
|
||||
"name": "f",
|
||||
"type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": [] },
|
||||
"params": [],
|
||||
"body": {
|
||||
"t": "lam",
|
||||
"params": ["x"],
|
||||
"paramTypes": [{ "k": "con", "name": "Ordering" }],
|
||||
"retType": { "k": "con", "name": "Unit" },
|
||||
"effects": [],
|
||||
"body": { "t": "lit", "lit": { "kind": "unit" } }
|
||||
}
|
||||
}],
|
||||
})).unwrap();
|
||||
let mut modules = BTreeMap::new();
|
||||
modules.insert("m".to_string(), m);
|
||||
let err = validate_canonical_type_names(&modules)
|
||||
.expect_err("Lam-embedded Ordering must be rejected");
|
||||
match err {
|
||||
WorkspaceLoadError::BareCrossModuleTypeRef { name, .. } => {
|
||||
assert_eq!(name, "Ordering");
|
||||
}
|
||||
other => panic!("expected BareCrossModuleTypeRef, got {other:?}"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user