dijkstracula / irving

there's no checking like bounded model checking
GNU Affero General Public License v3.0
1 stars 0 forks source link

Typechecker: second pass to substitute SortVars with their concrete Sorts? #46

Closed dijkstracula closed 1 year ago

dijkstracula commented 1 year ago

The original plan was to have the inference pass mutate the AST as it eagerly unifies sorts. However, this seems to be slightly brittle and conflates the thing we want to do now (typechecking) with what we want to do later (know the concrete instantiation of some program term).

Might be easier to just take a final pass after inference; for every symbol, and the Resolver bindings that we've accumulated in the first pass, patch everything up.

dijkstracula commented 1 year ago

1c3ad72.