Stream: Coq devs & plugin devs

Topic: infinite loops in type inference?

view this post on Zulip Jason Gross (Jan 15 2021 at 18:41):

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

Infinite loop in Coq's type inference? · Issue #13748 · coq/coq
Description of the problem Coq seems to infinite loop trying to typecheck the final Fixpoint here. I expect a relatively quick success or error: Inductive uncurry_types := | ccons (A : Type) (rest ...

Last updated: Oct 16 2021 at 02:03 UTC