diff --git a/crates/ail/tests/typeclass_22b2.rs b/crates/ail/tests/typeclass_22b2.rs index 0d696e6..e864395 100644 --- a/crates/ail/tests/typeclass_22b2.rs +++ b/crates/ail/tests/typeclass_22b2.rs @@ -127,3 +127,45 @@ fn class_method_entry_carries_full_metadata() { ), } } + +/// Property protected: a polymorphic FnDef that calls a class method +/// (e.g. `show x` where `x: a`) but does not declare the matching class +/// constraint in its `Forall.constraints` MUST receive a +/// `missing-constraint` diagnostic. This is the principal soundness +/// guarantee of class-method calls inside polymorphic functions: every +/// dispatch point at a polymorphic type must be backed by an in-scope +/// constraint that the caller will eventually have to satisfy. Without +/// this check, monomorphisation in 22b.3 would have no way to know +/// which dictionary to thread. +#[test] +fn fn_calling_class_method_without_declared_constraint_fires_missing_constraint() { + let entry = examples_dir().join("test_22b2_missing_constraint.ail.json"); + let ws = ailang_core::workspace::load_workspace(&entry) + .expect("workspace loads"); + let diagnostics = ailang_check::check_workspace(&ws); + assert!( + diagnostics.iter().any(|d| d.code == "missing-constraint"), + "expected missing-constraint; got: {:?}", + diagnostics.iter().map(|d| &d.code).collect::>() + ); +} + +/// Property protected: when a polymorphic FnDef declares the matching +/// class constraint in its `Forall.constraints`, the call to the class +/// method typechecks clean — the residual constraint produced at the +/// call site is satisfied by the in-scope declared constraint, and no +/// diagnostic fires. This is the positive counterpart to the +/// missing-constraint check: declaring `Show a =>` makes `show x` +/// well-formed inside the body. +#[test] +fn fn_with_correct_constraint_typechecks_green() { + let entry = examples_dir().join("test_22b2_constraint_declared.ail.json"); + let ws = ailang_core::workspace::load_workspace(&entry) + .expect("workspace loads"); + let diagnostics = ailang_check::check_workspace(&ws); + assert!( + diagnostics.is_empty(), + "expected no diagnostics; got: {:?}", + diagnostics + ); +} diff --git a/crates/ailang-check/src/diagnostic.rs b/crates/ailang-check/src/diagnostic.rs index 2d79964..906238b 100644 --- a/crates/ailang-check/src/diagnostic.rs +++ b/crates/ailang-check/src/diagnostic.rs @@ -62,6 +62,13 @@ //! the build refuses it. Note that an invalid suppression does NOT //! suppress its target diagnostic — the original still fires //! alongside this error. +//! - `missing-constraint` (Iter 22b.2) — `severity: error`. Emitted +//! by the per-fn typecheck arm when a polymorphic `FnDef` calls a +//! class method (e.g. `show x` where `x: a`) but its declared +//! `Forall.constraints` (after one-step superclass expansion) does +//! not include the residual class constraint. `ctx`: +//! `{"class": "", "method": "", "at_type": ""}`. Concrete- +//! type residuals are deferred to the `no-instance` diagnostic. use serde::Serialize; diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 20389ac..19da231 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -442,6 +442,28 @@ pub enum CheckError { /// can attach a `SuggestedRewrite` that drops the wrapper. #[error("reuse-as body must be an allocating term (Term::Ctor or Term::Lam), got {got}")] ReuseAsNonAllocatingBody { got: String, body_form_a: String }, + + /// Iter 22b.2 (Task 9): a polymorphic `FnDef` calls a class method + /// (e.g. `show x` where `x: a`), producing a residual class + /// constraint `(class, a)` at the call site, but the fn's declared + /// `Forall.constraints` does not list that constraint (and the + /// one-step superclass-expansion of the declared set still does + /// not cover it). Without an in-scope constraint, monomorphisation + /// (22b.3) would have no dictionary to thread, so this is a hard + /// soundness error. Code: `missing-constraint`. `ctx`: + /// `{"class": "", "method": "", "at_type": ""}`. + /// Concrete-type residuals (`Type::Con`) are deferred to Task 10's + /// `no-instance` diagnostic. + #[error( + "fn `{def}` calls class method `{method}` (class `{class}`) at type `{at_type}`, \ + but its declared constraints do not include `{class} {at_type}`" + )] + MissingConstraint { + def: String, + method: String, + class: String, + at_type: String, + }, } pub(crate) type Result = std::result::Result; @@ -480,6 +502,7 @@ impl CheckError { CheckError::TailCallNotInTailPosition => "tail-call-not-in-tail-position", CheckError::AmbiguousCtor { .. } => "ambiguous-ctor", CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body", + CheckError::MissingConstraint { .. } => "missing-constraint", } } @@ -520,6 +543,9 @@ impl CheckError { CheckError::ReuseAsNonAllocatingBody { got, .. } => { serde_json::json!({"got": got}) } + CheckError::MissingConstraint { class, method, at_type, .. } => { + serde_json::json!({"class": class, "method": method, "at_type": at_type}) + } _ => serde_json::Value::Object(serde_json::Map::new()), } } @@ -1100,6 +1126,31 @@ fn check_in_workspace( .collect(); env.module_types = build_module_types(ws); env.current_module = m.name.clone(); + // Iter 22b.2 (Task 9): merge per-module class-method tables into a + // single workspace-wide map for [`synth`]'s `Term::Var` arm. Method + // names are unique workspace-wide (enforced by + // `workspace::build_registry`'s method-name-collision check), so + // the merge has no overwrites. Also walk every module's + // `Def::Class` to build the one-step superclass expansion table. + let mut class_methods: BTreeMap = BTreeMap::new(); + for g in module_globals.values() { + for (n, e) in &g.class_methods { + class_methods.insert(n.clone(), e.clone()); + } + } + env.class_methods = class_methods; + let mut class_superclasses: BTreeMap> = BTreeMap::new(); + for module in ws.modules.values() { + for def in &module.defs { + if let Def::Class(cd) = def { + class_superclasses.insert( + cd.name.clone(), + cd.superclass.as_ref().map(|s| s.class.clone()), + ); + } + } + } + env.class_superclasses = class_superclasses; // Workspace isn't directly needed in the env; cross-module lookup uses // only `module_globals`. But we keep the ws reference in the // comment as a reminder, in case cross-module ADTs are added later. @@ -1270,7 +1321,12 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> { let mut effects = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; - let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter)?; + // Iter 22b.2 (Task 9): per-fn residual class constraints. Every + // call to a class method inside the body pushes a + // [`ResidualConstraint`] here; after the body finishes, we + // compare against the expanded declared set. + let mut residuals: Vec = Vec::new(); + let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals)?; unify(&ret_ty, &body_ty, &mut subst)?; // Iter 14e: tail-position verification (Decision 8). Runs after @@ -1284,9 +1340,106 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> { return Err(CheckError::UndeclaredEffect(e.clone())); } } + + // Iter 22b.2 (Task 9): missing-constraint check. Build the expanded + // declared-constraint set (declared + one-step superclass per + // Decision 11) and compare against residuals. Var-shaped residuals + // not covered by the expanded set fire `MissingConstraint`. Concrete + // residuals are deferred to Task 10's `no-instance` arm. + let declared_constraints: Vec = match &f.ty { + Type::Forall { constraints, .. } => constraints.clone(), + _ => Vec::new(), + }; + let expanded = expand_declared_constraints(&declared_constraints, &env.class_superclasses); + for r in &residuals { + let r_ty = subst.apply(&r.type_); + if let Type::Var { name } = &r_ty { + // Skip residuals over metavars (`$mN`) — those mean the + // residual is over a value the body never connected to a + // rigid var; treat as concrete-uncovered, which Task 10 + // will handle. Only rigid (source-level) vars participate + // in the missing-constraint check here. + if Subst::meta_id(name).is_some() { + continue; + } + let satisfied = expanded + .iter() + .any(|d| d.class == r.class && constraint_type_matches(&d.type_, &r_ty)); + if !satisfied { + return Err(CheckError::MissingConstraint { + def: f.name.clone(), + method: r.method.clone(), + class: r.class.clone(), + at_type: name.clone(), + }); + } + } + } Ok(()) } +/// Iter 22b.2 (Task 9): per-call-site residual class constraint +/// recorded by [`synth`] when a `Term::Var` resolves to a class method. +/// Carries the method name (for diagnostic rendering), the class, and +/// the type the class is applied to at the call site. The type is +/// typically a fresh metavar (which unification then ties to the +/// argument's actual type) or, after `subst.apply`, a rigid var or a +/// concrete `Type::Con`. +#[derive(Debug, Clone)] +pub(crate) struct ResidualConstraint { + /// Class name (e.g. `Show`). + pub class: String, + /// Class param's instance at this call site. Pre-substitution: the + /// fresh metavar inserted at the Var site. Post-substitution: the + /// solved type — rigid var, concrete con, or unsolved metavar. + pub type_: Type, + /// Method name (e.g. `show`); used by the missing-constraint + /// diagnostic to point the author at which call site triggered + /// the residual. + pub method: String, +} + +/// Iter 22b.2 (Task 9): expand a list of declared class constraints +/// with their one-step superclass closure (Decision 11). For every +/// declared `(C, t)`, append `(S, t)` if class `C` has a superclass +/// `S`. Only one step — Decision 11 forbids deeper chains. The +/// expanded list is what [`check_fn`] uses to decide whether a +/// residual is satisfied. +fn expand_declared_constraints( + declared: &[Constraint], + class_superclasses: &BTreeMap>, +) -> Vec { + let mut out: Vec = declared.to_vec(); + for c in declared { + if let Some(Some(sc)) = class_superclasses.get(&c.class) { + out.push(Constraint { + class: sc.clone(), + type_: c.type_.clone(), + }); + } + } + out +} + +/// Iter 22b.2 (Task 9): equality of constraint types for the +/// missing-constraint match. The residual type has been +/// `subst.apply`-d, so two rigid vars match iff their names are equal; +/// a `Type::Con` matches another `Type::Con` iff their head names and +/// args agree. Conservative: anything outside `Var` / `Con` is rejected +/// (the schema bounds Constraint.type_ to plain types, and Task 9 only +/// fires on Var residuals anyway). +fn constraint_type_matches(declared: &Type, residual: &Type) -> bool { + match (declared, residual) { + (Type::Var { name: a }, Type::Var { name: b }) => a == b, + (Type::Con { name: a, args: aa }, Type::Con { name: b, args: ba }) => { + a == b + && aa.len() == ba.len() + && aa.iter().zip(ba.iter()).all(|(x, y)| constraint_type_matches(x, y)) + } + _ => false, + } +} + /// Iter 14e: verifies that every `Term::App { tail: true, .. }` and /// `Term::Do { tail: true, .. }` actually sits in tail position, per /// Decision 8. @@ -1397,7 +1550,12 @@ fn check_const(c: &ConstDef, env: &Env) -> Result<()> { let mut effects = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; - let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter)?; + // Iter 22b.2 (Task 9): const bodies don't carry a `Forall.constraints` + // (rejected upstream), so any residual would have to be concrete — + // Task 10's no-instance arm will pick those up. We thread an + // accumulator only to keep `synth`'s signature uniform. + let mut residuals: Vec = Vec::new(); + let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals)?; unify(&c.ty, &v, &mut subst)?; if !effects.is_empty() { return Err(CheckError::ConstHasEffects( @@ -1416,6 +1574,7 @@ pub(crate) fn synth( in_def: &str, subst: &mut Subst, counter: &mut u32, + residuals: &mut Vec, ) -> Result { match t { Term::Lit { lit } => Ok(match lit { @@ -1425,15 +1584,37 @@ pub(crate) fn synth( Literal::Unit => Type::unit(), }), Term::Var { name } => { - // Lookup precedence: locals → local globals → qualified - // cross-module ref. A `Forall` resolved at any of these - // levels is instantiated with fresh metavars at the use - // site (textbook ML rule); rigid vars and concrete types - // pass through unchanged. + // Lookup precedence: locals → local globals → class-method + // table → qualified cross-module ref. A `Forall` resolved at + // any of these levels is instantiated with fresh metavars at + // the use site (textbook ML rule); rigid vars and concrete + // types pass through unchanged. + // + // Iter 22b.2 (Task 9): the class-method channel sits between + // local globals and qualified cross-module ref. When a name + // resolves through `env.class_methods`, we substitute the + // class param with a fresh metavar and record a residual + // class constraint — `check_fn` later compares the residual + // set against the declared `Forall.constraints`. let raw = if let Some(t) = locals.get(name) { t.clone() } else if let Some(t) = env.globals.get(name) { t.clone() + } else if let Some(cm) = env.class_methods.get(name) { + // Iter 22b.2 (Task 9): instantiate the class param with + // a fresh metavar; the body's unification at the call + // site fills it in, and the residual is the class + // constraint we owe at this use site. + let fresh = Subst::fresh(counter); + let mut mapping: BTreeMap = BTreeMap::new(); + mapping.insert(cm.class_param.clone(), fresh.clone()); + let inst_ty = substitute_rigids(&cm.method_ty, &mapping); + residuals.push(ResidualConstraint { + class: cm.class_name.clone(), + type_: fresh, + method: name.clone(), + }); + return Ok(inst_ty); } else if name.matches('.').count() == 1 { let (prefix, suffix) = name.split_once('.').expect("checked"); let target_module = match env.imports.get(prefix) { @@ -1472,7 +1653,7 @@ pub(crate) fn synth( Ok(maybe_instantiate(raw, counter)) } Term::App { callee, args, .. } => { - let cty = synth(callee, env, locals, effects, in_def, subst, counter)?; + let cty = synth(callee, env, locals, effects, in_def, subst, counter, residuals)?; let cty = subst.apply(&cty); let (params, ret, fx) = match &cty { Type::Fn { params, ret, effects: fx, .. } => { @@ -1508,7 +1689,7 @@ pub(crate) fn synth( }); } for (a, exp) in args.iter().zip(params.iter()) { - let actual = synth(a, env, locals, effects, in_def, subst, counter)?; + let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals)?; unify(exp, &actual, subst)?; } for e in fx { @@ -1517,9 +1698,9 @@ pub(crate) fn synth( Ok(subst.apply(&ret)) } Term::Let { name, value, body } => { - let v = synth(value, env, locals, effects, in_def, subst, counter)?; + let v = synth(value, env, locals, effects, in_def, subst, counter, residuals)?; let prev = locals.insert(name.clone(), v); - let r = synth(body, env, locals, effects, in_def, subst, counter)?; + let r = synth(body, env, locals, effects, in_def, subst, counter, residuals)?; match prev { Some(p) => { locals.insert(name.clone(), p); @@ -1531,10 +1712,10 @@ pub(crate) fn synth( Ok(r) } Term::If { cond, then, else_ } => { - let c = synth(cond, env, locals, effects, in_def, subst, counter)?; + let c = synth(cond, env, locals, effects, in_def, subst, counter, residuals)?; unify(&Type::bool_(), &c, subst)?; - let t1 = synth(then, env, locals, effects, in_def, subst, counter)?; - let t2 = synth(else_, env, locals, effects, in_def, subst, counter)?; + let t1 = synth(then, env, locals, effects, in_def, subst, counter, residuals)?; + let t2 = synth(else_, env, locals, effects, in_def, subst, counter, residuals)?; unify(&t1, &t2, subst)?; Ok(subst.apply(&t1)) } @@ -1552,7 +1733,7 @@ pub(crate) fn synth( }); } for (a, exp) in args.iter().zip(sig.params.iter()) { - let actual = synth(a, env, locals, effects, in_def, subst, counter)?; + let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals)?; unify(exp, &actual, subst)?; } effects.insert(sig.effect.clone()); @@ -1646,7 +1827,7 @@ pub(crate) fn synth( } for (a, exp) in args.iter().zip(qualified_fields.iter()) { let exp_inst = substitute_rigids(exp, &mapping); - let actual = synth(a, env, locals, effects, in_def, subst, counter)?; + let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals)?; unify(&exp_inst, &actual, subst)?; } Ok(Type::Con { @@ -1655,7 +1836,7 @@ pub(crate) fn synth( }) } Term::Match { scrutinee, arms } => { - let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter)?; + let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter, residuals)?; if arms.is_empty() { return Err(CheckError::NonExhaustive { ty: ailang_core::pretty::type_to_string(&s_ty), @@ -1673,7 +1854,7 @@ pub(crate) fn synth( let prev = locals.insert(n.clone(), t.clone()); pushed.push((n.clone(), prev)); } - let body_ty = synth(&arm.body, env, locals, effects, in_def, subst, counter)?; + let body_ty = synth(&arm.body, env, locals, effects, in_def, subst, counter, residuals)?; for (n, prev) in pushed.into_iter().rev() { match prev { Some(p) => { @@ -1748,9 +1929,9 @@ pub(crate) fn synth( Ok(subst.apply(&result_ty.expect("checked arms is non-empty"))) } Term::Seq { lhs, rhs } => { - let lty = synth(lhs, env, locals, effects, in_def, subst, counter)?; + let lty = synth(lhs, env, locals, effects, in_def, subst, counter, residuals)?; unify(&Type::unit(), <y, subst)?; - synth(rhs, env, locals, effects, in_def, subst, counter) + synth(rhs, env, locals, effects, in_def, subst, counter, residuals) } Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => { let mut pushed: Vec<(String, Option)> = Vec::new(); @@ -1759,7 +1940,7 @@ pub(crate) fn synth( pushed.push((n.clone(), prev)); } let mut body_effects: BTreeSet = BTreeSet::new(); - let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter); + let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals); for (n, prev) in pushed.into_iter().rev() { match prev { Some(p) => { @@ -1847,7 +2028,7 @@ pub(crate) fn synth( // subset rule against `declared_effs` — exactly like // `Term::Lam`. let mut body_effects: BTreeSet = BTreeSet::new(); - let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter); + let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals); // Restore body-scope locals (params + name). for (n, prev) in pushed.into_iter().rev() { @@ -1874,7 +2055,7 @@ pub(crate) fn synth( // scope (params are not visible here; only the recursive // binding is). let prev_in = locals.insert(name.clone(), ty.clone()); - let in_ty = synth(in_term, env, locals, effects, in_def, subst, counter); + let in_ty = synth(in_term, env, locals, effects, in_def, subst, counter, residuals); match prev_in { Some(p) => { locals.insert(name.clone(), p); @@ -1890,7 +2071,7 @@ pub(crate) fn synth( // No constraint generated, no environment change. The // wrapper records author intent for the future RC inc/dec // emission pass (18c.3); typing is pure passthrough. - synth(value, env, locals, effects, in_def, subst, counter) + synth(value, env, locals, effects, in_def, subst, counter, residuals) } Term::ReuseAs { source, body } => { // Iter 18d.1: `(reuse-as SRC NEW-CTOR)` requires `body` to @@ -1904,7 +2085,7 @@ pub(crate) fn synth( // shape-compatibility check (18d.2 will add a // `reuse-as-shape-mismatch` diagnostic when codegen has // the actual size info). - let _ = synth(source, env, locals, effects, in_def, subst, counter)?; + let _ = synth(source, env, locals, effects, in_def, subst, counter, residuals)?; match body.as_ref() { Term::Ctor { .. } | Term::Lam { .. } => {} other => { @@ -1930,7 +2111,7 @@ pub(crate) fn synth( } // Body's type is the result type of the whole reuse-as // expression. - synth(body, env, locals, effects, in_def, subst, counter) + synth(body, env, locals, effects, in_def, subst, counter, residuals) } } } @@ -2223,6 +2404,20 @@ pub struct Env { /// these names are legal as `Type::Var { name }` and unify only /// with themselves. pub rigid_vars: BTreeSet, + /// Iter 22b.2 (Task 9): workspace-wide class-method table. Merged + /// from every module's [`ModuleGlobals::class_methods`] so that a + /// `Term::Var { name: "show" }` in any module resolves to the + /// declaring class's [`ClassMethodEntry`]. Method-name uniqueness + /// is enforced earlier by `workspace::build_registry`'s + /// method-name-collision check (Iter 22b.2.6), so the merge is + /// safe (no overwrites). Read in [`synth`]'s `Term::Var` arm. + pub class_methods: BTreeMap, + /// Iter 22b.2 (Task 9): one-step superclass expansion table. + /// Maps each class name to its (optional) superclass class name. + /// Used by [`check_fn`] to expand `Forall.constraints` for the + /// missing-constraint check (Decision 11: max one step). The + /// schema permits at most one superclass per class. + pub class_superclasses: BTreeMap>, } /// Back-pointer from a ctor name to the ADT that declared it. Stored diff --git a/crates/ailang-check/src/lift.rs b/crates/ailang-check/src/lift.rs index 4dabba0..da26324 100644 --- a/crates/ailang-check/src/lift.rs +++ b/crates/ailang-check/src/lift.rs @@ -684,7 +684,14 @@ impl<'a> Lifter<'a> { let mut subst = Subst::default(); let mut counter: u32 = 0; let mut effects: BTreeSet = BTreeSet::new(); - let ty = synth(t, &self.env, locals, &mut effects, in_def, &mut subst, &mut counter)?; + // Iter 22b.2 (Task 9): the lift pass does its own type + // synthesis to figure out free-var types for letrec captures. + // Class-method residuals collected here are discarded — the + // missing-constraint check has already run for the enclosing + // fn during `check_fn`. Threading the accumulator only keeps + // `synth`'s signature uniform. + let mut residuals: Vec = Vec::new(); + let ty = synth(t, &self.env, locals, &mut effects, in_def, &mut subst, &mut counter, &mut residuals)?; Ok(subst.apply(&ty)) } } diff --git a/examples/test_22b2_constraint_declared.ail.json b/examples/test_22b2_constraint_declared.ail.json new file mode 100644 index 0000000..0d5ef8c --- /dev/null +++ b/examples/test_22b2_constraint_declared.ail.json @@ -0,0 +1,46 @@ +{ + "schema": "ailang/v0", + "name": "test_22b2_constraint_declared", + "imports": [], + "defs": [ + { + "kind": "class", + "name": "Show", + "param": "a", + "methods": [ + { + "name": "show", + "type": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Str" }, + "effects": [] + } + } + ] + }, + { + "kind": "fn", + "name": "describe", + "type": { + "k": "forall", + "vars": ["a"], + "constraints": [ + { "class": "Show", "type": { "k": "var", "name": "a" } } + ], + "body": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Str" }, + "effects": [] + } + }, + "params": ["x"], + "body": { + "t": "app", + "fn": { "t": "var", "name": "show" }, + "args": [{ "t": "var", "name": "x" }] + } + } + ] +} diff --git a/examples/test_22b2_missing_constraint.ail.json b/examples/test_22b2_missing_constraint.ail.json new file mode 100644 index 0000000..a5b4d12 --- /dev/null +++ b/examples/test_22b2_missing_constraint.ail.json @@ -0,0 +1,43 @@ +{ + "schema": "ailang/v0", + "name": "test_22b2_missing_constraint", + "imports": [], + "defs": [ + { + "kind": "class", + "name": "Show", + "param": "a", + "methods": [ + { + "name": "show", + "type": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Str" }, + "effects": [] + } + } + ] + }, + { + "kind": "fn", + "name": "describe", + "type": { + "k": "forall", + "vars": ["a"], + "body": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Str" }, + "effects": [] + } + }, + "params": ["x"], + "body": { + "t": "app", + "fn": { "t": "var", "name": "show" }, + "args": [{ "t": "var", "name": "x" }] + } + } + ] +}