[Builtin] Introduce 'AssociateType' in 'KnownTypeIn' #4172
Conversation
| @@ -93,7 +93,7 @@ nopCostParameters = toMachineParameters $ CostModel defaultCekMachineCosts nopCo | |||
| arguments. We have checked this and there there was no dependence: let's | |||
| leave open the possibility of doing it again in case anything changes. | |||
| -} | |||
| instance uni ~ DefaultUni => ToBuiltinMeaning uni NopFuns where | |||
| instance KnownBuiltinTypeIn uni Integer => ToBuiltinMeaning uni NopFuns where | |||
There was a problem hiding this comment.
This returns the original version just to show that it's possible. My latest PR made that impossible (which I only figured out after the PR was merged), so I thought it would be nice to fix that. Although it's not really important, we don't even have more than one universe, so who cares if we can or cannot define universe-polymorphic built-in functions.
| @@ -100,7 +101,7 @@ insertBuiltin | |||
| insertBuiltin fun = | |||
| case toBuiltinMeaning fun of | |||
| BuiltinMeaning sch meta _ -> | |||
| case typeSchemeResult sch of | |||
| case typeSchemeResult @(Term TyName Name DefaultUni DefaultFun ()) sch of | |||
There was a problem hiding this comment.
This is the type annotation. And it's the place that was triggering the OVERLAPPABLE instance that is now removed. So this piece of code was already quite weird (we're trying to infer term under the presence of a KnownType term a constraint and propagate that upwards where the constraint does not exist and that doesn't quite work).
| -- This constraint is just to get through 'KnownPolytype' stuck on an unknown type straight | ||
| -- to the custom type error that we have in the @Typed@ module. Though, somehow, the error | ||
| -- gets triggered even without the constraint when this function in used, but I don't | ||
| -- understand how that is possible and it does not work when the function from the @Debug@ | ||
| -- module is used. So we're just doing the right thing here and adding the constraint. | ||
| , KnownMonotype term args res a |
There was a problem hiding this comment.
I dropped that OVERLAPPING instance, so this is now obsolete.
effectfully
force-pushed
the
effectfully/builtins/introduce-AssociateType-2
branch
from
7426ced to
a279e9e
Compare
This drops the `term` argument from `KnownTypeIn` allowing us to express more and require less. See the comments. `KnownType term a` is recovered and user code is not affected apart from `KnownTypeIn DefaultUni` instances being simpler and some old testing code (that was already behaving weirdly) requiring a few explicit type applications.
effectfully
force-pushed
the
effectfully/builtins/introduce-AssociateType-2
branch
from
a279e9e to
d073e26
Compare
effectfully
deleted the
effectfully/builtins/introduce-AssociateType-2
branch
|
I compared this branch with its parent (90d7665) and there is a slowdown: The figures for the parent are comparable with the figures from master on the 1st of November (the first table in the other PR) and the ones for the PR are comparable with master on the 2nd of November (the second in the other PR). What I don't understand is that I benchmarked both master and your branch on the 1st of November and then again on the second, and both branches slowed down, but I thought I hadn't updated your branch between the two lots of benchmarks. Perhaps I was wrong about that. Anyway, what I think happened was that I compared your branch against master twice and both times your branch was faster than master, but I hadn't noticed that that second time both branches had slowed down. I don't know where this leaves us overall. |
|
I can't see how this could have slowed us down, doesn't this only affect type-level stuff? |
This reverts commit 3959845.
Not exactly. It moves constraints like |
This drops the `term` argument from `KnownTypeIn` allowing us to express more and require less. See the comments. `KnownType term a` is recovered and user code is not affected apart from `KnownTypeIn DefaultUni` instances being simpler and some old testing code (that was already behaving weirdly) requiring a few explicit type applications.
…ctMBO#4172)" (IntersectMBO#4195) This reverts commit 3959845.
This drops the
termargument fromKnownTypeInallowing us toexpress more and require less. See the comments.
KnownType term ais recovered and user code is not affectedapart from
KnownTypeIn DefaultUniinstances being simpler andsome old testing code (that was already behaving weirdly) requiring
a few explicit type applications.