Default arguments in interfaces do not seem to work

[bgavran]

Summary

An error is thrown when compiling an implementation of an interface with a default parameter in one of its functions.

Tested on latest Idris version, but also a version from November 2025.

Could be related to #3291. @andrevidela suggested it might be related to some previous fixes (#3467, #3475 ), recording here for posterity

Steps to Reproduce

Attempt to compile the code below (available in the following gist)

module DefaultWithInterface 

interface I a where
  f : {default 3 x : Nat} -> a

I Bool where
  f = ?f_rhs

Expected Behavior

Compiles without error.

Observed Behavior

While processing right hand side of I implementation at DefaultWithInterface:6:1--7:13. When unifying:
    {_ : Nat} -> Bool
and:
    Bool
Mismatch between: {_ : Nat} -> Bool and Bool.