Odd type-inference

[ghost]

The following proof fails.

theory Foo
extends root

theorem lemma:'∀P y z. y = z → (x ↦ P x y) = (x ↦ P x z)'
  let 'P:𝒰 → 𝒰 → 𝒰'
  let 'y'
  let 'z'
  assume asm:'y = z'
  theorem lemma:'∀x. P x y = P x z'
    let 'x'
    combine (reflexive 'P x', asm)
  abstract lemma

It can be fixed by leading with theorem lemma:'∀P:𝒰 → 𝒰 → 𝒰. ∀ y z. y = z → (x ↦ P x y) = (x ↦ P x z)'

Surely the type annotation is unnecessary?

[phlegmaticprogrammer]

Nope, that's ok. Without the type annotation, P is assumed to have type '𝒰'.

[ghost]

But given that x has some type α, surely the fact that P is used in P x y constrains it to have type of the form α → β?

[phlegmaticprogrammer]

x has also type '𝒰', there is no type α. So 'P' has type '𝒰', so does 'P x', so does 'P x y'.

[ghost]

I meant α as a metavariable. So if x has type 𝒰, why isn't P constrained to have type of shape 𝒰 → β (where β is some concrete proofpeer type.)

[phlegmaticprogrammer]

Because in the above 'P x' does not mean higher-order function application, it means set theoretic function application.

[ghost]

Ah yes, of course. Thanks!