Unifier: remove unnecessary child unifiers
A child unifier is necessary for (1) backtracking, and (2) keeping track
of whether postponed metas were introduced to decide whether to insert a
coercion.
Jon Sterling
(Apr 4, 2026, 1:05 PM +0100)
89eb95ce
e28a7b97
+17
-25
+17
-25
Sources/PterodactylCore/Unification/Unifier+Rules.swift
+17
-25
Sources/PterodactylCore/Unification/Unifier+Rules.swift
···
14
14
let app_x = Value.Frame.app(x)
15
15
let lhs_x = lhs.plug(frame: app_x)
16
16
let rhs_x = rhs.plug(frame: app_x)
17
-
var child = childUnifier() { $0.bind() }
18
-
try await child.unify(value: lhs_x, with: rhs_x, in: fam_x)
19
-
try await child.state.commit(&state)
17
+
18
+
try await locally { $0.bind() } do: { unifier throws(UnifyError) in
19
+
try await unifier.unify(value: lhs_x, with: rhs_x, in: fam_x)
20
+
}
20
21
21
22
case .recordType(let fields):
22
23
var runningFieldImplsLhs: OrderedDictionary<String, Value> = [:]
···
164
165
try await domUnifier.state.commit(&state)
165
166
166
167
let x1 = fresh(type: dom1)
167
-
var famUnifier = childUnifier() { $0.bind() }
168
-
169
-
let x2 = domUnifier.state.postponed.isEmpty ? x1 : coerce(typedValue: TypedValue(type: dom1, value: x1), to: dom2)
170
-
let fibre1 = fam1.instantiate(with: x1)
171
-
let fibre2 = fam2.instantiate(with: x2)
172
-
173
-
try await famUnifier.unify(type: fibre1, with: fibre2)
174
-
try await famUnifier.state.commit(&state)
168
+
try await locally { $0.bind() } do: { famUnifier throws(UnifyError) in
169
+
let x2 = domUnifier.state.postponed.isEmpty ? x1 : coerce(typedValue: TypedValue(type: dom1, value: x1), to: dom2)
170
+
let fibre1 = fam1.instantiate(with: x1)
171
+
let fibre2 = fam2.instantiate(with: x2)
172
+
try await famUnifier.unify(type: fibre1, with: fibre2)
173
+
}
175
174
176
175
case let (.recordType(fields: fields1), .recordType(fields: fields2)):
177
176
let error = UnifyError.conflict
···
226
225
case (.global(let meta1, .flex), .global(let meta2, .flex)):
227
226
228
227
func caseLt() async throws(UnifyError) {
229
-
var child = childUnifier()
230
-
try await child.solve(metaName: meta2, spine: neutral2.spine, rhs: .shrink(size: size2, type: .decode(size1, neutral1)))
231
-
try await child.state.commit(&state)
228
+
try await solve(metaName: meta2, spine: neutral2.spine, rhs: .shrink(size: size2, type: .decode(size1, neutral1)))
232
229
}
233
230
234
231
func caseGt() async throws(UnifyError) {
235
-
var child = childUnifier()
236
-
try await child.solve(metaName: meta1, spine: neutral1.spine, rhs: .shrink(size: size1, type: .decode(size2, neutral2)))
237
-
try await child.state.commit(&state)
232
+
try await solve(metaName: meta1, spine: neutral1.spine, rhs: .shrink(size: size1, type: .decode(size2, neutral2)))
238
233
}
239
234
240
235
switch await compare(size: size1, with: size2) {
···
422
417
)
423
418
)
424
419
}
425
-
var child = childUnifier()
426
-
try await child.unify(value: .shift(neutral1), with: .shift(neutral2), in: .levelType)
420
+
try await unify(value: .shift(neutral1), with: .shift(neutral2), in: .levelType)
427
421
default:
428
422
throw UnifyError.size
429
423
}
···
496
490
try await assertSize(type: dom, size: size)
497
491
let x = fresh(type: dom)
498
492
let fibre = fam.instantiate(with: x)
499
-
var child = childUnifier() { $0.bind() }
500
-
try await child.assertSize(type: fibre, size: size)
501
-
try await child.state.commit(&state)
493
+
try await locally { $0.bind() } do: { unifier throws(UnifyError) in
494
+
try await unifier.assertSize(type: fibre, size: size)
495
+
}
502
496
503
497
case let .recordType(fields: fields):
504
498
var fieldSpecs: OrderedDictionary<String, Value.FieldSpec> = [:]
505
499
for (key, spec) in fields {
506
500
if spec.manifest == nil {
507
501
let prefixRecord = fresh(type: Value.Type_.recordType(fields: fieldSpecs))
508
-
var child = childUnifier()
509
-
try await child.assertSize(type: spec.type.instantiate(with: prefixRecord), size: size)
510
-
try await child.state.commit(&state)
502
+
try await assertSize(type: spec.type.instantiate(with: prefixRecord), size: size)
511
503
}
512
504
513
505
fieldSpecs[key] = spec