Can't unify an interface with its instance

[berewt]

The compiler seems to struggle to unify interfaces with dependent types with their implementation.

Steps to Reproduce

try to compile this module:

module Test

data Dummy : (lbl : Type) -> (st : List lbl) -> Type -> Type where
  MkDummy : a -> Dummy b st a


public export
interface IxPure (f : (lbl : Type) -> (st : List lbl) -> Type -> Type)
          where
  ixPure : a -> f lbl st a

IxPure Dummy where
  ixPure = MkDummy

pure12 : Dummy String xs Integer
pure12 = ixPure $ 12

Fails with:

Expected Behavior

It should compile.

Observed Behavior

It fails with:

Test.idr:16:10--17:1:While processing right hand side of pure12 at Test.idr:16:1--17:1:
Can't find an implementation for IxPure ?f

Workarounds

Specifying explicitly the value of f in pure12 solve the issue:

pure12 : Dummy String xs Integer
pure12 = ixPure {f = Dummy} $ 12

And the problem disappears as well if we remove the st parameters.