Leans situation with Additive/Multiplicative Groups is another example here. By tying overloaded syntax to dynamic dispatch, we end up in all sorts of weird places
Conversation
If we zoom out, instance resolution is kinda just a limited form of program synthesis, where all we can do is synthesize records of functions with really specific rules. What if we broadened our horizons here, and opened up the door to broader, user programmable synthesis?
2
3
yes, this would be so great
1
2
very onboard with this idea
1
2
Agda has _some_ support for this with tactic arguments, and it’s super useful. I’m definitely interested in seeing how far one can push this though :)
1
2
implementing instance search via embedded lambda prolog and elaborator reflection lol
1
2
Glad we’re on the same page lmao
1
2
1
1
But yeah adding elaborator reflection to Rust is probably a lost cause at this point… need a new systems PL
2
1
rust++
1