search

ethereum / fe

Emerging smart contract language for the Ethereum blockchain.
https://fe-lang.org
Other
1.6k stars 178 forks source link

Ensure termination in trait solving #1014

Closed Y-Nak closed 2 months ago

Y-Nak commented 2 months ago

This PR ensures the termination in trait solving by adding a bound on type depth. As the comments in the code describe, we'd need to revisit the trait solver when v2 is deployed. This limitation doesn't break the soundness of the trait solver itself, but in some cases, users might need to add extra type annotations in their code.

Y-Nak commented 2 months ago

@sbillig I tweaked the trait resolution process so that the solver prioritize consumer nodes that are closer to the original goal. This would mitigate the overhead since it hits the maximum solution limit of the original goal before hitting the depth limit in simple cases(in the vec case, the solver takes 0.03s), and I feel many cases would belong to this simple case. This is not a general solution, but assuming that we will improve the solver so that it can handle these cases properly without a depth limit, I think it'd be probably fine for now.

sbillig commented 2 months ago

Looks great, this is a much better solution than my suggestion 😅