LDC-E8101 — Construct above the declared layer

What it means

A package can declare a layer ceiling, and every construct in it must fit under that ceiling. The layer of a program is inferred from the constructs it actually uses: plain computation stays at the bottom, defaults and exceptions sit one step up, and conflict consumption — reasoning that reads the support status of a claim — belongs to the top layer. When the inference rises above the declared ceiling, the compiler stops at the construct that raised it and names the lowest layer that would accept it.

The ceiling is one-sided: declaring a higher layer than the program needs is never an error. Either raise the declared ceiling to the named layer or rewrite the construct so it stays within the declared one.

Example

run

{"argv": ["check", "$ROOT/example.law", "--layer", "L0"], "files": {"example.law": "language \"law.core\" version \"0.2\";\npackage probe.layer version \"0.1.0\";\nnamespace \"urn:law:probe:layer\";\n\nrelation disputed(subject: Text) kind institutional;\n\nrelation contested(subject: Text) kind institutional;\n\nrule Contested strict {\n    for v0: Text;\n    when supported(disputed(v0));\n    then contested(v0);\n}\n"}, "expect": "LDC-E8101"}

Fix

run

{"argv": ["check", "$ROOT/example.law", "--layer", "L3"], "files": {"example.law": "language \"law.core\" version \"0.2\";\npackage probe.layer version \"0.1.0\";\nnamespace \"urn:law:probe:layer\";\n\nrelation disputed(subject: Text) kind institutional;\n\nrelation contested(subject: Text) kind institutional;\n\nrule Contested strict {\n    for v0: Text;\n    when supported(disputed(v0));\n    then contested(v0);\n}\n"}, "expect": null}

Engine message

The engine reports this in its own wording:

Output

$ROOT/example.law:11:10: error LDC-E8101: conflict consumption `supported` requires layer L3 (contentious — dispute), but the package declares L0: raise `semantic_layer` or rewrite the construct within the layer

Related

• LDC-E8102 — the neighbouring layer refusal.