@@ -849,6 +849,90 @@
849849:: %submitt [m(note="") ~]
850850:: ^
851851::
852+:: ===================================================================
853+:: 5. General checker core (design; not implemented yet)
854+:: ===================================================================
855+::
856+:: The existing inference and recovery paths are described in
857+:: docs/compiler.md. This section is a plan for replacing them, not a
858+:: claim that the current checker implements these rules. The Grammar and
859+:: Decisions are authoritative if this design needs adjustment.
860+::
861+:: 5.1 State and unification. Give each inference variable an identity and
862+:: a union-find entry: parent or binding, rank, level, source, rigidity,
863+:: and the atom, arithmetic-atom and gate-free obligations it carries.
864+:: Hoon's immutable maps hold the entries; operations return the updated
865+:: state. Find compresses paths in that returned state. Bind only after an
866+:: occurs check, merge obligations at roots, and lower levels throughout
867+:: the bound type to the root's level. A rigid written capital may acquire
868+:: allowed constraints but cannot be forced to a concrete type or a
869+:: different written capital. Keep origins for both sides of each fit so
870+:: a failure can show both excerpts. Recursive named molds retain their
871+:: identity; the occurs check is for inference variables, not a ban on
872+:: declared recursion.
873+::
874+:: A scheme quantifies eligible variables above the enclosing level;
875+:: instantiate with fresh variables and copy their obligations. Written
876+:: capitals respect their lexical scope, including sharing with a local
877+:: definition when the enclosing definition uses the same name. Retain
878+:: aura variables and directional aura fits, rather than turning every
879+:: fit into symmetric equality. At a faced position a capital binds the
880+:: type under the face; joining an unnamed position with a faced one keeps
881+:: the face, independently of the order of the inputs. Different explicit
882+:: faces conflict. No gate may hide inside a gate-free type, including in
883+:: a container; propagate the obligation through its arguments.
884+::
885+:: 5.2 Work queue. A constraint owns its source span, the types and
886+:: expression shape it depends on, and the information needed to report
887+:: failure. Tags and constructors, null, decimal and cell literals,
888+:: wings, changes, unface and unknown match subjects enter the same queue.
889+:: Index waiting constraints by the roots they read. Binding or merging a
890+:: root wakes its dependants; a retry either solves, fails with its sites,
891+:: or registers the roots still needed. Run to a fixed point, without
892+:: losing constraints when a root is redirected. Check patterns once the
893+:: subject is known. Contextual tags inspect case shapes and noun-equal
894+:: heads, retaining the named union and its site in diagnostics.
895+::
896+:: Variables reachable from an open tag constraint remain monomorphic
897+:: across definitions, so a later use, including main, can fix them.
898+:: Other eligible variables can generalize, with their atom and gate-free
899+:: obligations intact. At each definition boundary resolve its holes and
900+:: apply the specified decimal and cell defaults, without defaulting a
901+:: decimal whose definition is generic over its aura. A decimal fits @ud,
902+:: @u, @ and *; other concrete auras need their own literal. At module
903+:: completion retry the queue and report each still-open constraint at its
904+:: source; an unresolved tag asks for a ^-, never a guessed union.
905+::
906+:: 5.3 Definition order and kinds. Use the existing dependency graph's
907+:: strongly connected components in dependency order. Give a recursive
908+:: group of gates monomorphic placeholders, infer all members in one state,
909+:: solve what can be solved, then generalize together. Reject a cycle
910+:: involving a non-gate value, including one through a gate, and show the
911+:: cycle. Check a named definition's holes before later uses can fix them.
912+:: Infer main as an ordinary expression against ordinary prelude schemes;
913+:: only its resulting type determines library, page, island or store.
914+:: Afterwards check kind-specific invariants: recursively find the field
915+:: containing a gate in island data or a model, and inspect subscriptions
916+:: for watchability only at %watch. A page load may be any gate to ask,
917+:: including pure and typed paths. Preserve request provenance needed for
918+:: a watchability proof through ordinary calls and aliases.
919+::
920+:: 5.4 Matches and migration. A reusable usefulness matrix over noun
921+:: constructors, constants, cells and wildcards checks nested patterns;
922+:: loobeans, lists and units expand to their cases. Test an arm against
923+:: previous rows for usefulness, then test a wildcard for exhaustiveness;
924+:: keep a witness for a missing case and the covering arm's site for a
925+:: dead one. Recursive types require memoized specialization and a
926+:: terminating treatment of recursive states. The same matrix can later
927+:: drive lowering. The bare-name/tag spelling rule is checked against the
928+:: subject and the cases the rest of the pattern can match.
929+::
930+:: Migrate in small stages with eval and ship goldens for every change.
931+:: Keep diagnostics and source sites in the single full result; types.txt
932+:: is a rendering of that result. As general inference covers an existing
933+:: recovery or source-proven slice, remove that slice and retain its tests.
934+:: An unsupported construct fails closed at its own site until then.
935+::
852936|%
853937+| %positions
854938::
@@ -11307,7 +11391,7 @@
1130711391 `[entry u.rest]
1130811392::
1130911393
11310−+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
11394++$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
1131111395+$ iadj (map term (list term))
1131211396+$ ivisited (map term ?)
1131311397+$ iwork (list [name=term done=?])
@@ -11403,7 +11487,7 @@
1140311487++ add-groups
1140411488 |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
1140511489 ^- iresolved
11406− ?~ components [env grouped artifacts]
11490+ ?~ components [env grouped artifacts ~]
1140711491 =/ component=(list term) i.components
1140811492 ?. (graph-cycle component graph) $(components t.components)
1140911493 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
@@ -11447,8 +11531,10 @@
1144711531 `[[[name.d (cap-names typ vars caps.state.p.result sub.state.p.result)] env] checked artifacts]
1144811532++ add-supported-defs-core
1144911533 |= [ds=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
11450− ^- [env=ienv artifacts=(list iwidth-definition)]
11451− ?~ ds [env artifacts]
11534+ ^- [env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
11535+ =/ failures=(list [name=term diag=idiag]) ~
11536+ |-
11537+ ?~ ds [env artifacts (flop failures)]
1145211538 =/ d=def i.ds
1145311539 ?: ?=(%mold -.d) $(ds t.ds)
1145411540 ?. (unique-value-name name.d globals) $(ds t.ds)
@@ -11459,37 +11545,34 @@
1145911545 =. gate-defs.initial checked
1146011546 =. head-evidence.initial heads
1146111547 =. initial (reserve-def-caps val.d initial)
11462− =/ result=iresult (infer-fragment val.d env initial)
11548+ =/ plain=iresult (infer-fragment val.d env initial)
11549+ =/ result=iresult plain
1146311550 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11551+ ?: ?=(%| -.result)
11552+ =/ failure=idiag
11553+ ?: (definite-diag p.result) p.result
11554+ ?: ?=(%| -.plain) p.plain
11555+ p.result
11556+ =? failures (definite-diag failure) [[name.d failure] failures]
11557+ $(ds t.ds)
1146411558 =/ added=(unit iadded-definition)
1146511559 (add-supported-result d result initial env checked artifacts)
1146611560 ?~ added $(ds t.ds)
1146711561 $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
1146811562::
11469−:: Full checking discards unsupported definitions. On that failure path only,
11470−:: retry a bounded number of missing definitions to explain a pending tag
11471−:: from the same ordinary inference state instead of hiding it behind the
11472−:: generic completeness error. No successful definition takes this path.
11473−++ module-pending-tag
11474− |= [ds=(list def) env=ienv base=istate fuel=@ud]
11563+:: Retry one unresolved definition to explain a pending tag. The gate
11564+:: evidence is built from the whole module, not only this definition.
11565+++ module-pending-tag-one
11566+ |= [d=def env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence)]
1147511567 ^- (unit [at=span msg=tape])
11476− =/ checked=(map term def) (direct-checked-gates ds env)
11477− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.base)
11478− |-
11479− ?~ ds ~
11480− ?: =(0 fuel) ~
11481− =/ d=def i.ds
11482− ?: ?=(%mold -.d) $(ds t.ds, fuel (dec fuel))
11483− ?^ (ienv-lookup name.d env) $(ds t.ds, fuel (dec fuel))
11568+ ?. ?=(%value -.d) ~
11569+ ?^ (ienv-lookup name.d env) ~
1148411570 =/ initial=istate base(gate-defs checked, head-evidence heads)
1148511571 =. initial (reserve-def-caps val.d initial)
1148611572 =/ result=iresult (infer-fragment val.d env initial)
1148711573 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11488− ?: ?=(%| -.result) $(ds t.ds, fuel (dec fuel))
11489− =/ pending=(unit [at=span msg=tape])
11490− (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
11491− ?^ pending pending
11492− $(ds t.ds, fuel (dec fuel))
11574+ ?: ?=(%| -.result) ~
11575+ (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
1149311576::
1149411577++ resolve-groups-core
1149511578 |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
@@ -11505,12 +11588,12 @@
1150511588 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
1150611589 =/ ordered=(list def) (dependency-order ds components)
1150711590 |-
11508− =/ next=[env=ienv artifacts=(list iwidth-definition)]
11591+ =/ next=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
1150911592 (add-supported-defs-core ordered (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)
1151011593 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
1151111594 =. grec-index.initial index
1151211595 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
11513− ?: =(env env.out) out
11596+ ?: =(env env.out) out(failures failures.next)
1151411597 $(env env.out, grouped grouped.out, artifacts artifacts.out)
1151511598::
1151611599:: +dependency-order: the value definitions, dependencies first
@@ -12540,6 +12623,80 @@
1254012623 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
1254112624 |((lien (weld imported (weld vals mold-names)) reserved-name) (lien defs.mod reserved-def))
1254212625::
12626+:: A scope collision retains source sites. Prelude declarations may be in
12627+:: another source, so their name and namespace are retained separately.
12628++$ iscope-diagnostic
12629+ [issue=idiag prelude=(unit [name=term kind=?(%value %mold %any)])]
12630+++ scope-import-diagnostic
12631+ |= [imports=(list import) prelude-values=(list term) prelude-molds=(list term) seen=written-fields]
12632+ ^- (each written-fields iscope-diagnostic)
12633+ ?~ imports [%& seen]
12634+ =/ imp=import i.imports
12635+ =/ n=term
12636+ ?- -.imp
12637+ %jibb face.imp
12638+ %sur name.imp
12639+ %mark mark.imp
12640+ ==
12641+ ?: (reserved-name n)
12642+ [%| [["`{(trip n)}` is reserved and cannot be bound" ~[[at.imp "reserved name"]]] ~]]
12643+ =/ earlier=(unit span) (~(get by seen) n)
12644+ ?^ earlier
12645+ [%| [["import `{(trip n)}` shadows an earlier import" ~[[u.earlier "earlier import"] [at.imp "conflicting import"]]] ~]]
12646+ ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x))))
12647+ [%| [["import `{(trip n)}` shadows a prelude name" ~[[at.imp "conflicting import"]]] `[n %any]]]
12648+ $(imports t.imports, seen (~(put by seen) n at.imp))
12649+++ scope-def-diagnostic
12650+ |= [defs=(list def) imports=written-fields prelude-values=(list term) prelude-molds=(list term) values=written-fields molds=written-fields]
12651+ ^- (unit iscope-diagnostic)
12652+ ?~ defs ~
12653+ =/ d=def i.defs
12654+ =/ n=term name.d
12655+ ?: (reserved-name n)
12656+ `[["`{(trip n)}` is reserved and cannot be bound" ~[[at.d "reserved name"]]] ~]
12657+ =/ imported=(unit span) (~(get by imports) n)
12658+ ?^ imported
12659+ `[["definition `{(trip n)}` shadows an import" ~[[u.imported "import"] [at.d "conflicting definition"]]] ~]
12660+ =/ seen=written-fields ?:(?=(%value -.d) values molds)
12661+ =/ earlier=(unit span) (~(get by seen) n)
12662+ ?^ earlier
12663+ `[["definition `{(trip n)}` shadows an earlier definition" ~[[u.earlier "earlier definition"] [at.d "conflicting definition"]]] ~]
12664+ =/ prelude-names=(list term) ?:(?=(%value -.d) prelude-values prelude-molds)
12665+ ?: (lien prelude-names |=(x=term =(n x)))
12666+ `[["definition `{(trip n)}` shadows a prelude name" ~[[at.d "conflicting definition"]]] `[n ?:(?=(%value -.d) %value %mold)]]
12667+ ?: ?=(%value -.d)
12668+ $(defs t.defs, values (~(put by values) n at.d))
12669+ $(defs t.defs, molds (~(put by molds) n at.d))
12670+++ module-scope-diagnostic
12671+ |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12672+ ^- (unit iscope-diagnostic)
12673+ =/ imports=(each written-fields iscope-diagnostic)
12674+ (scope-import-diagnostic imports.mod prelude-values prelude-molds ~)
12675+ ?: ?=(%| -.imports) `p.imports
12676+ (scope-def-diagnostic defs.mod p.imports prelude-values prelude-molds ~ ~)
12677+++ show-scope-diagnostic
12678+ |= [file=path src=@t diagnostic=iscope-diagnostic prelude=(unit ifile)]
12679+ ^- @t
12680+ =/ excerpts=(list @t)
12681+ %+ turn sites.issue.diagnostic
12682+ |= site=[at=span note=tape]
12683+ (show-error src [file line.beg.at.site col.beg.at.site note.site])
12684+ =/ previous=(list @t)
12685+ ?~ prelude.diagnostic ~
12686+ ?~ prelude ~
12687+ ?~ source.u.prelude ~
12688+ =/ parsed (parse at.u.prelude u.source.u.prelude)
12689+ ?: ?=(%| -.parsed) ~
12690+ =/ matching=(list def)
12691+ %+ skim defs.p.parsed
12692+ |= d=def
12693+ ?& =(name.d name.u.prelude.diagnostic)
12694+ |(=(%any kind.u.prelude.diagnostic) =(-.d kind.u.prelude.diagnostic))
12695+ ==
12696+ ?~ matching ~
12697+ ~[(show-error u.source.u.prelude [at.u.prelude line.beg.at.i.matching col.beg.at.i.matching "prelude declaration"])]
12698+ (of-wain:format [(crip msg.issue.diagnostic) (weld excerpts previous)])
12699+::
1254312700++ module-scope-valid
1254412701 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
1254512702 ^- ?
@@ -12970,6 +13127,31 @@
1297013127 ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
1297113128 `[u.name at.s]
1297213129::
13130+:: Select the first available reason in dependency order, rather than
13131+:: preferring one class of diagnostic across the whole module. Only the
13132+:: first 64 definitions are retried for pending tags, as before.
13133+++ module-unresolved-diagnostic
13134+ |= [ds=(list def) env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence) failures=(list [name=term diag=idiag]) values=(list term) file=path src=@t fuel=@ud]
13135+ ^- (unit @t)
13136+ ?~ ds ~
13137+ =/ d=def i.ds
13138+ =/ remaining=@ud ?:(=(0 fuel) 0 (dec fuel))
13139+ ?: ?=(%mold -.d) $(ds t.ds, fuel remaining)
13140+ ?^ (ienv-lookup name.d env) $(ds t.ds, fuel remaining)
13141+ =/ found=(list [name=term diag=idiag])
13142+ (skim failures |=(failure=[name=term diag=idiag] =(name.failure name.d)))
13143+ ?^ found `(show-inference-diagnostic file src name.d diag.i.found)
13144+ =/ pending=(unit [at=span msg=tape])
13145+ ?: =(0 fuel) ~
13146+ (module-pending-tag-one d env base checked heads)
13147+ ?^ pending
13148+ `(show-error src [file line.beg.at.u.pending col.beg.at.u.pending msg.u.pending])
13149+ =/ shadow=(unit [name=term at=span]) (module-sample-shadow ~[d] env values)
13150+ ?^ shadow
13151+ =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
13152+ `(show-error src [file line.beg.at.u.shadow col.beg.at.u.shadow msg])
13153+ $(ds t.ds, fuel remaining)
13154+::
1297313155:: Cache only completed interfaces for this invocation. The source bundle,
1297413156:: imported Hoon types and prelude are fixed for the whole graph. Check the
1297513157:: active path and duplicate sources before consulting it, so a cache hit
@@ -14230,7 +14412,7 @@
1423014412 ?~ recovered ~
1423114413 ?. ?=(~ vars.u.recovered) ~
1423214414 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14233− `[env.u.added grouped.resolution artifacts.u.added]
14415+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1423414416::
1423514417++ program-inferred-slot
1423614418 |= [typ=itype name=(unit term)]
@@ -14386,7 +14568,7 @@
1438614568 ?~ recovered ~
1438714569 ?. ?=(~ vars.u.recovered) ~
1438814570 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14389− `[env.u.added grouped.resolution artifacts.u.added]
14571+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1439014572::
1439114573+$ iview-site [xs=expr mapper=term]
1439214574++ program-view-site
@@ -14713,7 +14895,7 @@
1471314895 ?~ recovered ~
1471414896 ?. ?=(~ vars.u.recovered) ~
1471514897 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14716− `[env.u.added grouped.resolution artifacts.u.added]
14898+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1471714899::
1471814900:: Recover exactly one direct keyed each/turn row mapper, then its view.
1471914901:: The prelude's own each and turn schemes determine the mapper gate: the
@@ -14935,7 +15117,7 @@
1493515117 ?~ recovered ~
1493615118 ?. ?=(~ vars.u.recovered) ~
1493715119 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14938− `[env.u.added grouped.resolution artifacts.u.added]
15120+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1493915121::
1494015122:: The model a direct program's initializer must produce. Update's written
1494115123:: two-item sample gives it when it can be read. Otherwise main's own program
@@ -15092,7 +15274,7 @@
1509215274 ?~ recovered ~
1509315275 ?. ?=(~ vars.u.recovered) ~
1509415276 ?. ?=(~ (itype-vars typ.u.recovered)) ~
15095− `[env.u.added grouped.resolution artifacts.u.added]
15277+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1509615278::
1509715279++ derived-poke-command-scheme
1509815280 |= [prelude=ifile action=itype]
@@ -15260,9 +15442,9 @@
1526015442 (direct-prelude-evidence ds prelude.initial)
1526115443 ?~ heads resolution
1526215444 =/ checked=(map term def) (direct-checked-gates ds env.resolution)
15263− =/ completed=[env=ienv artifacts=(list iwidth-definition)]
15445+ =/ completed=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
1526415446 (add-supported-defs-core ~[main] checked heads env.resolution molds.initial globals.initial externals.initial surs.initial mark-externals.initial marks.initial jimports.initial reserved-molds.initial at.initial prelude.initial artifacts.resolution grec-index.initial)
15265− [env.completed grouped.resolution artifacts.completed]
15447+ [env.completed grouped.resolution artifacts.completed failures.resolution]
1526615448::
1526715449:: A static main may retain a generic element message in its ordinary
1526815450:: scheme. Instantiate that scheme, specialize it to canonical element !!,
@@ -15478,6 +15660,9 @@
1547815660 !(lien prelude-molds |=(m=term =(m n)))
1547915661 ==
1548015662 ==
15663+ =/ scope=(unit iscope-diagnostic)
15664+ (module-scope-diagnostic mod(defs ordinary, imports faces) prelude-values prelude-molds)
15665+ ?^ scope [%| [(show-scope-diagnostic at src u.scope prelude) ~]]
1548115666 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1548215667 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
1548315668 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
@@ -15526,6 +15711,9 @@
1552615711 =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
1552715712 =/ checking=module mod(defs ds)
1552815713 ?. (module-scope-valid checking prelude-values prelude-molds)
15714+ =/ scope=(unit iscope-diagnostic)
15715+ (module-scope-diagnostic checking prelude-values prelude-molds)
15716+ ?^ scope [%| [(show-scope-diagnostic at src u.scope prelude) ~]]
1552915717 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1553015718 =/ vals=(list term) (global-value-names ds)
1553115719 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
@@ -15601,15 +15789,14 @@
1560115789 ?~ store-parts ds
1560215790 (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
1560315791 ?. (module-values-complete required env)
15604− =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
15605− ?^ pending
15606− [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]
15607− :: A shadowing sample is an error, so it comes before any named value.
15792+ =/ components=icomponents (graph-components required (global-value-names required))
15793+ =/ ordered=(list def) (dependency-order required components)
1560815794 =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))
15609− =/ shadow=(unit [name=term at=span]) (module-sample-shadow required env values)
15610− ?^ shadow
15611− =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
15612− [%| [(show-error src [at line.beg.at.u.shadow col.beg.at.u.shadow msg]) ~]]
15795+ =/ checked=(map term def) (direct-checked-gates required env)
15796+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence required prelude.state)
15797+ =/ diagnostic=(unit @t)
15798+ (module-unresolved-diagnostic ordered env state checked heads failures.resolution values at src 64)
15799+ ?^ diagnostic [%| [u.diagnostic ~]]
1561315800 =/ missing=(unit term) (module-missing-value required env)
1561415801 =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
1561515802 [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]