type.mismatch

A value of one type is used where a different type is required.

Area 2, Values and types; not declinable; the next step is usually the agent's.

Why Jadpo refuses it

Every named type says what its values mean and which rules they follow. A value can stand in only for its own type, or for a type it builds on. Going the other way, such as from a plain Int to a Stock, always goes through a constructor, which checks the target's rules, so a value never takes on a type whose rules nobody checked.

What it looks like

main.jadpo:

type Stock = Int {    min: 0}function add(a: Stock, b: Stock) -> Stock {    return a + b}

  |6 |     return a + b  |            ^^^^^ this is `Int`

(agent) at the end of the next: line means your coding agent can make the fix itself.

Where an object is required, the error shows its shape and the value written out. A text goes in the one field the object must have, as an edit your coding agent can apply, and a standard type's page is one command away:

function author() -> PersonName {    return "Frank Herbert"}

  |2 |     return "Frank Herbert"  |            ^^^^^^^^^^^^^^^ the wrong kind of value

A second error with the same reason keeps its place and its own edit, and its reason: says As the first `type.mismatch` above. jadpo check --full writes every reason out, and --json gives the place of the first in sameAs.

How to fix it

If the value should become the required type, convert it with that type's constructor:

    return Stock(a + b)

The sum is checked against Stock's rules. Here that check can't fail: a and b are never below zero and Stock has no maximum, so their declared ranges prove the sum is a valid Stock. When nothing proves it, the construction starts with attempt and says what happens when it fails.

Related

• Creating values
• Construction failures by rule
• When one type can stand in for another
• Named types