How to use dependent coercion to coerce within a context?

Stream: general

[nrs]

structure bspkStr where
  str : String
  prop : ∀ s, s ∈ str.toList -> s.isAlphanum := by first | trivial | trace "bspkStr trivial proof failed"

instance {str : String} {prop : ∀ c, c ∈ str.toList -> c.isAlphanum}: CoeDep String str bspkStr where
  coe := .mk str prop

def myContext [CoeDep String str bspkStr] : bspkStr := "hello" -- type mismatch

I'm trying dependent coercions here because normal coercions fail on account of invoking the proof for prop too soon so the instance for Coe String bspkStr doesn't typecheck. What's the proper way to invoke CoeDep with the defined instance within myContext so that "hello" is coerced to bspkStr?

[nrs]

Note that

example [CoeDep String "hello" bspkStr]: bspkStr := "hello"

works but...

[nrs]

The above "hello" CoeDep fails to synthesize. Here is a mwe, but still not very useful

instance bspkInst : CoeDep String "hello" bspkStr where
  coe := .mk "hello" (by simp)

def mycoed : bspkStr := "hello"

[nrs]

solved: turns out that unsolved proof state in typeclass instance declaration doesn't block instance resolution (that was the whole reason I started trying using implicit arguments to the instance declaration, i thought the unsolved proof state was blocking resolution)

[Notification Bot]

nrs has marked this topic as resolved.

[nrs]

solved: turns out that unsolved proof state in typeclass instance declaration doesn't block instance resolution (that was the whole reason I started trying using implicit arguments to the instance declaration, i thought the unsolved proof state was blocking resolution)

[Notification Bot]

nrs has marked this topic as unresolved.

[nrs]

I was wrong, leaving the proof state unresolved is the same as using sorry