egraphs-good / egglog

egraphs + datalog!
https://egraphs-good.github.io/egglog/
MIT License
459 stars 54 forks source link

Infer types of functions values based on names #400

Closed saulshanabrook closed 3 months ago

saulshanabrook commented 3 months ago

Previously, the type inference for creating function values with (unstable-fn <name> [<partial arg>]*) did not use the name. It would only use the context within which the function was created to infer the type of the function.

This works fine if you only have one function sort defined or if always can infer it based on its calling location. However, I was noticing in my usages of unstable-fn I would often be passing another function reference as a partial arg. This means it would be hard for the type checker to figure out what type to use for these, so it would just give up and fail.

In this PR, I extend the type inference for functions to use the string name. If it is a literal value that shows up during type checking and we can find it in the function table, we use this to help infer what the types are. We can then narrow down both the partial arg types and also make sure that the output and inputs to the function are the same as those of the UnstableFn sort. If not, then we know that this constructor won't match.

The main change I had to do to implement this was to pass the TypeInfo into the accept method of TypeConstraints, so that we could lookup the function name.

I also had to add a new ImpossibleConstraint error for when a function is constructed with a string that doesn't match the function sort.