ssm-lang / sslang

A language built atop the Sparse Synchronous Model
BSD 3-Clause "New" or "Revised" License
18 stars 0 forks source link

Version 2: constraint-based type infernce #122

Closed leoqiao18 closed 1 year ago

leoqiao18 commented 1 year ago

This PR is version 2 of the constraint-based type inference. This version is going to look different from the first one, so I am making a new PR.

With the learnings from version 1, version 2 aims to implement constraint-based type inference in a cleaner and more fitting approach for sslang codebase.

leoqiao18 commented 1 year ago

The implementation is now complete. There are a couple of problems left that need to be addressed.

  1. Error regression tests: the current error regression tests are hard-coded with explicit error messages, which is not ideal. It is also the reason why this PR is not passing the regression tests. (https://github.com/ssm-lang/sslang/actions/runs/3414097454/jobs/5681601441#step:5:465)
  2. polyref1-fail.ssl: this PR is now incorrectly type-checking this failure case. A bit of work needs to be done to perform the value restriction technique. (https://github.com/ssm-lang/sslang/actions/runs/3414097454/jobs/5681601441#step:5:513)
  3. TypeInferSpec.hs: there is something weird going on with mangling inside the type inference unit test, causing correct inferences to fail the comparison tests. (https://github.com/ssm-lang/sslang/actions/runs/3414097454/jobs/5681601441#step:5:1990)
  4. TypeInferSpec.hs: I believe typechecks a program with complicated patterns unit test case is incorrect. (https://github.com/ssm-lang/sslang/actions/runs/3414097454/jobs/5681601441#step:5:2023)
leoqiao18 commented 1 year ago

Regarding the 4 things above:

  1. error regression tests: @j-hui says that I can just leave it as is for now. Since it is correctly throwing errors, it is ok despite having different error messages.
  2. polyref1-fail.ssl: I have added value restriction, so this is throwing error as expected. I am doing a little bit more than our previous type-inference, in that if there is a non-value binding, I will not generalize anything in the recursive binding group, which I think is the correct thing to do.
  3. TypeInferSpec.hs: @j-hui and I will investigate more about the type variable name mangling issue. There should probably be a more sophisticated type variable name mangling function
  4. TypeInferSpec.hs: the incorrect unit test case is fixed in PR #127 . The previous type inference implementation was not able to detect this incorrectness due to how it was inferring types from patterns (it was using the AnnDCon annotations generated from lowerAst, instead of inferring from the patterns themselves).
leoqiao18 commented 1 year ago

The PR is now ready for review and merge.