How are solved metas "revisited" in smalltt?

[VictorTaelin]

Suppose, for example, we want to type-check the following term:

main
: ∀(b: Bool) -> (if b then Nat else Char)
= λb -> (match b { true: <A>; false: <B> } : ?R)

Where <A> and <B> stand for arbitrary terms, and match performs the dependent elimination on bools. As we traverse this term in a conventional bidirectional type-checker, we'll see typed holes in the following order:

<A> : (?R true)
<B> : (?R false)
?R  : Bool -> *

Then, since the return type of main is (if b then Nat else Char), and since the dependent pattern-match returns (?R b), we'll have the following equation:

(if b then Nat else Char) = (?R b)

This satisfies all the requisites of pattern unification, giving us the substitution:

?R = λb (if b then Nat else Char)

So far, so good; my question is: what happens next? With this new knowledge, we would be able to substitute ?R for the found unification, and re-type-check the entire program. But this would wasteful. If I understand correctly, smalltt, a high-performance type theory elaborator by András Kovács, has a mechanism where <A> : (?R true) and <B> : (?R false) are frozen suspended, and, as soon as we know ?R, we're able to immediately go back, and check <A> : Nat and <B> : Char, respectively.

My question is: how this situation is handled? Will the type-checker just fail on <A> : (?R true), or will it suspend these problems and revisit them later? And, if that's the case, how is that implemented in a way that is more efficient than "re-checking" the whole program once R is solved?

Note: I've mirrored this question on StackExchange and will replicate the answer here when available.