Can't unify an interface with its instance

[edwinb]

Issue by berewt
Monday Apr 27, 2020 at 12:46 GMT
Originally opened as edwinb/Idris2-boot#330

---

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.

[edwinb]

Poking around inside here, the problem is that it can't solve the unification problem ?f ?lbl ?st = Dummy String xs, and telling it any one of f, lbl or st resolves it. It's supposed to notice that f is an argument to an implementation so should be treated as invertible, but somehow it seems that isn't happening...

EDIT: In fact it is happening, but isn't helping. I'll dig further.

[edwinb]

Ah, it's using the conversion check (which doesn't solve holes) for arguments to invertible holes, not unification, which would resolve the holes lbl and st. I believe I have a fix.