Handle kind-inference of unkown builtins more gracefully #5899
Conversation
|
Rather than ignoring names that fail checking, we should exclude from names that aren't present from starting a check at all; dunno where that spot might be though (not sure if that's different from the thing you said wouldn't work) |
32e5f2e to
bb91f3e
Compare
I agree, unfortunately it'd take a fair bit of work to untangle that thread far enough. We can invest it if it's a priority though. Here's as far as I've untangled things:
We're inferring the kind of all decls in the typechecker context; but I think the typechecker context contains a lot of stuff, the code that builds it is pretty expansive and tough to understand at a quick glance, it seems to do a bunch of fuzzy matching on things that might be relevant for TDNR. TBH we should probably rewrite this to either be more precise so we don't include a bunch of unused stuff, or preferably to defer things like kind inference until we know we actually want it; e.g. when we're actually trying TDNR. It's possible to do all of this better, but most of this code hasn't been touched in ages and I'm not familiar with it, so it'd take a good while to page in I think, and is touchy to mess with 😓 . |
|
I made a naive first attempt at omitting things here: 9fdfa06 but it didn't actually work, so the |
Overview
Addresses, but doesn't fully solve: #5896
Previously:
Now:
Implementation notes
GenandSolvemonads so we can properly handle errors triggered there.Test coverage
Loose ends
It would be nice to simply ignore definitions which trigger kind checking errors during TDNR; but with the way things are arranged it's quite tricky to separate things.
I think what's happening is we're somewhere collecting all possible matching names, then we infer kinds for all decls and terms which we might possibly reference; before we even do the initial typecheck and before we get to TDNR proper.
I'm not familiar with how the kind checker works, so it may not be so easy as to just cull anything that fails checking, since there are inter-dependencies on kinds between things, e.g. if I cull a type I need to make sure I correctly cull everything which refer to the unification variables in that culled type since they now may never be solved;