隐式参数并不总是根据它的编写方式使用的

Question

我有一个具有以下类型签名的函数：

loop : ∀ {x y z} → .⦃ _ : Rights y ⦄ → DRuby (⟨ x , y ⟩ , ⟨ y , z ⟩) → DRuby (x , z)

其中，⟨_⟩表示法用于构造玫瑰树，而Rights y是一个数据结构，它见证了玫瑰树的特定属性。

我经常要写.⦃ _ : Rights y ⦄和.⦃ _ : Lefts y ⦄，有时在一个类型的签名中有多个，而且它开始变得有点长，所以要缩短我想出来的东西。

infixr 5 R_⇒_
R_⇒_ : DShp → Set → Set
R x ⇒ y = .⦃ _ : Rights x ⦄ → y

然后，我可以将上述类型的签名写成

loop : ∀ {x y z} → R y ⇒ DRuby (⟨ x , y ⟩ , ⟨ y , z ⟩) → DRuby (x , z)

但是，在某些情况下，使用.⦃ _ : Rights y ⦄的原始版本可以工作，但是带有R y ⇒的版本不能进行类型检查--我遇到了无法解决约束/解析实例参数的错误。此外，我无法对实例参数进行模式匹配：

loop {x} {y} {z} ⦃ p ⦄ q = ?

给出误差

Unexpected implicit argument
when checking that the clause
loop {x} {y} {z} ⦃ p ⦄ q = ?
has type
{x : Rose (Type × Dir)} {y : _B_1266 x} {z : Rose (Type × Dir)} →
R x ⇒ DRuby (RS.⟨ _r_1261 ⟩ (x , y) , RS.⟨ _r_1269 ⟩ (y , z)) →
DRuby (x , z)

但是还有许多其他函数，在R y ⇒中，它的类型很好(如果我删除它，它也不会进行类型检查，所以它被使用了)。

我想我的问题有两个：

1. 是否期望在定义像R_⇒_这样的函数时，不能在内容上进行模式匹配，有时在实例搜索过程中找不到内容？

1. 是否有一种方法可以使函数/同义词/宏类似于R_⇒_正常工作？例如，类似于C宏的东西，它只是一个文本substitution?

Answer 1

感谢@Jesper为我解决了这个问题：→是所有操作符中优先级最低的，因为它由解析器直接处理，而不是作为符号解析，稍后被解析为操作符。因此，任何像a * b → c这样的代码(其中*是二进制操作)都将被解析为(a * b) → c，不管您给予*什么优先级。在本例中，它将R x ⇒ y → z解析为(R x ⇒ y) → z，这意味着Rights x只能在y中使用。解决方案是添加括号：R x ⇒ (y → z)。