typeclass resolution?

Stream: lean4

[Siddharth Bhat]

Consider:

inductive OpT (OpKind: Type) (Ops: OpKind -> Type -> Type): Type
| mk: (k: OpKind) -> (args: Ops k String)  -> OpT OpKind Ops

class  ToList (f: Type -> Type) where
   toList : f α → List α

instance  [ToList f] : Coe (f α) (List α) where
  coe := ToList.toList


inductive Op: Type
| mk: List String -> Op


-- Messages (1)
-- 21:29:
-- failed to synthesize instance
--  ToList (Ops k)
instance {OpKind: Type} {Ops: OpKind -> Type -> Type} {BBs: OpKind -> Type -> Type}
    {k: OpKind}
    [ToList (Ops k)] : Coe (OpT OpKind Ops) Op where
  coe op :=
    match op with
    | OpT.mk k args=> Op.mk (ToList.toList args)

I'm unsure what I'm doing wrong. As far as I can see, I declare that I want a [ToList (Ops k)] as a pre-requisite for this coercion.

╰─$ lean --version
Lean (version 4.0.0-nightly-2022-01-16, commit 189f4bd372d8, Release)

[Henrik Böving]

It does get a little more apparent if you dont name the first and the second k equivalently:

inductive OpT (OpKind: Type) (Ops: OpKind -> Type -> Type): Type
| mk: (k: OpKind) -> (args: Ops k String)  -> OpT OpKind Ops

class  ToList (f: Type -> Type) where
   toList : f α → List α

instance  [ToList f] : Coe (f α) (List α) where
  coe := ToList.toList


inductive Op: Type
| mk: List String -> Op

-- Messages (1)
-- 21:29:
-- failed to synthesize instance
--  ToList (Ops k)
instance {OpKind: Type} {Ops: OpKind -> Type -> Type} {BBs: OpKind -> Type -> Type}
    {k: OpKind}
    [inst : ToList (Ops k)] : Coe (OpT OpKind Ops) Op where
  coe op :=
    match op with
    | OpT.mk k2 args=> Op.mk (ToList.toList args)

leads to:

failed to synthesize instance
  ToList (Ops k2)

which is the actual issue here

[Henrik Böving]

you are referring to two different k's in the first and second part of your code and thus the instance is in fact not available here

[Henrik Böving]

If you were to change the instance to this:

instance {OpKind: Type} {Ops: OpKind -> Type -> Type} {BBs: OpKind -> Type -> Type}
    [inst : ∀ k : OpKind, ToList (Ops k)] : Coe (OpT OpKind Ops) Op where
  coe op :=
    match op with
    | OpT.mk k2 args=> Op.mk (ToList.toList args)

it can resolve the type class constraint, although I don't know whether this is what you are actually intending.