What March tells you when something is wrong

A compiler error is the part of a language you read most. March tries to make each one answer three questions: what is wrong, where (the exact piece of code, not just the line), and what to do about it. This page walks through real errors, from the syntax slips of your first hour to a protocol that one role breaks. Every output below is what march --check prints for the program above it today, generated from the compiler rather than pasted by hand.

The playground just below has most of them loaded. Pick one, edit it, and check it again to see how the message changes. It runs the real parser and typechecker in your browser.

How to read a March error

Here is the output for a String where an Int is, shortened and annotated:

-- TYPE MISMATCH --------------------- string-plus-int.march    ← the kind of problem, and the file

expected `String` but got `Int`. [type_mismatch]              ← the message, and its code

5 |     "item " ++ n                                            ← the source, with a caret
                   ^                                              on the exact subterm

    This is argument #2 of a function call.                   ← notes: context, then a fix
    Use `int_to_string(x)` to convert an Int to a String.

    `n` was bound here as `Int`:                              ← labels: other code that matters

4 |   fn label(n : Int) : String do
               ^
    run `march --explain type_mismatch`                       ← a longer page about this code

• The code in brackets ([type_mismatch]) is stable. march --explain <code> prints a page about it: what causes it, a program that triggers it, and how to fix it. The same pages are on this site, listed under Error reference.
• One mistake, one error. When a mistake would cause others downstream, March reports the mistake and holds back the errors that only follow from it.
• Fixes as edits. Many errors also carry a fix. march --check shows it under the error as the lines it changes (4 - old, 4 + new), march --check-json includes it as a text edit, and the language server offers it as a quick fix. Each fix has a tier, the applicability field of the edit, and the heading --check gives it:
  • machine-applicable (“fix (forge fix applies it)”): safe to apply unasked. Before showing one, --check and --check-json apply it to a copy of the file and check the copy, and the editor does the same before offering it. The fix keeps this tier only if its own error is gone and no new error or warning appeared. forge fix applies these, and the editor marks them as the preferred quick fix.
  • has-placeholders (“fix, with a placeholder to fill in”): the right shape with a part to fill in, such as the missing match arm whose body is todo("handle None").
  • maybe-incorrect (“possible fix (a guess: check it before applying it)”): one plausible repair among several, such as a field name with another field spelled just as close. It is offered and never applied unasked.

1. Syntax

The first errors most people meet come from habits other languages taught: then, elif, semicolons, curried calls. March names the habit and shows the March form.

then instead of do

mod Main do
  needs IO.Console

  fn sign(n : Int) : Int do
    if n > 0 then 1 else 0 end
  end

  fn main(_console : Cap(IO.Console)) do
    println(int_to_string(sign(3)))
  end
end

-- SYNTAX ------------------------------------ then.march

I don't recognize `then` here — March uses do/end blocks instead. [then_keyword]

5 |     if n > 0 then 1 else 0 end
                 ^^^^

    if cond do
        expr1
    else
        expr2
    end

    fix (`forge fix` applies it):

5 -     if n > 0 then 1 else 0 end
5 +     if n > 0 do 1 else 0 end

    run `march --explain then_keyword`

It recognises the keyword from another language and shows the whole if shape to copy. Try it

An if without an else

mod Main do
  fn clamp(x : Int) : Int do
    if x > 0 do
      x
    end
  end

  fn main() do
    clamp(5)
  end
end

-- SYNTAX ------------------------- if-without-else.march

March `if` expressions always need an `else` branch: [parse_error]

5 |     end
        ^^^

    if cond do
        expr1
    else
        expr2
    end
    run `march --explain parse_error`

if is an expression in March, so it always produces a value. The message states that rule rather than “unexpected token end”. Try it

An else if chain one end short

mod Main do
  fn pick(a : Bool, b : Bool) : Int do
    if a do 1 else if b do 2 else 3 end
  end

  fn main() do
    pick(false, true)
  end
end

-- SYNTAX --------------------------- else-if-chain.march

This `if` (line 3) needs its own `end`: the `end` on line 4 belongs to an outer block. [parse_error]

3 |     if a do 1 else if b do 2 else 3 end
        ^^

    I only noticed at the end of the file.
    `else if` is a nested `if` in the else position, so each `if` needs its own `end`: a two-branch chain ends `end end`, a three-branch chain `end end end`.

    fix (`forge fix` applies it):

3 |     if a do 1 else if b do 2 else 3 end
4 +     end

    run `march --explain parse_error`

A missing end is usually noticed far from where it belongs. This message points at the if that is missing it, says it only noticed at the end of the file, and says how many ends a chain needs. Try it

Semicolons

mod Main do
  needs IO.Console

  fn total() : Int do
    let x = 1; let y = 2
    x + y
  end

  fn main(_console : Cap(IO.Console)) do
    println(int_to_string(total()))
  end
end

-- SYNTAX ------------------------------- semicolon.march

Unexpected `;`: March separates expressions with newlines, not semicolons. [semicolon_separator]

5 |     let x = 1; let y = 2
                 ^

    Put each expression on its own line.

    fix (`forge fix` applies it):

5 -     let x = 1; let y = 2
5 +     let x = 1
6 +     let y = 2

    run `march --explain semicolon_separator`

The caret is on the ; itself, and the note says what to write instead. Try it

A curried call

mod Main do
  fn adder(x : Int) do
    fn (y) -> x + y
  end

  fn main() do
    adder(1)(2)
  end
end

-- SYNTAX ---------------------------- curried-call.march

`f(...)(...)` is not a chained call — March functions are not curried. [parse_error]

7 |     adder(1)(2)
                ^

    Write `f(a, b)` for a multi-argument call, or put the second call on its own line if you meant two separate statements.
    run `march --explain parse_error`

adder(1)(2) parses in many languages. March explains why it isn’t a chained call here, and gives the two things you probably meant. Try it

2. Names and “did you mean”

A misspelling gets a suggestion, and the suggestion is chosen by what fits, not only by spelling.

A misspelled module

mod Main do
  needs IO.Console

  fn count() : Int do
    Lsit.length([1, 2])
  end

  fn main(_console : Cap(IO.Console)) do
    println(int_to_string(count()))
  end
end

-- NAMING ----------------------- misspelled-module.march

Unknown module `Lsit`. Did you mean `List`? [unknown_qualified_name]

5 |     Lsit.length([1, 2])
        ^^^^^^^^^^^


    fix (`forge fix` applies it):

5 -     Lsit.length([1, 2])
5 +     List.length([1, 2])

    run `march --explain unknown_qualified_name`

The suggestion comes from the standard library’s modules. (The playground can’t show this one: it suggests from the module files on disk, which a browser doesn’t have.)

A misspelled record field

mod Main do
  fn main() do
    let r = { count: 1, cont: "x" }
    let n : Int = r.conut
    n
  end
end

-- NAMING --------------------------- field-by-type.march

This record does not have a field called `conut`. Did you mean `count`? [unknown_record_field]
The fields I see are: cont, count

4 |     let n : Int = r.conut
                      ^^^^^^^


    possible fix (a guess: check it before applying it):

4 -     let n : Int = r.conut
4 +     let n : Int = r.count

cont is the closer spelling, but it holds a String and the annotation wants an Int, so March suggests count. It also lists the fields the record does have. Try it

A misspelled constructor

mod Main do
  type Mail = Postal(Int) | Email(String)
  type Tag = Poss(Int)

  fn main() do
    let m : Mail = Posts(1)
    m
  end
end

-- NAMING --------------------- constructor-by-type.march

I don't know a constructor called `Posts`. [unknown_constructor]
Did you mean `Postal` (from type `Mail`)?

6 |     let m : Mail = Posts(1)
                       ^^^^^^^^


    fix (`forge fix` applies it):

6 -     let m : Mail = Posts(1)
6 +     let m : Mail = Postal(1)

Poss and the standard library’s Post are each one letter from Posts, but only Postal builds a Mail, which the annotation asks for. The suggestion says which type it comes from. Try it

3. Types

A type error puts its caret on the subterm whose type is wrong, says where the expected type came from, and, when the two types share a structure, shows only the part that differs.

A String where an Int is

mod Main do
  needs IO.Console

  fn label(n : Int) : String do
    "item " ++ n
  end

  fn main(_console : Cap(IO.Console)) do
    println(label(3))
  end
end

-- TYPE MISMATCH ------------------ string-plus-int.march

expected `String` but got `Int`. [type_mismatch]

5 |     "item " ++ n
                   ^

    This is the right side of `++`, which joins two `String`s.
    Use `int_to_string(x)` to convert an Int to a String.

    the expected type comes from here:

5 |     "item " ++ n
        ^^^^^^^

    `n` was bound here as `Int`:

4 |   fn label(n : Int) : String do
               ^
    run `march --explain type_mismatch`

The caret is on n, not on the whole ++. Two labels show where String is required and where n got its type, and the note names the conversion function. Try it

Two types that differ in one place

mod Main do
  needs IO.Console

  fn count(xs : List(Int)) : Int do
    List.length(xs)
  end

  fn main(_console : Cap(IO.Console)) do
    let names = ["a", "b"]
    println(int_to_string(count(names)))
  end
end

-- TYPE MISMATCH ------------------ structural-diff.march

expected `List(Int)` but got `List(String)`. [type_mismatch]

10 |     println(int_to_string(count(names)))
                                     ^^^^^

    This is argument #1 of a function call.
    The types differ here:
        List(String)
             ^^^^^^ expected `Int`

    the expected type comes from here:

10 |     println(int_to_string(count(names)))
                               ^^^^^^^^^^^^

    `names` was bound here as `List(String)`:

9 |     let names = ["a", "b"]
            ^^^^^
    run `march --explain type_mismatch`

List(String) and List(Int) share everything but the element type, so the diff underlines just String. With a large record or nested type, this saves comparing both in full. Try it

Too few arguments

mod Main do
  needs IO.Console

  fn main(_console : Cap(IO.Console)) do
    let add = fn (a, b) -> a + b
    println(int_to_string(add(1)))
  end
end

-- TYPE MISMATCH ----------- no-partial-application.march

`add` is a lambda with 2 parameters, but is called with 1 argument. [arity_mismatch]
March has no partial application — a call must supply all arguments.

6 |     println(int_to_string(add(1)))
                              ^^^^^^


    bound here with 2 parameters:

5 |     let add = fn (a, b) -> a + b
                  ^^^^^^^^^^^^^^^^^^

Coming from a curried language, add(1) looks like partial application. The message says March has none, and shows where add got its two parameters. Try it

A let? whose body is not a Result

mod Main do
  fn parse() : Result(Int, String) do Ok(1) end

  fn next() : Result(Int, String) do
    let? x = parse()
    x + 1
  end

  fn main() do
    next()
  end
end

-- TYPE MISMATCH --------------------- let-question.march

expected `Result(Int, String)` but got `Int`. [type_mismatch]

5 |     let? x = parse()
        ^^^^^^^^^^^^^^^^

    This is the declared return type of `next`.
    The code after `let?` must produce a Result with the same error type.

    the expected type comes from here:

4 |   fn next() : Result(Int, String) do
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    run `march --explain type_mismatch`

let? returns early on Err, so the rest of the function must produce a Result too. The note explains that rule instead of reporting a bare Int vs Result clash. Try it

Comparing a type that has no ordering

mod Main do
  needs IO.Console

  type Hue = Red | Blue

  fn main(_console : Cap(IO.Console)) do
    let a = Red
    let b = Blue
    println(if a < b do "less" else "not less" end)
  end
end

-- INTERFACE ------------------------- missing-impl.march

`Hue` does not implement interface `Ord`. [missing_impl]
`<` needs it here.

9 |     println(if a < b do "less" else "not less" end)
                   ^^^^^

    Add `derive Ord for Hue` after the type to get the structural one, or write `impl Ord(Hue) do ... end`.

    fix (`forge fix` applies it):

4 |   type Hue = Red | Blue
5 +   derive Ord for Hue

The message names the operator that needs Ord and gives both fixes: derive the structural ordering in one line, or write your own impl. Try it

4. Capabilities

In March, a program can only do the IO it was granted. main receives its capabilities as parameters, and each module declares the ones it uses with needs (see Capabilities). The errors talk about access in plain terms: “writes a file”, “the console capability”.

main with no grant

mod Main do
  needs IO.Console

  fn main() do
    println("hello")
  end
end

-- CAPABILITY ----------------------- main-no-grant.march

`main` performs IO but declares no grant. The program reaches `IO.Console`; a `main` with no capability parameter is granted nothing. [cap_grant]
help: declare the grant `main` actually needs —
        fn main(_cap_console : Cap(IO.Console)) : ()
or grant everything with `fn main(cap : Cap(IO))`.
`forge fix` can apply this.

4 |   fn main() do
      ^^^^^^^^^^^^


    fix (`forge fix` applies it):

4 -   fn main() do
4 +   fn main(_cap_console : Cap(IO.Console)) do

    run `march --explain cap_grant`

It works out which capability the program actually reaches and writes the narrowest signature for main. forge fix applies it. Try it

Writing a file without saying so

mod Main do
  needs IO.Console

  fn save(n : Int) : () do
    let _ = file_write("/tmp/n", int_to_string(n))
    ()
  end

  fn main(c : Cap(IO.Console)) do
    save(1)
    println("saved")
  end
end

-- CAPABILITY ----------------------- missing-needs.march

`save` writes a file, but module `Main` declares no `needs IO.FileWrite`, and `main` is granted only `Cap(IO.Console)`. [cap_needs]
hint: add this to the module body —
        needs IO.FileWrite
and give `main` a `Cap(IO.FileWrite)` parameter: `fn main(…, _cap_filewrite : Cap(IO.FileWrite))`.

5 |     let _ = file_write("/tmp/n", int_to_string(n))
                ^^^^^^^^^^


    `main` calls `save` here:

10 |     save(1)
         ^^^^

    `main` is granted only `Cap(IO.Console)` here:

9 |   fn main(c : Cap(IO.Console)) do
             ^^^^^^^^^^^^^^^^^^^^^

    fix (`forge fix` applies it):

1 | mod Main do
2 +   needs IO.FileWrite
9 -   fn main(c : Cap(IO.Console)) do
9 +   fn main(c : Cap(IO.Console), _cap_filewrite : Cap(IO.FileWrite)) do

    run `march --explain cap_needs`

Two things are missing: the module’s needs IO.FileWrite line, and a grant on main. They are reported as one error, with the call chain from main and both edits in the hint. Try it

Passing the wrong capability

mod Main do
  needs IO.Console

  fn read(c : Cap(IO.FileRead)) : String do "x" end

  fn main(c : Cap(IO.Console)) do println(read(c)) end
end

-- CAPABILITY -------------------- wrong-capability.march

`read` needs file-read access, but `c` is the console capability. [cap_mismatch]

6 |   fn main(c : Cap(IO.Console)) do println(read(c)) end
                                                   ^

    `IO.Console` and `IO.FileRead` are both parts of `IO`; neither contains the other.
    help: give `main` a `Cap(IO.FileRead)` parameter and pass it to `read`.
    and add `needs IO.FileRead` to the module.

    `read` needs `Cap(IO.FileRead)`:

6 |   fn main(c : Cap(IO.Console)) do println(read(c)) end
                                              ^^^^^^^

    `c` was bound here as `Cap(IO.Console)`:

6 |   fn main(c : Cap(IO.Console)) do println(read(c)) end
              ^

    `Cap(IO.FileRead)` is named here, and the module declares no `needs IO.FileRead`:

4 |   fn read(c : Cap(IO.FileRead)) : String do "x" end
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

    `main` is granted only `Cap(IO.Console)` here:

6 |   fn main(c : Cap(IO.Console)) do println(read(c)) end
             ^^^^^^^^^^^^^^^^^^^^^

    fix (`forge fix` applies it):

1 | mod Main do
2 +   needs IO.FileRead
6 -   fn main(c : Cap(IO.Console)) do println(read(c)) end
6 +   fn main(c : Cap(IO.Console), _cap_fileread : Cap(IO.FileRead)) do println(read(c)) end
6 -   fn main(c : Cap(IO.Console)) do println(read(c)) end
6 +   fn main(c : Cap(IO.Console)) do println(read(_cap_fileread)) end

Underneath this is a type mismatch, but the message says what it means: read needs file-read access, and c is the console. It explains why neither capability covers the other, then shows every place the fix touches. Try it

5. Linearity

A linear value must be used exactly once: not copied, not dropped (see Linear types). Each error points at both uses, or at the place the value was lost.

Used twice

mod Main do
  needs IO.Console

  always_linear type Token = Token(Int)

  fn consume(t : Token) : Int do
    match t do Token(n) -> n end
  end

  fn main(_console : Cap(IO.Console)) do
    let t = Token(1)
    println(int_to_string(consume(t) + consume(t)))
  end
end

-- LINEARITY -------------------- linear-used-twice.march

The linear value `t` is used more than once here. [linear_used_twice]
Linear values must be consumed exactly once — they cannot be copied or ignored.

12 |     println(int_to_string(consume(t) + consume(t)))
                                                    ^


    `t` was already consumed here:

12 |     println(int_to_string(consume(t) + consume(t)))
                                       ^
    run `march --explain linear_used_twice`

The caret is on the second use and a label marks the first, even though both are on the same line. Try it

Consumed on some branches only

mod Main do
  needs IO.Console

  always_linear type Token = Token(Int)

  fn consume(t : Token) : Int do
    match t do Token(n) -> n end
  end

  fn main(_console : Cap(IO.Console)) do
    let t = Token(1)
    let n = match 2 do
      1 -> consume(t)
      2 -> consume(t) + 1
      _ -> 0
    end
    println(int_to_string(n))
  end
end

-- LINEARITY ----------------- linear-some-branches.march

The linear value `t` is consumed on some branches but not others. [linear_mixed_consumption]
On a branch that doesn't consume it, the value is dropped. Consume it on every branch, or end that branch with `panic(…)` if it never returns.

12 |     let n = match 2 do
                       ^^^^


    `t` is consumed on this branch:

13 |       1 -> consume(t)
                        ^

    but not on this one, where it is dropped:

15 |       _ -> 0
                ^

It names a branch that consumes the token and one that silently drops it, and suggests panic(…) for a branch that never returns. Try it

Captured by a closure

mod Main do
  needs IO.Console

  always_linear type Token = Token(Int)

  fn consume(t : Token) : Int do
    match t do Token(n) -> n end
  end

  fn twice(k : () -> Int) : Int do k() + k() end

  fn main(_console : Cap(IO.Console)) do
    let t = Token(1)
    println(int_to_string(twice(fn () -> consume(t))))
  end
end

-- LINEARITY ---------------------- linear-captured.march

The linear value `t` cannot be captured by a closure. [linear_captured]
A closure may be called multiple times, which would violate the exactly-once guarantee.
Pass `t` as a parameter to the closure instead.

14 |     println(int_to_string(twice(fn () -> consume(t))))
                                     ^^^^^^^^^^^^^^^^^^^

The message gives the reason (a closure can be called more than once) and the fix (take the value as a parameter). Try it

6. Actors

Actor errors use the actor’s own words: its messages, its state, the pid you spawned (see Actors).

A misspelled actor

mod Main do
  needs IO.Console

  actor Counter do
    state { n : Int }
    init { n: 0 }
    on Bump(k : Int) do { state with n: state.n + k } end
  end

  fn main(_console : Cap(IO.Console)) do
    let p = spawn(Countr)
    send(p, Bump(1))
  end
end

-- NAMING ------------------------ misspelled-actor.march

I don't know an actor called `Countr`. [unknown_constructor]
Did you mean `Counter`?

11 |     let p = spawn(Countr)
                       ^^^^^^


    fix (`forge fix` applies it):

11 -     let p = spawn(Countr)
11 +     let p = spawn(Counter)

Inside spawn(…) March is looking for an actor, so it calls Countr an actor and suggests one. Try it

The wrong argument in a message

mod Main do
  needs IO.Console

  actor Counter do
    state { n : Int }
    init { n: 0 }
    on Bump(k : Int) do { state with n: state.n + k } end
  end

  fn main(_console : Cap(IO.Console)) do
    let c = spawn(Counter)
    send(c, Bump("one"))
  end
end

-- TYPE MISMATCH ----------------- message-argument.march

expected `Int` but got `String`. [type_mismatch]

12 |     send(c, Bump("one"))
                      ^^^^^

    `Bump` is a message of actor `Counter`, and its handler declares this argument's type.

    the expected type comes from here:

7 |     on Bump(k : Int) do { state with n: state.n + k } end
                ^
    run `march --explain type_mismatch`

The expected type comes from the handler’s parameter, so the label points into the actor at k : Int, not at a generated message type. Try it

A handler that forgets to return the state

mod Main do
  needs IO.Console

  actor Counter do
    state { n : Int }
    init { n: 0 }
    on Bump(k : Int) do state.n + k end
  end

  fn main(_console : Cap(IO.Console)) do
    let c = spawn(Counter)
    send(c, Bump(1))
  end
end

-- ACTOR -------------------- handler-returns-state.march

The handler for `Bump` must return `Counter`'s new state, a `{ n : Int }`, but it returns an `Int`. [actor_handler_state_type]
A handler's result replaces the actor's state for the next message.

7 |     on Bump(k : Int) do state.n + k end
           ^^^^

    If this is the new value of `n`, return `{ state with n: … }` with it.

    this is an `Int`:

7 |     on Bump(k : Int) do state.n + k end
                            ^^^^^^^^^^^
    run `march --explain actor_handler_state_type`

A handler’s result becomes the actor’s next state. The message says so, and since the handler returns an Int and the state has one Int field, it suggests { state with n: … }. Try it

A message sent to the wrong actor

mod Main do
  needs IO.Console

  actor Counter do
    state { n : Int }
    init { n: 0 }
    on Bump(k : Int) do { state with n: state.n + k } end
  end

  actor Log do
    state { last : String }
    init { last: "" }
    on Note(t : String) do { state with last: t } end
  end

  fn main(_console : Cap(IO.Console)) do
    let log = spawn(Log)
    send(log, Bump(1))
  end
end

-- ACTOR ------------------------- send-wrong-actor.march

`Bump` is a message for `Counter`, but this pid is an actor `Log` (spawned on line 17), so the message would be dropped. [send_wrong_actor]
Send it to a pid spawned from `Counter`, or send this actor one of its own messages.

18 |     send(log, Bump(1))
                   ^^^^^^^

    `Log` handles `Note`.

    `log` is spawned from `Log` here:

17 |     let log = spawn(Log)
                   ^^^^^^^^^^
    run `march --explain send_wrong_actor`

Without this check, the message would be dropped at run time. The error says which actor the message belongs to, which actor the pid is and where it was spawned, and what that actor does handle. Try it

7. Session channels

A protocol gives each end of a channel a script of sends and receives (see Session types). The errors are phrased in terms of that script, not the session-type notation the checker uses internally.

A step out of order

mod Main do
  type Client = Client
  type Server = Server

  protocol Echo do
    Client -> Server : Int
    Server -> Client : Int
  end

  fn main() do
    let (cc, sc) = Chan.new(Echo)
    let cc2 = Chan.send(cc, 42)
    let cc3 = Chan.send(cc2, 43)
    Chan.close(cc3)
    Chan.close(sc)
  end
end

-- PROTOCOL -------------------- channel-wrong-step.march

`Chan.send` can't send here: at this point the channel must receive an `Int`. [session_state_mismatch]

13 |     let cc3 = Chan.send(cc2, 43)
                   ^^^^^^^^^^^^^^^^^^

    What is left on this channel: receive an `Int`, then close.

    the channel is `Client`'s end of protocol `Echo`, declared here:

5 |   protocol Echo do
      ^^^^^^^^^^^^^^^^
    run `march --explain session_state_mismatch`


-- PROTOCOL -------------------- channel-wrong-step.march

`Chan.close` can't close this channel here: at this point the channel must receive an `Int`. [session_state_mismatch]

15 |     Chan.close(sc)
         ^^^^^^^^^^^^^^

    What is left on this channel: receive an `Int`, then send an `Int`, then close.

    the channel is `Server`'s end of protocol `Echo`, declared here:

5 |   protocol Echo do
      ^^^^^^^^^^^^^^^^

Each error says what the channel must do next and spells out the rest of its script (“receive an Int, then close”). The second error is about the server’s end, which never received anything. Try it

A channel closed before its last step

mod Main do
  type Client = Client
  type Server = Server

  protocol Order do
    Client -> Server : Int
    choose by Server:
      ok  -> Server -> Client : Bool
      err -> Server -> Client : String
    end
    Client -> Server : String
  end

  fn main() do
    let (cc, sc) = Chan.new(Order)
    let cc2 = Chan.send(cc, 1)
    let (_n, sc2) = Chan.recv(sc)
    let sc3 = Chan.send(Chan.choose(sc2, :ok), true)
    let (label, cc3) = Chan.offer(cc2)
    match label do
      :ok ->
        let (_b, cc4) = Chan.recv(cc3)
        Chan.close(cc4)
      :err ->
        let (_s, cc4) = Chan.recv(cc3)
        Chan.close(Chan.send(cc4, "thanks"))
    end
    let (_t, sc4) = Chan.recv(sc3)
    Chan.close(sc4)
  end
end

-- PROTOCOL ------------------- channel-close-early.march

`Chan.close` can't close this channel here: at this point the channel must send a `String`. [session_state_mismatch]

23 |         Chan.close(cc4)
             ^^^^^^^^^^^^^^^

    What is left on this channel: send a `String`, then close.
    The conversation so far, in protocol `Order`:

      Client -> Server : Int       done
      choose by Server: ok | err   done
      Client -> Server : String    <- `Client` must do this next

    the channel is `Client`'s end of protocol `Order`, declared here:

 5 |   protocol Order do
       ^^^^^^^^^^^^^^^^^
    run `march --explain session_state_mismatch`

When the protocol has more than two steps, the error also draws the conversation so far, one step per line in the order the protocol declares them. done marks the steps this end has already taken; a choose is drawn with all its branches when the channel has gone past it. The arrow on the right (<- `Client` must do this next) is where the channel is now, and the headline says what the call tried instead. Here the ok branch closes the client’s end, but every branch of the choose leads to the client’s last String. A two-step protocol like Echo above gets no diagram, because the headline already says everything it would.

An offer left unhandled

mod Main do
  type C = C
  type S = S

  protocol Lookup do
    choose by S:
      ok  -> S -> C : Int
      err -> S -> C : String
    end
  end

  fn main() do
    let (cc, sc) = Chan.new(Lookup)
    let sc2 = Chan.choose(sc, :ok)
    Chan.close(Chan.send(sc2, 7))
    let (label, cc2) = Chan.offer(cc)
    match label do
      :ok ->
        let (_n, cc3) = Chan.recv(cc2)
        Chan.close(cc3)
    end
  end
end

-- PROTOCOL ------------------ offer-not-exhaustive.march

This `match` doesn't handle every branch the peer can choose — missing: :err. [session_offer_nonexhaustive]
The protocol's `offer` branches are: :ok, :err.

17 |     match label do
               ^^^^^^^^

    run `march --explain session_offer_nonexhaustive`

The protocol fixes which branches the other side can choose, so a match that skips one is an error, and the message names the branch you missed. Try it

8. Protocols and choreography

A protocol is checked when you declare it, before any code runs it. With @[endpoints], March generates each role’s API and checks that the role’s code follows the protocol (see Choreography).

A step that can never run

mod Main do
  type A = A
  type B = B

  protocol Ticker do
    loop do
      A -> B : Int
    end
    B -> A : Bool
  end

  fn main() do
    ()
  end
end

-- PROTOCOL ----------------------- step-after-loop.march

Protocol `Ticker`: this step can never run — it comes after a `loop`, and a `loop` block repeats forever, so it must be the last step. [protocol_invalid]

9 |     B -> A : Bool
        ^


    this `loop` repeats forever:

7 |       A -> B : Int
          ^
    run `march --explain protocol_invalid`

The message explains why the step is unreachable, and a label points at the loop that never ends. Try it

A step after a branch that loops forever

mod Main do
  type A = A
  type B = B

  protocol Batch do
    choose by A:
      more -> loop do A -> B : Int end
      done -> A -> B : Bool
    end
    B -> A : Bool
  end

  fn main() do
    ()
  end
end

-- PROTOCOL --------------------- step-after-choose.march

Protocol `Batch`: this step can never run in the `choose` branch that ends in a `loop` — the steps after a `choose` are projected into EVERY branch. Move it into the `done` branch, after its last step. A branch with several steps lists them on the lines after `done ->`, one per line, indented under the label (no `do`/`end`). [protocol_invalid]

10 |     B -> A : Bool
         ^


    this `loop` repeats forever:

7 |       more -> loop do A -> B : Int end
                          ^
    run `march --explain protocol_invalid`

The steps after a choose run at the end of every branch, so the more branch, which loops forever, can never reach B -> A : Bool. The message names the branch that can (done) and shows how a branch with several steps is written: one step per line under done ->, with no do/end. Try it

A crash nobody handles

mod Main do
  needs IO
  needs Session.Live

  @[endpoints]
  protocol Logging do
    may crash C
    L -> I : Int
    C -> I : String
    I -> L : String
  end

  fn main(_c : Cap(IO)) do () end
end

-- PROTOCOL ----------------------------- may-crash.march

Protocol `Logging`: `C` may crash, so `C -> I : ...` needs `or crash do ... end`: what does `I` do if `C` crashes before sending? [role_needs_invalid]

9 |     C -> I : String
        ^

    The crash branch is the rest of the conversation when `C` is gone. It must begin, for `L`, with a message from `I`; the fix sends one each, for you to change to what the conversation should do.

    fix (`forge fix` applies it):

 9 |     C -> I : String
10 +       or crash do
11 +         I -> L : String
12 +       end

    run `march --explain role_needs_invalid`

Once a role may crash, every message from it needs a plan for when it doesn’t arrive. The error asks the question the protocol must answer: what does I do if C crashes before sending? The machine fix adds an or crash branch for you to fill in. Try it

A role that skips a step

mod Main do
  needs IO
  needs Session.Live

  @[endpoints]
  protocol Stream do
    loop do
      Prod -> Cons : Int
      choose by Cons:
        more -> Cons -> Prod : Bool
        done -> Cons -> Prod : Bool
                stop
      end
    end
  end

  pfn cons(s : Cap(Session.Live), st : Stream_Cons.S_recv_Msg_Prod_Cons_1) : Stream_Cons.Yield do
    Stream_Cons.close(s, Stream_Cons.choose_done(s, st, true))
  end

  fn main(_c : Cap(IO)) do () end
end

-- PROTOCOL --------------------- role-skips-a-step.march

Role `Cons` tries to choose `more` or `done` here, but at this point protocol `Stream` says it must receive an `Int` from `Prod`. [protocol_step_order]

18 |     Stream_Cons.close(s, Stream_Cons.choose_done(s, st, true))
                                                         ^^

    Take that step with `Stream_Cons.recv_Msg_Prod_Cons_1` first.
    The conversation so far, in protocol `Stream`:

      loop do                         (repeats)
        Prod -> Cons : Int            <- `Cons` must do this next
        choose by Cons: more | done   <- `Cons` tried this

    `Cons` is here: it must receive an `Int` from `Prod`:

8 |       Prod -> Cons : Int
          ^^^^

    `st` is the state bound here:

17 |   pfn cons(s : Cap(Session.Live), st : Stream_Cons.S_recv_Msg_Prod_Cons_1) : Stream_Cons.Yield do
                                       ^^
    run `march --explain protocol_step_order`

The role’s code calls a generated function, but the error is about the protocol: what Cons tried to do, the step it skipped (with a “you are here” label on the protocol line), and which function takes that step. (The playground can’t load the session runtime this one needs.)

The diagram draws the whole conversation, not only Cons’s side, up to the step that went wrong. Read it top to bottom. A loop is drawn as one round, marked (repeats), with its steps indented under it. Two arrows sit in the right-hand column: one on the step Cons must take next and one on the step it tried, so the gap between them is what Cons skipped. A choose that Cons has not reached yet is drawn on one line with its branches (more | done).

A role that repeats a step

mod Main do
  needs IO
  needs Session.Live

  @[endpoints]
  protocol Pump do
    hello: A -> B : String
    loop do
      tick: A -> B : Int
      tock: B -> A : Int
      choose by A:
        go   -> A -> B : Bool
        quit -> A -> B : Bool
                stop
      end
    end
  end

  pfn role_a(s : Cap(Session.Live), st : Pump_A.Entry) : Pump_A.Yield do
    let st1 = Pump_A.send_Hello(s, st, "hi")
    let st2 = Pump_A.send_Tick(s, st1, 1)
    Pump_A.recv_Tock(s, st2, fn (_n, st3) ->
      Pump_A.recv_Tock(s, Pump_A.send_Tick(s, st3, 2), fn (_m, st4) ->
        Pump_A.close(s, Pump_A.choose_quit(s, st4, true))))
  end

  fn main(_c : Cap(IO)) do () end
end

-- PROTOCOL ------------------- role-repeats-a-step.march

Role `A` tries to send an `Int` to `B` here, but at this point protocol `Pump` says it must choose `go` or `quit`. [protocol_step_order]

23 |       Pump_A.recv_Tock(s, Pump_A.send_Tick(s, st3, 2), fn (_m, st4) ->
                                                   ^^^

    Take that step with `Pump_A.choose_go` first.
    The conversation so far, in protocol `Pump`:

      hello: A -> B : String     done
      loop do                    (repeats)
        tick:  A -> B : Int      done   <- `A` tried this again
        tock:  B -> A : Int      done
        choose by A: go | quit   <- `A` must do this next

    `A` is here: it must choose `go` or `quit`:

11 |       choose by A:
                     ^

    `st3` is the state bound here:

22 |     Pump_A.recv_Tock(s, st2, fn (_n, st3) ->
                                          ^^^
    run `march --explain protocol_step_order`

Inside a loop, a role’s next step can come earlier in the protocol than the one it just took. Here A went round again without choosing whether to go on. The diagram marks the steps of this round as done and the one A tried as tried this again. The choose it must make next is drawn on one line with its branches, since A has not picked one. Once a role is inside a branch, the diagram shows the branch it took and names the others in the right-hand column (other branch: `more`). A long conversation keeps three steps of context and shortens the rest to … N earlier steps. (The playground can’t load the session runtime this one needs.)

A role reaching past its grant

mod Main do
  needs IO
  needs IO.Console
  needs IO.FileWrite
  needs Session.Live

  @[endpoints]
  protocol Stream do
    role Cons needs IO.Console
    loop do
      Prod -> Cons : Int
      choose by Cons:
        more -> Cons -> Prod : Bool
        done -> Cons -> Prod : Bool
                stop
      end
    end
  end

  pfn save(n : Int) : () do
    let _ = file_write("/tmp/n", int_to_string(n))
    ()
  end

  pfn cons(s : Cap(Session.Live), con : Cap(IO.Console), st : Stream_Cons.Entry) : Stream_Cons.Yield do
    Stream_Cons.recv_Msg_Prod_Cons_1(s, st, fn (n, st1) ->
      save(n)
      Stream_Cons.close(s, Stream_Cons.choose_done(s, st1, true)))
  end

  fn main(c : Cap(IO)) do
    let _ = Stream_Run.run_Cons(c, "cons", "secret", Stream_Run.addrs_from_env(),
      fn (s, con, st) -> cons(s, con, st))
    ()
  end
end

-- CAPABILITY -------------------------- role-grant.march

The body of role `Cons` writes a file, but the role is granted only `Cap(IO.Console)` (`role Cons needs IO.Console`). A role's grant bounds everything its code reaches, as `main`'s grant bounds the program. [role_grant_exceeded]
help: add `IO.FileWrite` to the grant in protocol `Stream`: `role Cons needs IO.Console, IO.FileWrite`. The body then takes one `Cap` per granted capability, in the grant's order, between the session capability and the state, so it gains a parameter: `fn (s, cap_console, cap_file_write, st) -> ...`. Pass `cap_file_write` on to any function the body hands its capabilities to. Or remove the use.

21 |     let _ = file_write("/tmp/n", int_to_string(n))
                 ^^^^^^^^^^


    the body calls `cons` here:

33 |       fn (s, con, st) -> cons(s, con, st))
                              ^^^^

    `cons` calls `save` here:

27 |       save(n)
           ^^^^

    the body of role `Cons`, passed to `Stream_Run.run_Cons`:

33 |       fn (s, con, st) -> cons(s, con, st))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

    role `Cons` is granted only `Cap(IO.Console)` here:

9 |     role Cons needs IO.Console
        ^^^^^^^^^^^^^^^^^^^^^^^^^^
    run `march --explain role_grant_exceeded`

A role can carry its own capability grant. The file write is two calls deep, and the error traces the path from the role’s body to file_write, then shows the grant it breaks. The help writes out the widened role Cons needs line. It also gives the body’s new parameter list: the body takes one Cap for each capability in the grant, so widening the grant adds a parameter too.

9. Refinements

A refinement type adds a condition to a type, like {Int | _ >= 0} or {List(Int) | len(_) > 0}, and March proves those conditions at compile time with the z3 solver (see Refinement types). When a proof fails, the error gives a concrete counterexample, points at where the failing value came from, and writes the guard over your own names. When every argument of the failing call is a known value and the function does no I/O, the compiler also runs that call once in its interpreter and says what happens. These need z3, so the playground can’t run them; install March to try them.

An index that is out of range

mod Main do
  fn third() : Int do
    List.nth([1, 2, 3], 7)
  end

  fn main() : Int do
    third()
  end
end

-- REFINEMENT ------------------ index-out-of-range.march

refinement violation: index must be less than the list's length [refinement_violated]
argument `n` of `List.nth` does not satisfy precondition `_ < len(xs)`
note: `7` can never satisfy `n < len(xs)`; pass a value that does

3 |     List.nth([1, 2, 3], 7)
        ^^^^^^^^^^^^^^^^^^^^^^

    running `List.nth([1, 2, 3], 7)` panics: "List.nth: index out of bounds"
    `List.nth_opt` is `List.nth` without the requirement: it returns `Option` instead of panicking.
        match List.nth_opt([1, 2, 3], 7) do
          Some(v) -> …
          None -> …
        end

    `n` is `7` here:

3 |     List.nth([1, 2, 3], 7)
                            ^
    run `march --explain refinement_violated`

List.nth requires an index below the list’s length. The solver knows the literal list has three elements, so this call can never succeed, and the note says so. Every argument is a value, so the compiler also runs the call once in its interpreter and reports what happens: List.nth panics.

A guard that proves the opposite

mod Main do
  fn head_of(xs : {List(Int) | len(_) > 0}) : Int do
    match xs do
      Cons(h, _) -> h
      Nil        -> panic("empty")
    end
  end

  fn first_or_zero(ys : List(Int)) : Int do
    if List.length(ys) == 0 do
      head_of(ys)
    else
      0
    end
  end

  fn main() : Int do
    first_or_zero([1, 2, 3])
  end
end

-- REFINEMENT ---------------------- counterexample.march

refinement violation: argument `xs` of `head_of` does not satisfy precondition `len(_) > 0` [refinement_violated]
for example, when `ys` is `[]`
note: guard the call (e.g. `if len(ys) > 0 do head_of(ys) else … end`) or pass a value known to satisfy it

11 |       head_of(ys)
           ^^^^^^^^^^^

    running `head_of([])` panics: "empty"

    this argument must satisfy `len(ys) > 0`:

11 |       head_of(ys)
                   ^^

    `ys` comes from here:

9 |   fn first_or_zero(ys : List(Int)) : Int do
                       ^^

    the call is reached only when this is true:

10 |     if List.length(ys) == 0 do
            ^^^^^^^^^^^^^^^^^^^^
    run `march --explain refinement_violated`

Inside this branch ys is known to be empty, so the call fails whenever it runs. The counterexample (ys is []) shows when, the labels point at where ys comes from and at the condition that leads here, and the note suggests the guard that would make the call safe. Running head_of([]) shows the panic the guard prevents.

A return type that isn’t met

mod Main do
  needs IO.Console

  fn magnitude(n : Int) : {Int | _ >= 0} do
    if n < 0 do n else 0 end
  end

  fn main(_console : Cap(IO.Console)) do
    println(int_to_string(magnitude(-3)))
  end
end

-- REFINEMENT ------------------- return-refinement.march

`magnitude` does not satisfy its return type constraint on all code paths. [return_refinement_violated]

The return type requires:

    _ >= 0

but magnitude(-1) returns -1.

4 |   fn magnitude(n : Int) : {Int | _ >= 0} do
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

    Every branch must produce a return value satisfying `_ >= 0`.

The function body is checked against its own return type, and the counterexample is run: magnitude(-1) returns -1, a negative number.

A recursion that may not stop

mod Main do
  @[decreases(n)]
  fn down(n : Int) : Int do
    if n == 0 do 0 else down(n - 1) end
  end

  fn main() do
    down(3)
  end
end

-- WARNING: RECURSION ----------------- termination.march

`down` is not shown to terminate: the recursive call `down(n - 1)` is not shown to decrease `n`: e.g. n = -1 [termination_unproved]
note: the exit `n == 0` misses a negative `n`; `n <= 0` covers it.
note: a metric must stay at least 0 and fall at every recursive call (left to right, for several components). Otherwise refine the parameter (`{Int | _ >= 0}`), or write a metric that does fall.

4 |     if n == 0 do 0 else down(n - 1) end
                            ^^^^^^^^^^^

    run `march --explain termination_unproved`

This one is a warning (the program still compiles). It finds the input that never reaches the base case (n = -1) and suggests the one-character fix, n <= 0.

Division in a module that promised not to panic

mod Main do
  needs IO.Console
  cap no_panic

  fn scale(d : {v : Int | v * v >= 0}) : Int do
    10 / d
  end

  fn main(_console : Cap(IO.Console)) do
    println(int_to_string(scale(2)))
  end
end

-- REFINEMENT ------------------- division-no-panic.march

division by `d` in `cap no_panic` module: refinement does not rule out zero (e.g. d = 0). [division_by_zero]

Use `Math.checked_div` or `Math.checked_mod` to return `Option(Int)` instead of panicking, or annotate the divisor parameter with `{v : Int | v != 0}` (or `v > 0`) to prove it is safe.

6 |     10 / d
        ^^^^^^

    run `march --explain division_by_zero`

cap no_panic is a promise the module makes, so a divisor that might be zero is an error. The refinement on d holds for every integer, zero included, so it proves nothing. The message offers two ways out.

Dividing by a value from a pattern

mod Main do
  needs IO.Console
  cap no_panic

  type Stats = Stats(Int, Int)

  fn average(s : Stats) : Int do
    match s do
      Stats(total, count) -> total / count
    end
  end

  fn main(_console : Cap(IO.Console)) do
    println(int_to_string(average(Stats(10, 2))))
  end
end

-- REFINEMENT -------------------- division-pattern.march

division by `count` in `cap no_panic` module may be by zero — no refinement proves `count ≠ 0`. [division_by_zero]

`count` is not a function parameter, so no refinement annotation reaches it. Guard the division instead, which the checker reads as proof: `if count == 0 do <fallback> else ... / count end`. Or use `Math.checked_div` or `Math.checked_mod`, which return `Option(Int)` instead of panicking.

9 |       Stats(total, count) -> total / count
                                 ^^^^^^^^^^^^^

    run `march --explain division_by_zero`

Here the divisor comes out of a pattern, not a parameter, so there is no annotation to add. The message says so and gives the fix that always works: a guard. The checker reads if count == 0 do ... else ... end, so the division in the else branch is proved.

10. Performance: why a copy happens

March updates a list or a tree in place when the function rebuilding it holds the only reference to it. When something else still holds the value, the function allocates a new copy instead: the program is still correct, only slower. Nothing in an ordinary check says so, because nothing is wrong. march --why-copies is the report you ask for when you want to know. The playground only checks programs, so it can’t show this one.

A list that is used again after List.map

mod Main do
  needs IO.Console

  fn inc_all(xs : List(Int)) : List(Int) do
    let ys = List.map(xs, fn x -> x + 1)
    let n = List.length(xs)
    List.append(ys, [n])
  end

  fn main(_console : Cap(IO.Console)) do
    println(int_to_string(List.length(inc_all([1, 2, 3]))))
  end
end

-- WARNING: COPY ---------------------- copy-shared.march

`List.map` builds a new copy instead of reusing `xs` in place, because `xs` is used again afterwards. [copy_shared]
A function can update a value in place only when it holds the only reference to it; make this call the last use of `xs` and `List.map` reuses its memory instead of allocating.
help: move `let n = List.length(xs)` above the call.

5 |     let ys = List.map(xs, fn x -> x + 1)
                          ^^


    `xs` is used again here, so it is still shared when `List.map` runs:

6 |     let n = List.length(xs)
                            ^^

    fix (`forge fix` applies it):

4 |   fn inc_all(xs : List(Int)) : List(Int) do
5 +     let n = List.length(xs)
6 -     let n = List.length(xs)

    run `march --explain copy_shared`

List.map could have rewritten xs’s cells in place, but List.length(xs) on the next line still needs the old list, so it built a new one. The warning points at both lines and offers the fix: take the length first. The fix appears only when moving the later line is safe (it is the value’s only later use and has no side effects); forge fix can apply it. The same report names two other reasons a value stays shared: it is also passed to the enclosing call, or a closure captured it. See the memory model.

11. Run-time failures

Some mistakes only show when the program runs. march FILE reports them the way it reports a compile error: what happened, the line with a caret, and then each call that led there, innermost first. The playground only checks programs, so it can’t show these.

A panic two calls deep

mod Main do
  needs IO.Console

  fn price(code : String) : Int do
    match code do
    "a" -> 1
    _ -> panic("unknown product code: " ++ code)
    end
  end

  fn total(codes : List(String)) : Int do
    List.fold_left(codes, 0, fn (acc, c) -> acc + price(c))
  end

  fn main(_console : Cap(IO.Console)) do
    println(int_to_string(total(["a", "zz"])))
  end
end

-- RUNTIME ---------------------------------- panic.march

The program panicked: unknown product code: zz [panic]

7 |     _ -> panic("unknown product code: " ++ code)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

    Calls inside the standard library are left out; set MARCH_BACKTRACE=full to see them.

    `price` was called here:

12 |     List.fold_left(codes, 0, fn (acc, c) -> acc + price(c))
                                                       ^^^^^^^^

    `List.fold_left` was called here:

12 |     List.fold_left(codes, 0, fn (acc, c) -> acc + price(c))
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

    `total` was called here:

16 |     println(int_to_string(total(["a", "zz"])))
                               ^^^^^^^^^^^^^^^^^^

A compiled program prints the same header, headline and panic line. Below that it lists the functions the panic was reached through, each by its first line, because a compiled program doesn’t record the line of each call.

The first excerpt is the panic itself. Each one after it is a call on the way there: price was called from the function passed to List.fold_left, which total called, which main called. Calls inside the standard library are left out unless you set MARCH_BACKTRACE=full.

An actor that crashes

mod Main do
  needs IO.Console
  needs IO.Spawn

  actor Counter do
    state { n : Int }
    init { n: 0 }
    on Bump(k : Int) do
      if k < 0 do panic("negative bump") else { state with n: state.n + k } end
    end
  end

  fn main(_console : Cap(IO.Console), _spawn : Cap(IO.Spawn)) do
    let pid = spawn(Counter)
    send(pid, Bump(1))
    send(pid, Bump(-5))
    run_until_idle()
    println("done")
  end
end

-- RUNTIME ---------------------------- actor-crash.march

Actor `Counter` crashed while handling `Bump(-5)`: negative bump [actor_crashed]

9 |       if k < 0 do panic("negative bump") else { state with n: state.n + k } end
                      ^^^^^^^^^^^^^^^^^^^^^^

    Its state when it crashed: { n: 1 }
    Nothing supervises this `Counter`, so it stays dead and later messages to it are dropped. The rest of the program keeps running.

An actor’s crash doesn’t stop the program, so it would be easy to miss. The report names the actor, the message it was handling (with its arguments), where the handler failed, and the actor’s state at the time. It also says what happens next: nobody supervises this Counter, so it stays dead. A supervised actor is restarted by its supervisor instead, and no report is printed.

12. Test failures

A failing test is reported the same way, by march test and by forge test (which runs the tests compiled; both print the same report). These are run-time failures, not compiler errors, so the playground can’t show them: it only checks programs. Install March and run march test on the examples to try them.

An assert == that fails

mod Main do
  type Role = Admin | Guest | Owner(Int)
  type User = { name : String, tags : List(Role) }
  derive Eq, Show for Role
  derive Eq, Show for User

  pfn load_user() : User do
    { name: "ann", tags: [Admin, Owner(1), Guest] }
  end

  test "the loaded user" do
    let user = load_user()
    let expected = { name: "ann", tags: [Admin, Owner(2), Guest] }
    assert (user == expected)
  end
end

FAIL: "the loaded user"
-- TEST FAILURE ----------------------- assert-diff.march

The two sides of this `==` are not equal. [assert_failed]

14 |     assert (user == expected)
                 ^^^^^^^^^^^^^^^^

    left `user`
        User { name = ann, tags = [Admin, Owner(1), Guest] }
                                                ^
    right `expected`
        User { name = ann, tags = [Admin, Owner(2), Guest] }
                                                ^

    They first differ at `.tags[1]`.

Each side is labelled with the expression that produced it, and the carets mark where the two values first differ, not just that they differ. A value too long for one line is shown only along the path to the difference, with everything else as …; a list of the wrong length and a string that differs partway through are pointed at the same way.

A property that fails

mod Main do
  needs IO.Process, IO.Clock

  pfn total(a : Int, b : Int) : Int do
    a + b
  end

  test "sums stay under 50" do
    Check.all(Gen.tuple2(Gen.int(0, 100), Gen.int(0, 100)), fn pair ->
      match pair do
      (a, b) ->
        assert (total(a, b) < 50)
        true
      end
    )
  end
end

FAIL: "sums stay under 50"
-- TEST FAILURE ----------- property-counterexample.march

This property does not hold. [property_failed]

 9 |     Check.all(Gen.tuple2(Gen.int(0, 100), Gen.int(0, 100)), fn pair ->
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

    It failed on run 1 of 100.

    Smallest failing input (shrunk in 3 steps from `(98, 11)`):

        a = 39
        b = 11

    It failed this assertion:

    This `<` comparison is false. [assert_failed]

    12 |         assert (total(a, b) < 50)
                         ^^^^^^^^^^^^^^^^

        left `total(a, b)`
            50
        right
            50

    Seed 42: replay it with `forge test --seed=42`.

Check.all tries the property on 100 generated inputs. When one fails, it shrinks it to a smallest input that still fails and names each part by the property’s own parameters (a and b, which the match takes apart). Then it shows the failed assertion inside it. The seed reproduces the run: forge test --seed=42.

Error reference

Every code that has a march --explain page also has one on this site: