RCE language specification, draft 0.5

7. Well-formedness: what is refused at entry

This section is the checklist of rules a program must pass to be accepted (well-formedness). Each rule has a name such as W-TY-1, and a refused program is reported with the rule it broke. Example: a function declared -> i64 whose body returns text is refused by W-TY-1.

A program is refused if any rule fails. Every diagnostic names its rule.

Lexical and syntax

W-LEX-1 Not UTF-8, BOM, bare CR, or a tab character.
W-LEX-2 Inconsistent dedent (2.6).
W-LEX-3 A literal outside every possible type range, or an invalid \u{}.
W-SYN-1 Not in the language of section 3.
W-VER-1 A first-line # rce-version: declaration naming a version other than 0.5, 0.6 or 0.7 (2.7).

Names and modules

W-NAME-1 Unresolved name, or a name resolved in the wrong namespace.
W-NAME-2 Duplicate declaration in one scope; shadowing a parameter, field or module-level name inside the same item.
W-MOD-1 use of a private item; W-MOD-2 import cycle. The reference checker reports a private name reached through use as W-VIS-1, which is the same rule.
W-MOD-3 An imported name that clashes with a declaration of the importing module or with a name imported from another module (imported names are not renamed).
W-SAFE-1 The identifiers unsafe, Rc, Arc, RefCell, transmute, static: refused with "memory safety is by construction" (there are no escape hatches in RCE other than the extern boundary of 5.11).
W-FFI-1 An extern declaration whose ABI is not "C", that is comptime or generic, or whose parameter or result types break 5.11; or a foreign function's name used other than as the callee of a direct call.

Types

W-TY-1 Any typing rule of section 5 fails.
W-TY-2 Nested option τ??; borrow of a borrow &&τ; [τ] not behind a borrow; a borrow, region type or fn type inside a data type.
W-TY-3 Integer/float mixing without as; implicit narrowing.
W-PAT-1 A binding pattern whose name equals a variant in scope.
W-MATCH-1 A non-exhaustive match (5.3 [Match]); W-MATCH-2 an unreachable arm (subsumed by earlier unguarded arms).
W-PLACE Left side of an assignment or op= is not a mutable place.

Ownership and borrowing

W-OWN-1 Use after move (O1). W-OWN-2 Violating [No-Alias-Write] or [No-Mut-Read]. W-OWN-3 Storing, returning (except R-RET) or capturing a borrow. W-REG-1 A region-typed value escaping its with arena block.
W-SPAWN-1 Spawning with a borrow or region-typed argument.

The Form

W-STATE-1 A state with no fields; W-STATE-2 a field initializer that is not a comptime constant; W-STATE-3 a field type that is not an owned data type.
W-STEP-1 A step naming an undeclared region or matching an undeclared event. W-STEP-2 Totality: an event that no step and no actor handler can ever match. W-STEP-3 The arrow form on a region with more than one field. W-STEP-4 Within one region, two unguarded steps whose patterns overlap (the second is unreachable).
W-EFF-1 emit, spawn, channel operations or select in a pure fn; reading another region's fields in a step; calling a foreign function anywhere but fn main or a task function.
W-REC-1 A cycle in the call graph, including through trait methods after monomorphization, other than a cycle of plain functions (one function calling itself included) whose calls are done by layered summed measures, or each of whose cycles of calls passes through a function declared with bound (6.7); par or for … par in a function of a cycle with a bounded function; bound on an iterator, a foreign function or a trait signature.
W-CT-1 Comptime code that calls a non-comptime-safe function or traps or exceeds fuel.
W-INT-1 An example or check that does not hold.
W-SIMD-1 A lane-wise operator on arrays of different lengths, of an unfixed length, or with non-numeric lanes (5.1).
W-LIN-1 A linear value not consumed exactly once on every path, copied, moved inside a loop, or placed in a collection, field, payload, channel or iterator (5.12).
W-DEV-1 A growable value (List, Map, Set, text, slice, channel, iterator) bound in a device region, or emit, spawn, send, select, yield or a foreign call inside one (5.13).
W-ITER-1 An iterator function that is not pure or has an arrow body; yield outside an iterator function; an iter τ value used other than as a for operand or .collect() receiver (5.14).
W-REF-1 A refined type (5.1) that is generic, refines a type other than an integer type, text or a collection, or whose predicate is outside the decidable fragment (a term other than self, self.len() or an integer literal, an operator other than a comparison, and, or, not, or a call other than a text character class).
W-LOOP-1 A LOOP_LIMIT declaration that is not const LOOP_LIMIT: u64 = n with a positive literal n (6.7).
W-TRAIT-1 An impl not matching its trait; W-TRAIT-2 incoherent or orphan impls; W-TRAIT-3 a type used with ==, !=, an ordering operator or a generic bound without implementing the trait it needs.

Version 0.8 only (5.16)

W-CTX-1 Context text made other than by C.lit of a string literal or C.encode; joined with another context or plain text; carried by an event payload; an unknown context.
W-SEC-1 An operator or method on a secret other than ==/!=; a secret in an emitted value, a channel, an error payload or a foreign call.
W-CAP-1 A capability outside an event payload field or a parameter; Guarded outside a state field; an authority that is not a declared struct.
W-CAP-2 A step that writes a Guarded[τ, A] field on an event without a Cap[A] field. (W-NAME-2 refuses a declaration named after a 5.16 type or context.)

Version 0.6 only (Appendix C, applies only to a module declaring # rce-version: 0.6): W-PAR-1 to W-PAR-4, W-DL-1, W-ND-1, W-GRP-1 to W-GRP-3, W-SES-1 to W-SES-3, W-SCOPE-1, W-ATOM-1, W-ATOM-2, W-CRDT-1, W-LVAR-1, W-LVAR-2, W-NODE-1, W-SUP-1, W-SUP-2, W-INTR-1 and W-RT-1.

Refused examples by rule

Each program below breaks the rule named above it. Run it to see the refusal, or edit it until it is accepted.

`W-CT-1` (3)

spec/examples/inadmissible/comptime_check.rce

Expected: refused at the admit stage by W-CT-1: line 3: W-CT-1 comptime block in `f`: trap: check failed

const N: usize = 12

fn f() -> usize
    comptime
        check N % 8 == 0
    return N

spec/examples/inadmissible/const_overflow.rce

Expected: refused at the admit stage by W-CT-1: line 1: W-CT-1 const `BIG`: trap: overflow: 300 is outside u8

const BIG: u8 = 200 + 100

spec/examples/inadmissible/state_init_overflow.rce

Expected: refused at the admit stage by W-CT-1: line 0: W-CT-1 state initializer: trap: overflow: 256 is outside u8

state S
    n: u8 = 255 + 1

event E

step S on E -> n

`W-DEV-1` (3)

spec/examples/ill_typed/device_emit.rce

Expected: refused at the check stage by W-DEV-1: line 3: W-DEV-1 emit inside a device region

fn main()
    with device gpu
        emit 1

spec/examples/ill_typed/device_extern.rce

Expected: refused at the check stage by W-DEV-1: line 5: W-DEV-1 `c_tick` is a foreign function and cannot be called in a device region

extern "C" fn c_tick() -> u32

fn main()
    with device gpu
        let t = c_tick()

spec/examples/ill_typed/device_list.rce

Expected: refused at the check stage by W-DEV-1: line 3: W-DEV-1 a device region holds fixed-size values only, found List[u64]

fn f(n: u64) -> u64
    with device gpu
        let xs: List[u64] = [n, n]
        return xs.len() as u64

`W-EFF-1` (2)

spec/examples/ill_typed/extern_in_pure.rce

Expected: refused at the check stage by W-EFF-1: line 3: W-EFF-1 `c_rand` is a foreign function: only main and task functions may call it

extern "C" fn c_rand() -> u32

fn roll() -> u32 = c_rand()

spec/examples/ill_typed/pure_send.rce

Expected: refused at the check stage by W-EFF-1: line 2: W-EFF-1 emit in a pure function

fn f(x: i64) -> i64
    emit x
    return x

`W-FFI-1` (3)

spec/examples/ill_typed/extern_abi.rce

Expected: refused at the check stage by W-FFI-1: line 1: W-FFI-1 unknown ABI "stdcall" (only "C")

extern "stdcall" fn c_f(n: u32) -> u32

fn main()
    emit c_f(1)

spec/examples/ill_typed/extern_owned_param.rce

Expected: refused at the check stage by W-FFI-1: line 1: W-FFI-1 foreign parameter type List[u8] is not bool, an integer, f64, &text, &[scalar] or &mut [scalar]

extern "C" fn c_take(xs: List[u8]) -> u32

fn main()
    emit c_take([1, 2])

spec/examples/ill_typed/extern_text_result.rce

Expected: refused at the check stage by W-FFI-1: line 1: W-FFI-1 foreign result type text is not bool, an integer, f64 or ()

extern "C" fn c_name(n: u32) -> text

fn main()
    emit c_name(1)

`W-INT-1` (12)

spec/examples/inadmissible/arena_size_limit.rce

Expected: refused at the admit stage by W-INT-1: line 8: W-INT-1 check: trap: size limit

fn build(n: u64) -> u64
    var k: u64 = 0
    with arena a bound 16
        let xs: List[u64] @a = [n, n, n, n, n, n, n, n, n, n]
        k = xs.len() as u64
    return k

check build(12345) == 10

spec/examples/inadmissible/bslice_boundary.rce

Expected: refused at the admit stage by W-INT-1: line 1: W-INT-1 check: trap: not a char boundary

check "héllo"[0:2] == "h"

spec/examples/inadmissible/f32_overflow.rce

Expected: refused at the admit stage by W-INT-1: line 1: W-INT-1 check: trap: non-finite float

check (1e39 as f32) as f64 > 0.0

spec/examples/inadmissible/false_check.rce

Expected: refused at the admit stage by W-INT-1: line 2: W-INT-1 check is false

intent "fib"
    check fib(10) == 56

fn fib(n: u32) -> u64
    var a: u64 = 0
    var b: u64 = 1
    for _ in 0..n
        let t = a + b
        a = b
        b = t
    return a

spec/examples/inadmissible/guard_trap.rce

Expected: refused at the admit stage by W-INT-1: line 2: W-INT-1 example does not hold: event 1 (Go) refused: trap(division by zero)

intent "guard trap refuses (S1)"
    example Go(d: 0) -> 1

state S
    n: i64 = 1

event Go(d: i64)

step S on Go(d: d) if 10 / d > 1 -> n + 1
step S on Go(d: _) -> n

spec/examples/inadmissible/iter_unbounded.rce

Expected: refused at the admit stage by W-INT-1: line 9: W-INT-1 check: trap: loop bound

const LOOP_LIMIT: u64 = 100

fn naturals() -> iter u64
    var i: u64 = 0
    loop
        yield i
        i += 1

check naturals().collect().len() == 5

spec/examples/inadmissible/loop_bound.rce

Expected: refused at the admit stage by W-INT-1: line 2: W-INT-1 check: trap: loop bound

intent "x"
    check spin() == 0

fn spin() -> u64
    var k: u64 = 0
    while true bound 10
        k += 1
    return 0

spec/examples/inadmissible/loop_limit_low.rce

Expected: refused at the admit stage by W-INT-1: line 9: W-INT-1 check: trap: loop bound

const LOOP_LIMIT: u64 = 10

fn count(n: u64) -> u64
    var k: u64 = 0
    while k < n
        k += 1
    return k

check count(20) == 20

spec/examples/inadmissible/u64_underflow.rce

Expected: refused at the admit stage by W-INT-1: line 4: W-INT-1 check: trap: overflow: -1 is outside u64

fn sub(a: u64, b: u64) -> u64
    return a - b

check sub(0, 1) == 0

spec/examples/inadmissible/unexpected_refusal.rce

Expected: refused at the admit stage by W-INT-1: line 2: W-INT-1 example does not hold: event 1 (Dec) refused: trap(overflow: -1 is outside u64)

intent "counter"
    example Dec -> 0

state Counter
    n: u64 = 0

event Dec

step Counter on Dec -> n - 1

spec/examples/inadmissible/wrong_example_value.rce

Expected: refused at the admit stage by W-INT-1: line 2: W-INT-1 example does not hold: final value is 2, expected 3

intent "counter"
    example Inc, Inc -> 3

state Counter
    n: u64 = 0

event Inc

step Counter on Inc -> n + 1

spec/examples/inadmissible/wrong_refusal.rce

Expected: refused at the admit stage by W-INT-1: line 2: W-INT-1 example does not hold: event 1 (Dec) refused: Underflow

intent "counter"
    example Dec -> refused: Other

state Counter
    n: u64 = 0

event Dec

error Underflow
error Other

step Counter on Dec -> try n.checked_sub(1) else Underflow

`W-ITER-1` (3)

spec/examples/ill_typed/iter_effect.rce

Expected: refused at the check stage by W-ITER-1: line 1: W-ITER-1 iterator function `ticks` must be pure

fn ticks(c: chan u64) -> iter u64
    yield 1

spec/examples/ill_typed/iter_stored.rce

Expected: refused at the check stage by W-ITER-1: line 5: W-ITER-1 an iterator may only be the operand of `for` or the receiver of `.collect()`

fn evens() -> iter u64
    yield 0

fn f() -> u64
    let it = evens()
    return 0

spec/examples/ill_typed/yield_outside.rce

Expected: refused at the check stage by W-ITER-1: line 2: W-ITER-1 yield outside an iterator function

fn f() -> u64
    yield 1
    return 0

`W-LEX-1` (1)

spec/examples/reject/tab_indent.rce

Expected: refused at the parse stage by W-LEX-1: line 2: W-LEX-1 tab character

fn f() -> i64
	return 1

`W-LEX-2` (1)

spec/examples/reject/bad_dedent.rce

Expected: refused at the parse stage by W-LEX-2: line 3: W-LEX-2 inconsistent dedent

fn f() -> i64
        let x = 1
    return x

`W-LEX-3` (1)

spec/examples/inadmissible/literal_out_of_range.rce

Expected: refused at the check stage by W-LEX-3: line 1: W-LEX-3 literal 300 is outside u8

fn f() -> u8 = 300

`W-LIN-1` (6)

spec/examples/ill_typed/linear_copy.rce

Expected: refused at the check stage by W-LIN-1: line 8: W-LIN-1 a linear value cannot be copied

linear struct H
    id: i32

extern "C" fn c_close(h: H) -> i32

fn main()
    let h = H(id: 3)
    let g = copy(h)
    let _ = c_close(h)
    let _ = c_close(g)

spec/examples/ill_typed/linear_field.rce

Expected: refused at the check stage by W-LIN-1: line 4: W-LIN-1 struct field `a` cannot hold a linear value

linear struct H
    id: i32

struct Pair
    a: H
    b: i32

spec/examples/ill_typed/linear_in_list.rce

Expected: refused at the check stage by W-LIN-1: line 4: W-LIN-1 a linear value cannot sit inside List

linear struct H
    id: i32

fn f(hs: List[H]) -> u64
    return 0

spec/examples/ill_typed/linear_loop.rce

Expected: refused at the check stage by W-LIN-1: line 0: W-LIN-1 linear `h` is moved inside a loop

linear struct H
    id: i32

extern "C" fn c_close(h: H) -> i32

fn main()
    let h = H(id: 3)
    for i in 0..3
        let _ = c_close(h)

spec/examples/ill_typed/linear_one_branch.rce

Expected: refused at the check stage by W-LIN-1: line 8: W-LIN-1 linear `h` is consumed on some branches but not others

linear struct H
    id: i32

extern "C" fn c_close(h: H) -> i32

fn main()
    let h = H(id: 3)
    if h.id > 0
        let _ = c_close(h)

spec/examples/ill_typed/linear_unconsumed.rce

Expected: refused at the check stage by W-LIN-1: line 0: W-LIN-1 linear `h` is not consumed at the end of its block

linear struct H
    id: i32

extern "C" fn c_close(h: H) -> i32

fn main()
    let h = H(id: 3)
    emit h.id

`W-LOOP-1` (1)

spec/examples/ill_typed/loop_limit_type.rce

Expected: refused at the check stage by W-LOOP-1: line 1: W-LOOP-1 LOOP_LIMIT must be declared `const LOOP_LIMIT: u64 = n` with a positive literal n

const LOOP_LIMIT: i64 = 10

`W-MATCH-1` (1)

spec/examples/ill_typed/non_exhaustive.rce

Expected: refused at the check stage by W-MATCH-1: line 6: W-MATCH-1 match is not exhaustive: missing Green

kind Light
    Red
    Green

fn f(l: Light) -> u8
    match l
        Red -> return 1

`W-NAME-1` (1)

spec/examples/ill_typed/unknown_name.rce

Expected: refused at the check stage by W-NAME-1: line 1: W-NAME-1 unknown name `y`

fn f() -> i64 = y + 1

`W-OWN-1` (1)

spec/examples/ill_typed/use_after_move.rce

Expected: refused at the check stage by W-OWN-1: line 5: W-OWN-1 `s` is used after it was moved

fn take(s: text) -> u64 = s.len() as u64

fn twice(s: text) -> u64
    let a = take(s)
    return a + take(s)

`W-OWN-2` (2)

spec/examples/ill_typed/modify_while_iterating.rce

Expected: refused at the check stage by W-OWN-2: line 3: W-OWN-2 `xs` is borrowed by the for loop and cannot be modified inside it

fn f()
    var xs: List[i64] = [1, 2]
    for x in xs
        xs.append(x)

spec/examples/ill_typed/mut_alias.rce

Expected: refused at the check stage by W-OWN-2: line 6: W-OWN-2 `xs` is borrowed mutably and again in one call

fn both(a: &mut List[i64], b: &List[i64])
    pass

fn bad()
    var xs: List[i64] = [1]
    both(&mut xs, &xs)

`W-OWN-3` (1)

spec/examples/ill_typed/borrow_escape.rce

Expected: refused at the check stage by W-OWN-3: line 1: W-OWN-3 a returned borrow must derive from a borrowed parameter (R-RET)

fn f() -> &List[i64]
    let xs: List[i64] = [1]
    return &xs

`W-REC-1` (3)

spec/examples/ill_typed/rec_not_structural.rce

Expected: refused at the check stage by W-REC-1: line 4: W-REC-1 recursion through countdown has no decreasing measure (6.7): no layers of summed measures, each kept by every call not yet done and shrunk by at least one, leave the remaining calls without a cycle, and a cycle of its calls passes through no function declared with `bound`

fn countdown(n: u64) -> u64
    if n == 0
        return 0
    return countdown(n - 1)

spec/examples/ill_typed/rec_same_arg.rce

Expected: refused at the check stage by W-REC-1: line 8: W-REC-1 recursion through loop_forever has no decreasing measure (6.7): no layers of summed measures, each kept by every call not yet done and shrunk by at least one, leave the remaining calls without a cycle, and a cycle of its calls passes through no function declared with `bound`

kind Tree2
    Leaf2(v: i64)
    Node2(l: Box[Tree2], r: Box[Tree2])

fn loop_forever(t: &Tree2) -> i64
    match t
        Leaf2(v: v) -> return v
        Node2(l: l, r: r) -> return loop_forever(t)

spec/examples/ill_typed/recursion.rce

Expected: refused at the check stage by W-REC-1: line 1: W-REC-1 recursion through f, g has no decreasing measure (6.7): no layers of summed measures, each kept by every call not yet done and shrunk by at least one, leave the remaining calls without a cycle, and a cycle of its calls passes through no function declared with `bound`

fn f(n: u64) -> u64 = g(n)

fn g(n: u64) -> u64 = f(n)

`W-REG-1` (1)

spec/examples/ill_typed/arena_escape.rce

Expected: refused at the check stage by W-REG-1: line 5: W-REG-1 a value in arena `a` escapes into `out`

fn f(s: &text) -> List[text]
    var out: List[text] = []
    with arena a
        let ws: List[text] @a = s.words()
        out = ws
    return out

`W-SAFE-1` (1)

spec/examples/ill_typed/unsafe_name.rce

Expected: refused at the check stage by W-SAFE-1: line 2: W-SAFE-1 `unsafe` is refused

fn f() -> i64
    let unsafe = 1
    return unsafe

`W-SIMD-1` (2)

spec/examples/ill_typed/simd_len.rce

Expected: refused at the check stage by W-SIMD-1: line 2: W-SIMD-1 lane-wise `+` needs two arrays of one fixed length, found [i32; 3] and [i32; 4]

fn f(a: [i32; 3], b: [i32; 4]) -> [i32; 3]
    return a + b

spec/examples/ill_typed/simd_text.rce

Expected: refused at the check stage by W-SIMD-1: line 2: W-SIMD-1 lane-wise `*` needs numeric lanes, found text

fn f(a: [text; 2], b: [text; 2]) -> [text; 2]
    return a * b

`W-SPAWN-1` (2)

spec/examples/ill_typed/extern_spawn.rce

Expected: refused at the check stage by W-SPAWN-1: line 4: W-SPAWN-1 `c_work` is a foreign function and cannot be spawned

extern "C" fn c_work(n: u32) -> u32

fn main()
    spawn c_work(3)

spec/examples/ill_typed/spawn_borrow.rce

Expected: refused at the check stage by W-SPAWN-1: line 7: W-SPAWN-1 spawned tasks cannot receive borrows

fn worker(c: chan i64, xs: &List[i64])
    c <- 1

fn main()
    let c = chan[i64](1)
    let xs: List[i64] = [1]
    spawn worker(c, &xs)

`W-STATE-2` (1)

spec/examples/ill_typed/state_no_init.rce

Expected: refused at the check stage by W-STATE-2: line 2: W-STATE-2 field `n` needs a comptime initial value

state S
    n: u64

event E

step S on E -> n

`W-STEP-2` (1)

spec/examples/ill_typed/unhandled_event.rce

Expected: refused at the check stage by W-STEP-2: line 5: W-STEP-2 event `Dec` is handled by no step or actor: δ would not be total

state Counter
    n: u64 = 0

event Inc
event Dec

step Counter on Inc -> n + 1

`W-STEP-4` (1)

spec/examples/ill_typed/unreachable_step.rce

Expected: refused at the check stage by W-STEP-4: line 7: W-STEP-4 unreachable: the unguarded step at line 6 already handles S on E

state S
    n: u64 = 0

event E

step S on E -> n + 1
step S on E -> n + 2

`W-SYN-1` (10)

spec/examples/reject/assign_in_expr.rce

Expected: refused at the parse stage by W-SYN-1: line 1: W-SYN-1 expected `)` (found `=`)

fn f() -> i64 = (x = 1)

spec/examples/reject/chained_compare.rce

Expected: refused at the parse stage by W-SYN-1: line 1: W-SYN-1 expected end of line (found `<`)

fn f(a: i64) -> bool = 0 < a < 10

spec/examples/reject/class_keyword.rce

Expected: refused at the parse stage by W-SYN-1: line 1: W-SYN-1 expected a declaration (found `class`)

class Foo
    x: i64

spec/examples/reject/if_expr_no_else.rce

Expected: refused at the parse stage by W-SYN-1: line 1: W-SYN-1 expected `else` (found end of line)

fn f(a: bool) -> i64 = if a then 1

spec/examples/reject/kind_empty.rce

Expected: refused at the parse stage by W-SYN-1: line 2: W-SYN-1 expected indented block (found `fn`)

kind K
fn f() -> i64 = 1

spec/examples/reject/missing_arrow_example.rce

Expected: refused at the parse stage by W-SYN-1: line 2: W-SYN-1 expected `->` (found integer `1`)

intent "x"
    example Inc 1

spec/examples/reject/state_no_fields.rce

Expected: refused at the parse stage by W-SYN-1: line 2: W-SYN-1 expected indented block (found `event`)

state S
event E

spec/examples/reject/step_no_on.rce

Expected: refused at the parse stage by W-SYN-1: line 4: W-SYN-1 expected `on` (found `E`)

state S
    n: i64 = 0
event E
step S E -> n

spec/examples/reject/try_in_then.rce

Expected: refused at the parse stage by W-SYN-1: line 1: W-SYN-1 expected an expression (found `try`)

fn f(a: bool) -> i64 = if a then try g() else 0

spec/examples/reject/unterminated_string.rce

Expected: refused at the parse stage by W-SYN-1: line 1: W-SYN-1 unterminated string

fn f() -> text = "abc

`W-TRAIT-2` (1)

spec/examples/ill_typed/orphan_impl.rce

Expected: refused at the check stage by W-TRAIT-2: line 1: W-TRAIT-2 orphan impl: neither the trait nor the type is declared in this module

impl Eq for List[i64]
    fn eq(&self) -> bool = true

`W-TY-1` (10)

spec/examples/ill_typed/f32_literal.rce

Expected: refused at the check stage by W-TY-1: line 2: W-TY-1 `*` on f32 and f64: no implicit conversion

fn f(x: f32) -> f32
    return x * 2.0

spec/examples/ill_typed/f32_mixed.rce

Expected: refused at the check stage by W-TY-1: line 2: W-TY-1 `+` on f32 and f64: no implicit conversion

fn f(x: f32, y: f64) -> f32
    return x + y

spec/examples/ill_typed/fail_not_error.rce

Expected: refused at the check stage by W-TY-1: line 2: W-TY-1 fail needs an error, found ?0

fn f() -> i64
    fail 3

spec/examples/ill_typed/int_mismatch.rce

Expected: refused at the check stage by W-TY-1: line 1: W-TY-1 `+` on u8 and i64: no implicit conversion

fn f(a: u8, b: i64) -> i64 = a + b

spec/examples/ill_typed/iter_yield_type.rce

Expected: refused at the check stage by W-TY-1: line 2: W-TY-1 expected text, found ?0

fn names() -> iter text
    yield 3

spec/examples/ill_typed/missing_return.rce

Expected: refused at the check stage by W-TY-1: line 1: W-TY-1 `f` can reach its end without returning i64

fn f(x: i64) -> i64
    if x > 0
        return 1

spec/examples/ill_typed/select_after_type.rce

Expected: refused at the check stage by W-TY-1: line 2: W-TY-1 expected u64, found text

fn f(a: chan u64)
    select
        recv some(x) from a -> pass
        after "soon" -> pass

spec/examples/ill_typed/text_index_char.rce

Expected: refused at the check stage by W-TY-1: line 2: W-TY-1 cannot compare u8 with text

fn f(s: &text) -> bool
    return s[0] == "a"

spec/examples/ill_typed/u64_mixed.rce

Expected: refused at the check stage by W-TY-1: line 2: W-TY-1 `+` on u64 and i64: no implicit conversion

fn f(a: u64, b: i64) -> u64
    return a + b

spec/examples/ill_typed/unchecked_union.rce

Expected: refused at the check stage by W-TY-1: line 6: W-TY-1 expected i64, found i64 ! E

error E

fn g() -> i64 ! E
    fail E

fn f() -> i64 = g()

Built from spec commit 49fa9af. Code cells run the reference checker rce-check, written in Rust and compiled to WebAssembly, inside your browser; nothing is sent to a server. Read-aloud uses the Kokoro-82M model (Apache-2.0), served from this site and run in your browser.

7. Well-formedness: what is refused at entry

Refused examples by rule

W-CT-1 (3)

W-DEV-1 (3)

W-EFF-1 (2)

W-FFI-1 (3)

W-INT-1 (12)

W-ITER-1 (3)

W-LEX-1 (1)

W-LEX-2 (1)

W-LEX-3 (1)

W-LIN-1 (6)

W-LOOP-1 (1)

W-MATCH-1 (1)

W-NAME-1 (1)

W-OWN-1 (1)

W-OWN-2 (2)

W-OWN-3 (1)

W-REC-1 (3)

W-REG-1 (1)

W-SAFE-1 (1)

W-SIMD-1 (2)

W-SPAWN-1 (2)

W-STATE-2 (1)

W-STEP-2 (1)

W-STEP-4 (1)

W-SYN-1 (10)

W-TRAIT-2 (1)

W-TY-1 (10)