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:

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: Mar 02 2024 at 17:02 UTC