It occurs to me that our universal quantification step rather expects to know the type which is being universally quantified. But, in some cases, there may be variables present in this type. I am specifically concerned about inference of the parameter types for fn expressions. It's possible that we do something wrong there, though I can't say specifically what, so this issue is kind of a mental note to come back to this and think about it.
It occurs to me that our universal quantification step rather expects to know the type which is being universally quantified. But, in some cases, there may be variables present in this type. I am specifically concerned about inference of the parameter types for fn expressions. It's possible that we do something wrong there, though I can't say specifically what, so this issue is kind of a mental note to come back to this and think about it.