Open eddyb opened 6 years ago
At the moment, the chalk-engine crate doesn't know anything about unification, but I had indeed always hoped to move unification into chalk, and compile it down to some sort of opcodes. I've also toyed with the idea of factoring out the unification code into a separate library for the time being. Anyway, I don't think we need to block experiments in Rust on that basis.
But what exactly is the motivation here? To find non-matching trees faster? That could potentially be useful in impl matching, I suppose, but I don't think in many other contexts?
I've also wanted to try the algorithm described here, which basically creates a decision tree that can be walked to simultaneously extract matching values and find mismatches.
Instead of zipping two trees and using the same unification procedure as the rest of inference, the "pattern" type could be turned into linear "instruction stream" for a matcher ("interpreter"), to walk the type "tree", first to check that the type actually matches and then to unify variables (if any).
E.g for.
Result<Vec<$0>, io::Error>
, it would check theResult
,Vec
andio::Error
heads, and for($0, $0)
it could equate the pair elements, before unifying a type with$0
, in both cases.This could also apply to Chalk, but I'm less familiar with its internal representation. cc @nikomatsakis @sunjay