Infer types of functions values based on names

[saulshanabrook]

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.

[yihozhang]

Looks great!

[yihozhang]

Are there cases where the first argument is not a string? Like can you write programs like

(relation fns (String))
(fns "+")
(fns "-")
(fns "*")
(fns "/")
(rule ((fns op) (= v (unstable-app (unstable-fn op) 1 2))) ((extract v)))

I think it is not unfair to disallow programs like this and enforce the first argument to be a string literal.

[yihozhang]

Also, if the function is a primitive, it seems we cannot do much here, which is a pity.

[saulshanabrook]

Yeah I kept support for when the first argument is not a string... I don't think it's important but it felt easier to keep supporting it then disallow it. And you can still get some type checking with it, just not based on the name.

And yes you are right, we don't support type checking with primitives... we could hard code those or try something more creative but I don't think it's necessary at the moment. I personally never refer to primitives functions directly like that and if you do, again, it is still supported just won't infer based on the name.