iyi

Learn · step 5 of 8

Typed where it is written

A def that writes all of its types is typed at its definition, caller or no caller. A trait-restricted parameter is typed against exactly its bound, so a generic body cannot use what it did not declare.

What the rule says

R-2c Definition-site typing. A def whose parameters and return are all written is typed at its definition, caller or no caller — R-2's declared types stand in for the missing call. A trait-restricted parameter is typed too: the bound is written, and a bound is enough — the compiler synthesizes one witness type per simple trait, implements its abstract requirements as stubs, and types the body against exactly the bound, so a generic body cannot quietly use what it did not declare (the half duck-typed generics never check and Rust checks always). pub is not the condition: a module's unmarked function, a type's private def, a type the module never marked pub, and a method an impl block gives a type are typed at their definition too, since the probe is the definition asking about itself and R-2's wall is for callers. A script's top-level defs, class methods, an abstract class's methods and parameters (through its virtual type, as a caller's value arrives), a parameter with a default, an external name, a splat (one element) and a named-only parameter are all in reach. Each def is typed on its own, so every one that does not type is reported, not the first. Out of reach and stated: supertrait/generic/associated-type traits, block-taking and unannotated defs, operator-named defs, defs of a mixin module (whose self is the includer's), defs of a generic type and forall defs (no one type to probe with), an abstract class's class methods (self there is a subclass), a double splat, a parameter typed by a module, a metaclass or one of the library's abstract roots (Int, Number, Value), defs a macro writes, .cr sources. (Added with the agentic waves: a build, check, and the LSP may not disagree about what "clean" means. Mechanism: semantic/definition_typing.cr, probes from resolved signatures under if false, anchored at the def. First catch: this spec's own gate fixture — a signature edited to Int64 over a body still returning Int32.)R-2c SPEC.md, line 39

Run it

This step is grounded in samples/iyi/collections.iyi, 128 lines in the repository, read out of the tree when this page is built.

Run it in your browser from the module the compiler built for it.

Step two asked an exported name to write its types down, and spent that writing on the consumer: the artifact is enough because the declaration is complete. This step spends the same writing a second time, on the module that wrote it.

If a declaration says everything, then nothing is missing when the body is checked either. A call was only ever standing in for the types, and the types are on the page.

What lazy typing let through#

Crystal types a def when somebody calls it. iyi inherited that, and here is the shape of the problem, from the scanner inside the three module calculator.

samples/iyi/calc/lexer.iyilines 28 to 28
pub def scan(source : String) : Array(Token) | BadCharacter

Nothing in that file calls scan. Its callers are the parser and the driver, in other modules, which is the ordinary shape of a library. So compiling calc/lexer on its own used to type the signature and skip the body under it, and report a clean build about code it never visited. Ask a different question, run iyi check, open the file in an editor, and you could get a different answer, because each one visited a different set of bodies.

R-2c is the rule that closes it: a def whose parameters and return are all written is typed at its definition. The declared types stand in for the missing call, which is why this is a dividend of step two rather than a new tax. What a module exports it had to write down anyway.

A bound is enough#

The interesting half is the parameter whose type is a trait.

A def taking a trait is generic: the body will run on types that do not exist yet, and there is no call to learn them from. Duck typed generics answer by never checking, and finding out in whichever caller compiled first. Rust answers by checking always, against the bound.

iyi answers the way Rust does: for each trait-restricted parameter it synthesizes one witness type, implements the trait's abstract requirements with stub bodies, and types the body against the witness. So the body is checked against exactly what the signature declared, and against nothing the program happens to contain.

That is why the rejection at the foot of this page names a type nobody wrote.

Limits#

The rule states its own limits, and this step's program is one of them.

samples/iyi/collections.iyilines 108 to 110
def describe(e : Enumerable) : String
  "#{e.size} items"
end

That signature is fully written and it is still typed per call, because Enumerable answers an associated type and a witness for one of those is not built. Supertrait and generic traits are out for the same reason, along with block taking defs, defs that annotate nothing, and .cr sources. Each of those is written into the premise above rather than discovered later.

The sample this step is grounded in is what that limit costs, and it says so in its own header: a default method is only typed when it is called, so a trait that merely compiles has proved nothing about its bodies.

samples/iyi/collections.iyilines 5 to 12
# `std/enumerable.iyi` holds the trait. This file implements it twice and calls
# every method it defines. Both matter: a default method is only typed when it
# is called, so a trait that merely compiles has proved nothing about whether
# its bodies are sound.
#
# `Nums` and `Words` answer `Elem` differently — `Int32` and `String` — and each
# gets the same 57 default methods from one `each`. That is the claim II.6
# makes, running.

That is why the file calls every method Enumerable defines. It is a test standing in for a rule, which is exactly the position every fully declared def in the tree was in before this rule existed.

Reach outside the bound#

The clearest way to see a body typed with no caller is to write one that cannot be typed, and give it nothing to be called from. The program below defines a trait with one requirement, a type that implements it, and a function that asks the bound for a method the bound never declared. The type in the file happens to have that method. Nothing calls the function at all.

Break it

a body typed at its definition, reaching outside its bound

records/break/r2c_outside_bound.iyi40 lines
# Breaks R-2c: a def whose parameters and return are all written is typed at
# its definition, caller or no caller, and a trait-restricted parameter is
# typed against exactly its bound. Two halves of the rule fail here at once.
#
# Nothing in this file calls `loudest`, so under the lazy typing iyi inherited
# from Crystal its body would never be visited and the build would report
# itself clean. And `User`, the only implementer of `Greet` in the program, has
# a `shout` of its own: duck-typed generics would have found it and compiled.
# `Greet` declares `greet` and nothing else, so the body reaches outside the
# bound it wrote down, and the message names the witness type the compiler
# synthesized to type it (SPEC.md R-2c;
# src/compiler/iyi/semantic/definition_typing.cr).
module diagnostics/r2c_outside_bound

pub trait Greet
  abstract def greet : String
end

pub struct User
  getter name : String

  def initialize(@name : String)
  end

  # Present on the concrete type, and irrelevant to the def below: the bound is
  # what that body is typed against, not whatever happens to implement it.
  def shout : String
    "HELLO"
  end
end

impl Greet for User
  def greet : String
    "Hello, #{name}."
  end
end

pub def loudest(g : Greet) : String
  g.shout
end
$ IYI_PATH=<iyi>/src iyi build --no-codegen --no-color records/break/r2c_outside_bound.iyi
Showing last frame. Use --error-trace for full trace.

In records/break/r2c_outside_bound.iyi:39:5

 39 | g.shout
        ^----
Error: undefined method 'shout' for IyiDefTypeWitness_Diagnostics_R2cOutsideBound_Greet
R-2cDefinition-site typing. A def whose parameters and return are all written is typed at its definition, caller or no caller — R-2's declared types stand in for the missing call. A trait-restricted parameter is typed too: the bound is written, and a bound is enough — the compiler synthesizes one witness type per simple trait, implements its abstract requirements as stubs, and types the body against exactly the bound, so a generic body cannot quietly use what it did not declare (the half duck-typed generics never check and Rust checks always). pub is not the condition: a module's unmarked function, a type's private def, a type the module never marked pub, and a method an impl block gives a type are typed at their definition too, since the probe is the definition asking about itself and R-2's wall is for callers. A script's top-level defs, class methods, an abstract class's methods and parameters (through its virtual type, as a caller's value arrives), a parameter with a default, an external name, a splat (one element) and a named-only parameter are all in reach. Each def is typed on its own, so every one that does not type is reported, not the first. Out of reach and stated: supertrait/generic/associated-type traits, block-taking and unannotated defs, operator-named defs, defs of a mixin module (whose self is the includer's), defs of a generic type and forall defs (no one type to probe with), an abstract class's class methods (self there is a subclass), a double splat, a parameter typed by a module, a metaclass or one of the library's abstract roots (Int, Number, Value), defs a macro writes, .cr sources. (Added with the agentic waves: a build, check, and the LSP may not disagree about what "clean" means. Mechanism: semantic/definition_typing.cr, probes from resolved signatures under if false, anchored at the def. First catch: this spec's own gate fixture — a signature edited to Int64 over a body still returning Int32.)SPEC.md, line 39. Recorded run, exit code 1, iyi 0.17.0 (built on Crystal 1.22.0-dev [fe3db8354] (2026-10-14)), commit fe3db8354f56. Regenerate with npm run record:diagnostics.

What the rule bought

A build, iyi check and every keystroke in the editor answer one question the same way, because a fully declared body is typed where it is written rather than once per caller, and a library whose functions nobody has called yet cannot report itself clean. A generic body is checked against the bound it wrote down instead of against whatever type turns up, which is the half duck typed generics never check and Rust checks always.

Standing on

src/compiler/iyi/semantic/definition_typing.cr
the pass, the witness type it synthesizes per simple trait, and a fence around each thing it may not reach, every one of them kept on record with the failure that earned it
samples/iyi/collections.iyi
the header's own sentence about a default method typed only when it is called, and why that file calls every method the trait defines
samples/iyi/calc/lexer.iyi
an exported signature whose callers all live in other modules
SPEC.md
R-2c, including its own list of limits