allowing coe with metavars?

Stream: lean4

[James Gallicchio]

is it possible to configure a Coe instance such that it continues instance search even with metavariables?

To de-XY, here's a little example

inductive ParseRes (α : Type)

def Parser (α) := String → String.Pos → ParseRes α

def seq (p1 : Parser α) (p2 : Parser β) : Parser γ := sorry

def ofString (tgt : String) : Parser Unit := sorry
instance : Coe String (Parser Unit) := ⟨ofString⟩

set_option trace.Elab.coe true in
def parser : Parser Nat :=
  seq "hi" "bye"

I could make a class specifically for "coercions to Parser" where the type arg is marked outParam and all my combinators take a parameter of that type, but it seems a bit unwieldy

[Reid Barton]

In Haskell (GHC) you could write something like instance (a ~ Unit) => FromString (Parser a) to get the behavior you want

[James Gallicchio]

:/ hoping there's a lean replacement for that; otherwise I'll have to go with the custom CoeToParser class