bolt/rules/laws/unsafe.bend fails

raw source on the hub · import 0x729eecea86ea5a2cdba3a2856a313bca/bolt/rules/laws/unsafe.bend as Unsafe

rule unsafe (project-wide): an @unsafe def that a LAWS.bend or PROOF.bend reaches by relative imports, over the files bolt read. The checker skips its termination check, prints "All terms check, but N defs rely on unsafe or foreign code:" (2.0.16: "with N unsafe annotation(s).") and exits 0, so a gate that only reads the exit status goes green on a proof that is not sound (a def that never returns proves anything). Recurse on a shrinking argument, or on a fuel, and drop the @unsafe; or keep the def out of what the laws import. An @unsafe def no law file reaches is not this rule's business. The rule reads each file's digest (bolt/rules/digest.bend), and takes every closure over one import graph.

4 imports

import Base
import ../../finding.bend as F
import ../digest.bend as Digest
import ../imports.bend as Imports

The reader could not load this file (at 0x729eecea86ea5a2cdba3a2856a313bca/bolt/config.bend:31). What bend.ts says:

Error:
- expected : a fresh name (duplicate declaration: Set)
- observed : 'Set'
Location:
30 | # a name (a group's or a rule's) at a level
31>| type Set is Data:
   |      ^^^
32 |   Set{name: String, level: Level}