Basically I keep thinking that I'm writing an inference engine for this shit anyway, and polonius is doing basically that too, so why not just straight up stick a logic programming engine into the compiler and write my type checker and borrow checker in datalog or prolog?
The main barriers to this are:
Per zjcurtis: "Prolog in a compiler dep is a good way to have a slow compiler". Datalog seems much more practical though. His recommendations:
As a simple approach, you could basically turn the type (or borrowing) part of a Garnet program into datalog, and then if the datalog program doesn't error then your program is well-typed. So it sounds like problems 1 and 3 are solved at least, and there's somewhere to start for problem 2.
Oh, also, my type system is basically 1ML, and 1ML can be lowered to System Fω. There are probably implementations of System Fω's rules out there in Prolog, so if I find a good one maybe I can port it to datalog and use that as a basis.
Ok I've made a proof of concept here: https://hg.sr.ht/~icefox/pancake. It doesn't work though, because Datalog can't really create new data, just query the data that is already there. So instantiating new types via substitution requires basically "shelling out" to the host language, generating more Datalog rules, and either rerunning the query or picking up where you left off. And that Feels Bad and I really kinda don't want to do that.
I grappled with this for a while, then read https://dl.acm.org/doi/10.1145/3428195 which ran into the exact same problem and said "we solved this by shelling out to the host language, generating more Datalog rules, and picking up where we left off". I'm happy that I'm not stupid, at least, and this approach may be worth picking up again in the future. Putting a datalog impl into the compiler might still be useful for borrow checking or property resolution, so.
Okay. This is 100% possible if I really want to. But I'm not going to do it right now.