infinite loops in type inference? · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: infinite loops in type inference?

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: Jun 04 2023 at 19:30 UTC