Spectacular success! But a problem with typeclass inference

Stream: lean4

[Philip Wadler]

Type coercions and type classes in Lean make possible very concise forms of expression, often far more concise and readable than what is available in Agda.

For example, here is a definition of de Bruijn indices for a tiny lambda calculus.

inductive lookup : TpEnv → Tp → Type where
  | stop :
       ----------------
       lookup (Γ ▷ A) A
  | pop :
       lookup Γ B
       ----------------
     → lookup (Γ ▷ A) B
  deriving Repr

prefix:90 "S" => lookup.pop
notation:max "Z" => lookup.stop

Something similar to the above is easy to do in Agda. But what Lean makes easy, and Agda makes hard, is to convert a natural number into the corresponding de Bruijn index.

instance : OfNat (Γ ▷ A ∋ A) Nat.zero where
  ofNat := lookup.stop

instance [OfNat (Γ ∋ B) n] : OfNat (Γ ▷ A ∋ B) (Nat.succ n) where
  ofNat := lookup.pop (OfNat.ofNat n)

example : 2 = (S S Z : ∅ ▷ ℕ ⇒ ℕ ▷ ℕ ▷ ℕ ∋ ℕ ⇒ ℕ) := rfl

This is great! However, when I use it inside a larger term, Lean gets into trouble with inference.

def one_c : ∅ ⊢ (A ⇒ A) ⇒ A ⇒ A := ƛ ƛ # S Z ⬝ # Z
def one_c' : ∅ ⊢ (A ⇒ A) ⇒ A ⇒ A := ƛ ƛ # 1 ⬝ # 0

The first of these is fine, but the second (which should be equivalent) reports an error for # 0.

typeclass instance problem is stuck, it is often due to metavariables
  OfNat ?m.30623 0

Is there any workaround? Any suggestions gratefully received.

The complete code from which the above snippets are taken is available at https://github.com/plfa/plfl/blob/main/src/Typesig.lean.

[Sebastian Ullrich]

Hi Phil! With a recent Lean, I get a slightly different error message:

typeclass instance problem is stuck, it is often due to metavariables
  OfNat (∅▷A⇒A▷A∋?m.116054) 0

This is indeed a problem: we don't know what type to look up before converting the numeral, but without knowing the type none of the OfNat instances are a perfect match. Lean never uses the knowledge that there is only one applicable instance in order to fill in holes in the typeclass problem, so we are stuck. I believe it would be similar in Haskell?

One workaround would be to use a more syntactic approach, by strengthening the # notation when followed by a numeral:

macro_rules
  | `(# $n:num) => do
    let n ← n.getNat.foldM (fun _ acc => `(S $acc)) (← `(Z))
    `(# $n)

It would even be possible to override the meaning of any numeral but that probably isn't a good idea. Or you could expand that approach into a full EDSL for term depending on what your goals are.

[Philip Wadler]

@Sebastian Ullrich Thanks very much. Your explanation makes sense if it never works, but in fact it works sometimes and fails others. I'd be happy to provide additional type information to help the inferencer, but I have no idea what extra information to provide or how to provide it. Any clues?

[Sebastian Ullrich]

The specific problem is the type variable introduced by the application, we can either specify it in a subterm:

ƛ ƛ # 1 ⬝ (# 0 : _ ⊢ A)

or in the application application itself if we unfold the notation:

ƛ ƛ term.application (A := A) (# 1) (# 0)

[Philip Wadler]

@Sebastian Ullrich Thanks, that gives a workaround.