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:
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?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?