Successful instance search is followed by failure?

Stream: general

[nrs]

The following instance search first succeeds and then fails. Anyone has tips to figure out how to debug this? It works when I replace class SubSig (siga sigb : Signature) where with class SubSig (siga sigb : outParam Signature) where, but I'm not actually sure it is always the case siga and sigb are only inferred after the fact. Is this the right way to solve this?

import Mathlib

namespace myNamespace

structure Signature where
  symbols : Type
  arity : symbols -> Nat

inductive Ext (sig : Signature) (α : Type _)
| mk : (s : sig.symbols) -> (Fin2 (sig.arity s) -> α) -> Ext sig α

def Ext.map (f : α -> β) : Ext sig α -> Ext sig β
| ⟨s, g⟩ => ⟨s, f ∘ g⟩

def Alg (sig : Signature) (α : Type _) : Type _ := Ext sig α -> α

inductive W (sig : Signature)
| sup : Ext sig (W sig) -> W sig

class SubSig (siga sigb : Signature) where
  inj : Ext siga α -> Ext sigb α

def inject {siga sigb : Signature}  (ext : Ext siga (W sigb)) [SubSig siga sigb] : W sigb :=
  ⟨SubSig.inj ext⟩

inductive NatTySh | nat
def NatTyE : Signature := ⟨NatTySh, fun _ => 0⟩
def NatVal : Alg NatTyE Type := fun
  | ⟨.nat, _⟩ => Nat

inductive IArithExprSymbols {sig : Signature} [inst : SubSig NatTyE sig] : W sig -> Type _
| val : Nat -> IArithExprSymbols (inject (siga := NatTyE) ⟨.nat, (nomatch .)⟩) --succeeds
| add : IArithExprSymbols (inject (⟨.nat, (nomatch .)⟩ : Ext NatTyE (W sig))) --succeeds
| add' : IArithExprSymbols (inject _) -- tracing this line
| add'' : IArithExprSymbols (inject ⟨NatTySh.nat, (nomatch .)⟩)  -- doesn't work either, succeeds with `outParam` change

/-
▶ expected type (71:36-71:37)
sig : Signature
inst : SubSig NatTyE sig
⊢ Ext ?m.6063 (W sig)

▶ 71:29-71:37: error:
typeclass instance problem is stuck, it is often due to metavariables
  SubSig ?m.6063 sig

▶ 71:10-71:38: information:
[Meta.synthInstance] 💥️ SubSig NatTyE ?m.6058 ▼
  [] new goal SubSig NatTyE ?m.6058 ▼
  [instances] #[@SubAlg.toSubSig, inst]
  [] 💥️ apply inst to SubSig NatTyE ?m.6058 ▼
  [tryResolve] 💥️ SubSig NatTyE ?m.6058 ≟ SubSig NatTyE sig

[Meta.synthInstance] 💥️ SubSig NatTyE ?m.6064 ▼
  [] new goal SubSig NatTyE ?m.6064 ▼
  [instances] #[@SubAlg.toSubSig, inst]
  [] 💥️ apply inst to SubSig NatTyE ?m.6064 ▼
  [tryResolve] 💥️ SubSig NatTyE ?m.6064 ≟ SubSig NatTyE sig

[Meta.synthInstance] ✅️ SubSig NatTyE sig ▼
  [] result inst (cached)


▶ 71:29-71:37: information:

[Meta.synthInstance] 💥️ SubSig ?m.6063 ?m.6064 ▼
  [] new goal SubSig ?m.6063 ?m.6064 ▶
  [] 💥️ apply inst to SubSig ?m.6063 ?m.6064 ▶

...

[Meta.synthInstance] 💥️ SubSig ?m.6063 sig ▼
  [] new goal SubSig ?m.6063 sig ▼
  [instances] #[@SubAlg.toSubSig, inst]
  [] 💥️ apply inst to SubSig ?m.6063 sig ▼
  [tryResolve] 💥️ SubSig ?m.6063 sig ≟ SubSig NatTyE sig
-/

[Eric Wieser]

Can you add the imports to make your example work?

[nrs]

Sorry I should be used to doing this by now

[nrs]

done

[Eric Wieser]

I get a syntax error after your last line, your (s aren't closed

[nrs]

argh fixed my bad

[Eric Wieser]

I guess (set_option trace.Meta.synthInstance true in inject _) is needed to see the trace messages

[nrs]

I used set_option trace.Meta.synthInstance true at the top of the inductive declaration (didn't know you could literally set_option right inside a term, thanks!)

[Eric Wieser]

I think in the term it maybe doesn't show the thing you wanted to show (success followed by failure)

[Eric Wieser]

But your issue here is that typeclass synthesis is not allowed to populate metavariables, unless you mark them as outParam or semiOutParam

[Eric Wieser]

And you should think carefully about whether those are actually what you want, or if instead the caller should just have provided a type annotation

[nrs]

Hm right when I use trace.Meta.synthInstance directly inside the term there's only the failure, but at the top of the inductive it reports that on the same line there's a success before the failure

[nrs]

I'll be investigating outParam and semiOutParam more closely, thanks a lot for taking the time!!

[Eric Wieser]

Note that the indentation is currently broken for the trace output (lean4#6389), which can make it hard to read

[Eric Wieser]

You can work around it by using #guard_msgs in, and then the version that gets copied into a comment has the correct indentation

[nrs]

Noted! very useful stuff, thanks a lot!