Discussion: instance argument candidates from the context

[UlfNorell]

Currently any variable in the context is available for instance search, so you can define things like

foo : {A : Set} (eqA : Eq A) → A → A → Bool
foo eqA x y = isYes (x == y)

My question is this: are there cases where you need this, or could we restrict instance search to only consider variables from the context that are themselves instance arguments?

There are two reasons why I think this would be desirable

• it mirrors the treatment of top-level instances (only things declared instance are considered)
• there can be very many things in the context, making instance search slow

[jespercockx]

AFAIK there is currently no way to declare an instance in a telescope. What would be a sensible syntax for it? Maybe something like this:

foo : instance {A : Set} → Set
foo = it

I also think that all instance arguments in the telescope should be considered instances automatically, otherwise passing around instance arguments could become very painful.

[UlfNorell]

My suggestion is that only instance arguments in the context are considered for instance search, not that nothing from the context is considered. In your example you would have to say

foo : {{A :Set}} → Set

[jespercockx]

I see, in that case I am in favor of this proposal.

[andreasabel]

I cannot judge the consequences of this, but a cautious agreement to your proposal from me.

[np]

What about module parameters?

On 11/10/2015 03:20 PM, Ulf Norell wrote:

My suggestion is that only instance arguments in the context are
considered for instance search, not that nothing from the context is
considered. In your example you would have to say

|foo : {{A :Set}} → Set |

—
Reply to this email directly or view it on GitHub
#1716 (comment).

Best regards,
-- NP

[UlfNorell]

The same rules would apply to module parameters (obviously).