I thought type inference was supposed to be terminating in the absence of typeclasses? I have a very small example where it seems to loop forever where the fanciest thing I'm using is fixpoints: https://github.com/coq/coq/issues/13748
Last updated: Feb 05 2023 at 20:03 UTC