在接口实现中使用类型同义词

Question

给定两个接口：

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

我希望使用以下类型同义词在给定第二个接口的情况下实现第一个接口：

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

执行以下操作：

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

然而，idris编译器给出了以下错误：

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

在我看来，编译器没有能力看到类型同义词实际上是一个类型构造函数。有什么办法可以解决这个问题吗？

Answer 1

是的，根据Idris issue #3727，这似乎是对接口实现的故意限制。至于解决方法，以下方法不是很直接，但它是有效的：

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)