Type Inference Problem

Stream: lean4

[Marcus Rossel]

I have a scenario where I feel like it should be possible for Lean to infer a type, but it fails.
The setup is as follows:

structure Scheme where
  labels : Type
  type : labels → Type

structure Schemes where
  a : Scheme
  b : Scheme

structure Values (schemes : Schemes) where
  a : (l : schemes.a.labels) → schemes.a.type l
  b : (l : schemes.b.labels) → schemes.b.type l

def SchemeM (schemes : Schemes) (α : Type) :=
  Values schemes → (Values schemes) × α

def getA {schemes : Schemes} (l : schemes.a.labels) : SchemeM schemes (schemes.a.type l) :=
  fun values => (values, values.a l)

That is, getA is an operation in the SchemeM monad which takes a given label l and returns the value for that label.
The following demonstrates using this operation:

inductive A | a₁ | a₂

abbrev A.scheme : Scheme where
  labels := A
  type
    | a₁ => Nat
    | a₂ => String

def Empty.scheme : Scheme where
  labels := Empty
  type := (nomatch ·)

def exampleSchemes : Schemes where
  a := A.scheme
  b := Empty.scheme

example : SchemeM exampleSchemes Nat :=
  getA A.a₁ -- error

The problem is that this fails on the last line with:

application type mismatch
  getA A.a₁
argument
  A.a₁
has type
  A : Type
but is expected to have type
  ?m.29155.a.labels : Type

I can fix the issue by explicitly providing the implicit schemes parameter:

example : SchemeM exampleSchemes Nat :=
  getA (schemes := exampleSchemes) A.a₁

But don't understand why type inference is failing, as the return type of the example already explicitly states this (at least according to my vague understanding of how Lean might infer such a parameter).

Also, if I split up the Schemes and instead write all of the schemes individually, it works:

structure Scheme where
  labels : Type
  type : labels → Type

structure Values (schemeA schemeB : Scheme) where
  a : (l : schemeA.labels) → schemeA.type l
  b : (l : schemeB.labels) → schemeB.type l

def SchemeM (schemeA schemeB : Scheme) (α : Type) :=
  (Values schemeA schemeB) → (Values schemeA schemeB) × α

def getA {schemeA schemeB : Scheme} (l : schemeA.labels) : SchemeM schemeA schemeB (schemeA.type l) :=
  fun values => (values, values.a l)

inductive A | a₁ | a₂

abbrev A.scheme : Scheme where
  labels := A
  type
    | a₁ => Nat
    | a₂ => String

abbrev Empty.scheme : Scheme where
  labels := Empty
  type := (nomatch ·)

example : SchemeM A.scheme Empty.scheme Nat :=
  getA A.a₁

Is there any way to make the first version work, though?

[Sebastian Ullrich]

Right, this is a restriction in how Lean uses the expected type to infer implicit parameters: it only does that when the return type does not mention any explicit parameters. So the presence of l in the return type of getA prevents schemes to be inferred as well. There are a lot of such restrictions documented at https://github.com/leanprover/lean4/blob/9fd433785b35a4a309022db05ec6074da64da209/src/Lean/Elab/App.lean#L273-L310.

[Marcus Rossel]

@Sebastian Ullrich How does the inference of schemeA in the second version of getA work then? The return type also references schemeA.type l.