Unification using unification-fd

[chrisdone-artificial]

This swaps out specifically the unifier codepath of Hell with unification-fd's ST-based unifier.

chris@linux:~/Work/chrisdone/hell$ ./hell-status-quo --check /home/chris/Work/artificialio/brossa-infra/.github/workflows/scripts/summarise.hell --compiler-stats
  stat: read_file = 68.75 μs
  stat: parse_module_with_mode = 16.34 ms
  stat: resolve_module = 72.12 μs
stat: parse = 16.60 ms
stat: cycle_detect = 65.45 ms
stat: desugar = 54.18 ms
  stat: elaborate = 1.590 ms
  stat: unify = 638.1 ms
  stat: zonk = 688.6 ms
stat: infer = 1.328 s                 ###################
stat: check = 2.804 ms

chris@linux:~/Work/chrisdone/hell$ ./hell-ufd --check /home/chris/Work/artificialio/brossa-infra/.github/workflows/scripts/summarise.hell --compiler-stats
  stat: read_file = 114.2 μs
  stat: parse_module_with_mode = 29.61 ms
  stat: resolve_module = 79.21 μs
stat: parse = 30.09 ms
stat: cycle_detect = 63.70 ms
stat: desugar = 62.56 ms
  stat: elaborate = 3.719 ms
  stat: unify-and-zonk = 270.5 ms     ###################
stat: infer = 274.4 ms
stat: check = 2.561 ms

Remaining:

• Map the error type (UFailure) back to error messages
• Collapse the verbose code of 8 functions into one function
• (Optionally) Move the elaborator into unification-fd's STBinding monad, to skip the mapping between frozen and thawed meta variables. Asymptotics may moot this though.

[chrisdone-artificial]

I'm not sure that I like it that much. Will come back to it another time.