I remember learning in a class that type inference is decidable but usually takes a long time (e.g. type inference in OCaml is EXPTIME).
I was wondering, since Coq allows programs/values themselves to be in the Type somehow my guess would be that type inference is either:
- Doubly EXPTIME
Does someone know the answer to this? A reference and an intuition would be highly appreciated too.