An unused implicit argument of an interface method produces an unresolved hole

[spcfox]

Steps to Reproduce

interface Iface where
  method : {x : Type} -> Type

Expected Behavior

Successful compilation

Observed Behavior

Error: Unsolved holes:
Main.{x:836} introduced at:

[spcfox]

The problem is in the method code after elaboration. This is similar to #3467

data Iface : Type where
  MkIface : ({x : Type} -> Type) -> Iface

failing "Unsolved holes"
  method : Iface => {x : Type} -> Type
  method @{MkIface f} = f

[spcfox]

It is strange that the compiler returns code 0:

$ idris2 --check Main.idr; echo $?
1/1: Building Main (Main.idr)
Error: Unsolved holes:
Main.{x:831} introduced at: 
0

But with the manually desugared version (from the previous post) code 1

[spcfox]

This code also produces an unsolved hole:

interface Fail where
  f : Type -> {_ : Type} -> Type

[spcfox]

Another bug that isn't fixed in #3475:

interface Iface where
  method : (x : Double) -> Type

failing "Mismatch between: Double and Int"
  implementation {x : Int} -> Iface where
    method _ = Type