I'm wondering if type inhabitance for the calculus of constructions is semi-decideable. I know the following:
- System F inhabitance and, correspondingly, second-order unification are semi-decideable
- Higher-order unification is at least as hard as second order unification
- Folk knowledge holds that higher-order untyped unification is semi-decideable (I haven't found any concrete sources for this)
- CoC is a higher-order full dependently-typed logic
- Some simpler restrictive dependently typed higher-order logics have decidable type inhabitance
I don't know what is true about inhabitance in CoC. I don't know how dependent types with no restrictions impact semidecidability. This feels to me like it should be an obvious question, but hours of searching and talking to other PL researchers today gave me nothing but different accounts of people's intuition, with nothing concrete.