dougalm
commented
1 year ago Looks good, but could you add some explanation of the API change of checkE? Why did it used to return the checked E-kinded object, and why is it ok for it to now return unit?
It was just a performance consideration in the first place. The idea was that since we often have to apply the substitution as we check the term, we should be able to return the substituted term to save the caller from possibly repeating that work. But it turned out that we only rarely used this feature. The main user was in checking blocks, and we have a separate path for that now anyway. The other thing that's changed is that nowadays we only run the checker in debug mode, so performance isn't as critical.
We only actually use the allowd effects in two places: inference and type checking. Tracking them everywhere else hurts performance because we have to consider extending the allowed effects every time we emit a binding, which is a lot. Since we added the IR parameters, the effects carried in the Env are also ill-typed, because they're treated as CoreIR even though we can have SimpIR effects too. We had to use unsafeCoerceIRE to work around that. After this change, the only use of unsafeCoerceIRE is in pretty-printing.