Replace EvTerm with CoreExpr
I asked
I had some funky idea where a type checker plugin would have to | synthesize code for a custom-solved instances on the fly. But it seems that does not work because EvTerm is less expressive than Core (especially, no lambdas)
What would break if we had
| EvExpr CoreExpr
as an additional constructor there?
And Simon said
This has come up before. I think that'd be a solid win.
In fact, eliminate all the existing evidence constructors with "smart constructors" that produce an EvExpr. That'd mean moving stuff from the desugarer into these smart constructors, but that's ok.
I /think/ I didn't do that initially only because there were very few forms and it mean that there was no CoreExpr stuff in the type checker. But as we add more forms that decision looks and less good.
You'd need to add
zonkCoreExpr
in place ofzonkEvTerm
.
evVarsOfTerm
is called quite a bit; you might want to cache the result in theEvExpr
constructor.
This ticket tracks it. Not sure if i get to it right away, but I am happy to advise, review, and play around with the result.
Trac metadata
Trac field | Value |
---|---|
Version | 8.3 |
Type | Task |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |