search

johnynek / bosatsu

A python-ish pure and total functional programming language
Apache License 2.0
223 stars 11 forks source link

Check direct instantiation in inference #1080

Closed johnynek closed 7 months ago

johnynek commented 8 months ago

relates to #650

The idea is: if we can already see the sigma type in an annotation or apply, then we see if we can use simple instantiation to match the expected type. If so, we use that. The algorithm we have can only set meta variables to rho types (they can't directly hold forall or exists), so this allows some annotated inferences to be checked that would otherwise not typecheck. It doesn't change the inference in cases without annotations.

This is not exactly the quicklook algorithm, I don't think, but it is at least very related.

I should add some of the tests from the paper.

codecov-commenter commented 7 months ago

Codecov Report

Attention: 10 lines in your changes are missing coverage. Please review.

Comparison is base (92c5905) 92.51% compared to head (74c95eb) 92.32%.

Files Patch % Lines
.../src/main/scala/org/bykn/bosatsu/rankn/Infer.scala 95.68% 5 Missing :warning:
...e/src/main/scala/org/bykn/bosatsu/rankn/Type.scala 93.58% 5 Missing :warning:

:exclamation: Your organization needs to install the Codecov GitHub app to enable full functionality.

Additional details and impacted files ```diff @@ Coverage Diff @@ ## master #1080 +/- ## ========================================== - Coverage 92.51% 92.32% -0.19% ========================================== Files 93 93 Lines 10414 10564 +150 Branches 2465 2497 +32 ========================================== + Hits 9634 9753 +119 - Misses 780 811 +31 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.