Error reference

Every error Velaris can give — scraped from the compiler source itself, so this page cannot go stale. Braces are filled with your program’s names and values; every error also arrives with numbered fixes, and as JSON with --json.

CodeMessage template
E000unexpected character {source[pos]!r}
E001cannot find file '{path}'
E002unknown escape '\\{e}' in text
E100expected '{want}' but found '{t.text or 'end of file'}'
E101unexpected '{t.text}'
E200'{ns}' has no function called '{fname}'
E300function '{fn.name}' calls '{node.name}' which needs effect '{eff}', but '{fn.name}' {declared}
E310the '{where}' promise of '{fn.name}' calls '{node.name}' which has effects ({', '.join(sorted(eff))}); promises must be pure
E400no 'main' function found
E401'{node.name}' expects {len(ptypes)} argument(s) but got {len(node.args)}
E402a function value cannot use '{node.name}' from the code around it
E403remainder by zero
E405random(n) needs n greater than 0
E406this text has {holes} placeholder(s) but got {given} value(s)
E407this arithmetic made a number too big to hold (whole numbers go from {INT_MIN} to {INT_MAX})
E408an exit code must be between 0 and 255, not {code}
E500unknown type '{ftype}' for field '{fname}' of record '{r.name}'
E501'{node.name}' is declared {node.ann}, but this is an empty {'list' if empty_list else 'map'}
E502argument {i} of '{node.name}' is a call to a function that returns nothing
E503'{fn.name}' promises to return {declared_ret} but this return gives nothing
E504'while' needs a yes/no condition (Bool), but this is {c}
E505'invariant' must be a yes/no promise (Bool)
E506cannot tell what an empty list holds
E507'{r.name}' is used for both a record and a function
E508unknown record '{node.name}'
E509record '{node.name}' is missing field(s): {', '.join(missing)}
E510record '{t}' has no field '{node.field}'
E511records cannot be changed in place
E512cannot find imported file '{path}'
E513function '{f.name}' is defined in both '{fn_src[f.name]}' and '{path}'
E514'{name}' is the name of an import, so it cannot also be a variable
E520'get' on a map can fail - the key may be missing, and that cannot be ignored
E521'try' passes failure up, but '{fn.name}' cannot fail
E522'{node.subject.name}' cannot fail - call it directly, no check needed
E523'fail' is used, but '{fn.name}' does not declare it can fail
E524'main' cannot be 'or fail' - there is no one above it to handle the failure
E525'{node.subject.name}' returns nothing - write 'ok {{ ... }}' with no name
E530'{f2.name}' uses effects ({', '.join(sorted(f2.effects))}) - only pure functions can be passed as values
E540type variable '{tv}' must appear in at least one parameter (a {tv} only in the return type cannot be inferred)
E541type variable '{tv}' shadows a real type
E542'{node.name}' argument {i} should look like {want}, but this is {got}
E543'{f2.name}' is generic - generic functions cannot be passed as values yet
E600broken promise: {nice_name(name)} requires {expr_str(expr)} ({vals(expr)})
E601broken promise: {nice_name(name)} ensures {expr_str(expr)} ({vals(expr, (retval,))})
E602position {i} is outside the text (it has {len(t)} character(s))
E607this text grew too large to build
E609cannot split by empty text
E700promise cannot be kept: {nice_name(fn.name)} ensures {expr_str(ens_expr)} - proven without running the program: {vals} gives result = {rv}
E701this call can break a promise: '{fnB.name}' requires {expr_str(r_expr)}, but '{ctx.caller}' can call it with {vals} - proven without running the program
E703cannot prove the loop keeps 'invariant {expr_str(inv_expr)}' {where} in '{ctx.caller}' - the promises allow: {vals}
E704loop broke its promise: invariant {expr_str(inv_expr)} ({vals})
E705this 'get' can reach position {m.eval(idx, model_completion=True)}, but the list has {m.eval(length, model_completion=True)} item(s) - proven without running the program
E706this can {word} zero
E999self-test failed