Using type synonyms in interface implementations

Question

Given two interfaces:

interface Poset a (po : a -> a -> Type) where
  reflexive :  (x : a) -> x `po` x

interface JoinSemilattice a where
  join : a -> a -> a
  joinAssociative : (x, y, z : a) -> x `join` (y `join` z) = (x `join` y) `join` z

I wish to make an implementation of the first interface given the second interface using the following type synonym:

LTE : JoinSemilattice a => a -> a -> Type 
LTE x y = (x `join` y = y)

Doing the following:

implementation JoinSemilattice a => Poset a LTE where
...

However the idris compiler gives the following error:

 LTE  cannot be a parameter of Algebra.Lattice.Poset
 (Implementation arguments must be type or data constructors)

It seems to me that the compiler is not capable of seeing that the type synonym in fact is a type constructor. Is there any way to work around this?

Jeroen Noels Jeroen Noels · Accepted Answer · 2018-04-06T05:27:29

Yes, according to Idris issue #3727, this appears to be a deliberate restriction on interface implementations. As for a workaround, the following approach is less direct but it works:

interface Poset a (po : a -> a -> Type) where
  reflexive : (x : a) -> x `po` x 

interface JoinSemilattice a where 
  join : a -> a -> a
  selfJoin : (x : a) -> x `join` x = x 

data LTE : a -> a -> Type where
  CheckLTE : JoinSemilattice a => {x,y : a} -> x `join` y = y -> LTE x y

implementation JoinSemilattice a => Poset a LTE where
  reflexive x = CheckLTE (selfJoin x)

Using type synonyms in interface implementations

1 Answers