Just FYI, most dependent type systems don’t typecheck when a parameter to a type constructor is a function, since they can’t “deduce” very much about a function

Just FYI, most dependent type systems don’t typecheck when a parameter to a type constructor is a function, since they can’t “deduce” very much about a function except its signature. They can take proof objects (including objects involving evaluated functions, like ‘n % 2 = 0’) but not functions by themselves (like ‘loop {}’). This isn’t a technical problem with unification, the issue is a fundamental conflict between “intensional” versus “extensional” equality. Wikipedia has a good example that communicates the underlying confusion: https://en.wikipedia.org/wiki/Extensionality https://en.wikipedia.org/wiki/Extensionality AFAIK all depedently-typed general-purpose languages use intensional equality since it’s consistent, but there are proof-checkers that use extensional dependent type theories (inconsistency is less of a problem than you might think, and actually makes some higher-order topology and set theory much easier to program).