CODEWITHSUNDEEP
agda
otah007
otah007

Reputation: 525

Implicit argument not always used depending on how it's written

I have a function with the following type signature:

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

where the ⟨_⟩ notation is for constructing rose trees and Rights y is a data structure that witnesses that a certain property holds for a rose tree.

I often have to write .⦃ _ : Rights y ⦄ and .⦃ _ : Lefts y ⦄, sometimes multiple of these in a single type signature, and it starts to get a bit long, so to shorten things I came up with

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

and then I can write the above type signature as

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

However, in some cases the original version with .⦃ _ : Rights y ⦄ works but the version with R y ⇒ fails to typecheck - I get errors about failing to solve constraints/resolve instance arguments. Furthermore, I am unable to pattern match on the instance argument:

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

gives the error

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)

But there are a number of other functions where it typechecks just fine with R y ⇒ (and doesn't typecheck if I remove it, so it is being used).

I suppose my question is twofold:

  1. Is it expected behaviour that when defining a function like R_⇒_ I can't pattern match on the contents, and that sometimes the contents aren't found during instance search?

  2. Is there a way to make a function/synonym/macro like R_⇒_ that works properly? For example, something like a C macro that is just a textual substitution?

Upvotes: 1

Views: 96

Answers (1)

otah007
otah007

Reputation: 525

Thanks to @Jesper for solving the problem for me: → has the lowest precedence of all operators as it is handled directly by the parser rather than parsed as a symbol and resolved into an operator later. As a result, any piece of code like a * b → c, where * is a binary operation, will be parsed as (a * b) → c, no matter what precedence you give *. In this case it parses R x ⇒ y → z as (R x ⇒ y) → z, which means that Rights x can't be used except in y. The solution is to add parentheses: R x ⇒ (y → z).

Upvotes: 2

Related Questions