playground evidence

# The other half of the cycle. `dep/loop_a` imports this module and this
# module imports `dep/loop_a`, which is the edge that closes it.
module dep/loop_b

import dep/loop_a

pub def b : String
  "b"
end

# Breaks R-2: only what a module marks `pub` is reachable from outside it, and
# `greeting` in `dep/greeter` carries no `pub`. Qualifying the call does not get
# around that. It has to be genuinely unreachable rather than merely left out
# of an import's names, because a `.iyimod` carries a module's exports and nothing
# else, so if another module could call an unmarked name that artifact would
# not be enough to compile against.
module diagnostics/r2_not_exported

import dep/greeter

puts Dep::Greeter.greeting

# Breaks R-2: everything a module exports carries full parameter and return
# types, because the signature is the whole of what a consumer reads. Drop the
# return type and there is nothing to write into the artifact, so the omission
# is refused where it is written rather than inferred from the body.
module diagnostics/r2_missing_return_type

pub def total(numbers : Array(Int32))
  numbers.sum
end

puts total([1, 2, 3])

# Breaks R-2 the other way: the type is written, and the body does not honour
# it. An exported signature is a promise to every consumer that reads the
# artifact instead of the body, so the body is the thing that has to give.
module diagnostics/r2_wrong_return_type

pub def total(numbers : Array(Int32)) : Int32
  numbers.join(",")
end

puts total([1, 2, 3])

# Breaks R-2b: a bare `import` brings a module into scope under its qualified
# name and nothing more. Unqualified names arrive only through the list or the
# glob on an import line, `::{...}` or `::*`, which the consumer writes, so
# importing a module never quietly changes what a name in this file means.
# `polite` is exported and still not in scope here.
module diagnostics/r2b_name_not_imported

import dep/greeter

puts polite("iyi")

# 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

# Breaks R-3: `impl Trait for Type` may live in the module that defines the
# trait or the module that defines the type, and nowhere else. `Greet` belongs
# to `dep/greeter` and `User` belongs to `dep/user`, so this module owns
# neither and is the one place the impl cannot be written. That restriction is
# what makes a type's method set knowable from its declarations alone.
module diagnostics/r3_orphan_impl

import dep/greeter::*
import dep/user::*

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

puts User.new("iyi").greet

# Breaks R-3 from the calling side: a type's method set is closed, so a bound
# on a type parameter is a question with a definite answer at the call. `Int32`
# has no `impl Greet` and cannot acquire one later, so the call is refused as a
# missing trait rather than as a failed overload match.
module diagnostics/r3_unmet_trait_bound

pub trait Greet
  abstract def greet : String
end

pub struct User
  getter name : String

  def initialize(@name : String)
  end
end

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

pub def announce(item : T) : String forall T : Greet
  "-> #{item.greet}"
end

puts announce(User.new("iyi"))
puts announce(42)

# Breaks R-4 by asking for the one clause of it that has nothing behind it.
#
# R-4's third sentence says `@[Monomorphize]` forces specialisation across a
# module boundary. SPEC.md III.9 records what that is worth today: nothing in
# the compiler mentions the annotation, a dictionary or a GC shape. So this is
# not a feature that misbehaves, it is a name the compiler has never heard,
# and the rejection below is a compiler declining to accept a promise it
# cannot keep rather than compiling the program as though the rule were built.
#
# What runs instead of the dictionary is the rule's second sentence applied
# everywhere: a generic's body travels in the artifact and every consumer
# compiles it again for the types it uses. `bench/generic_boundary.py` is the
# measurement of what that costs a consumer's front end.
module diagnostics/r4_dictionary

@[Monomorphize]
pub def twice(x : T) : Array(T) forall T
  [x, x]
end

puts twice(1).size

# A module the break program imports, exporting one derive macro. It compiles:
# a macro body is expanded where the `derive` is written, not where the macro
# is defined, so the refusal this module earns lands in its consumer's build.
#
# `counted` asks a question about the whole program. `all_subclasses` answers
# with every type compiled beside it, which is exactly what R-5 keeps a macro
# away from: a derive that read it would generate different code depending on
# what else happened to be in the build, and then a `.iyimod` could not carry
# what it generated (SPEC.md R-5, II.4).
module dep/global_derive

pub macro counted(declaration)
  def counted : Int32
    {% count = 0 %}
    {% for field in declaration[:fields] %}
      {% count = field[:type].all_subclasses.size %}
    {% end %}
    {{ count }}
  end
end

# Breaks the error rule in SPEC.md III.1: an error is an ordinary member of a
# union, so handling one needs no new machinery, only the totality check a
# `case` already performs. `read` can return an `IOError` and this `case` has
# no branch for it, which is the same mistake as ignoring a returned error and
# is caught by the same check.
module diagnostics/errors_non_exhaustive

pub struct IOError
  getter path : String

  def initialize(@path : String)
  end
end

# `Error` is the compiler's trait, which is what lets a union member be an
# error member without any name in scope deciding it.
impl Error for IOError
  def message : String
    "no such file: #{path}"
  end
end

pub def read(path : String) : String | IOError
  return IOError.new(path) if path == "missing"
  "12"
end

case read("missing")
in String then puts it
end