improve 1164 #1166
improve 1164 #1166
Conversation
Codecov ReportAll modified and coverable lines are covered by tests ✅
❗ Your organization needs to install the Codecov GitHub app to enable full functionality. Additional details and impacted files@@ Coverage Diff @@
## main #1166 +/- ##
==========================================
+ Coverage 91.32% 91.50% +0.18%
==========================================
Files 96 96
Lines 11846 11970 +124
Branches 2675 2750 +75
==========================================
+ Hits 10818 10953 +135
+ Misses 1028 1017 -11 ☔ View full report in Codecov by Sentry. |
| refl_sub: forall a. Sub[a, a] = Sub(x -> x) | ||
| refl_any: Sub[forall a. a, exists a. a] = refl_sub | ||
| #ignore: Tup[forall a. Sub[a, a], Sub[forall a. a, exists a. a]] = Tup(refl_sub, refl_any) | ||
| ignore = Tup(refl_sub, refl_any) |
There was a problem hiding this comment.
add more tests here, looks like we haven't solved it yet.
| } | ||
| case _ => | ||
| None | ||
| }) |
There was a problem hiding this comment.
We should be able to match on any Quantification and instantiate it correctly. The existential and universal require instantiating two different directions to only one or the other is easy.
| @@ -1462,6 +1479,130 @@ object Infer { | |||
| } | |||
| } | |||
|
|
|||
| // noshadow must include any free vars of args | |||
| def liftQuantification[A]( | |||
There was a problem hiding this comment.
Should add direct tests of this in simple cases and possibly property checks. For instance, if there is a quantification on any arg, it should be lifted up. Or rather the result should not have quantification on any argument.
This improves type inference on function application in the common case that the fn and argument types are simple.
This seems to fix the issue with #1164 for now, but does not address the unshadowing approach I thought would be useful (that turns out to never actually be a codepath hit for reasons I don't understand).