[Agda] Problem with generalised variables

[G. Allais]

Hi Thorsten,

Note that we have an issue open to make this the default behaviour:
https://github.com/agda/agda/issues/3447

This is what Idris 2 does (unless the variable is explicitly re-bound
on the LHS by the user).

Cheers,

On 23/07/2020 18:00, Thorsten Altenkirch wrote:
> Thank you, Guillaume.
> 
> I see the declaration 
> I : A → A
> Is just a shorthand for
> I : {A : Set} → A → A
> 
> Hence if in the term I want to refer to A I have to introduce it as an explicit parameter.
> 
> Cheers,
> Thorsten
> 
> On 23/07/2020, 17:31, "Guillaume Brunerie" <guillaume.brunerie at gmail.com> wrote:
> 
>     Hi Thorsten,
> 
>     I : A → A
>     I {A} = S K (K {B = A})
> 
>     seems to work.
> 
>     Best,
>     Guillaume
> 
>     Den tors 23 juli 2020 kl 18:04 skrev Thorsten Altenkirch
>     <Thorsten.Altenkirch at nottingham.ac.uk>:
>     >
>     > Hi,
>     >
>     >
>     >
>     > I am writing some material about combinators and thought it is quite nice to use generalized variables for types:
>     >
>     >
>     >
>     > variable
>     >
>     >   A B C : Set
>     >
>     >
>     >
>     > K : A → B → A
>     >
>     > K x y = x
>     >
>     >
>     >
>     > S : (A → B → C) → (A → B) → (A → C)
>     >
>     > S f g x = f x (g x)
>     >
>     >
>     >
>     > However, when I try to define
>     >
>     >
>     >
>     > I : A → A
>     >
>     > I = S K K
>     >
>     >
>     >
>     > I run into the usual problem of an uninstantiated metavariable. Using explicit abstraction I was able to fix this by saying
>     >
>     >
>     >
>     > I : A → A
>     >
>     > I = S K (K {B = A})
>     >
>     >
>     >
>     > But when I try this in this setting I get quite a mouthy error message.
>     >
>     >
>     >
>     > Any advice? I don’t really want to introduce fake modules of possible because then I would to indent everything.
>     >
>     >
>     >
>     > Thorsten
>     >
>     >
>     >
>     >
>     >
>     > This message and any attachment are intended solely for the addressee
>     > and may contain confidential information. If you have received this
>     > message in error, please contact the sender and delete the email and
>     > attachment.
>     >
>     > Any views or opinions expressed by the author of this email do not
>     > necessarily reflect the views of the University of Nottingham. Email
>     > communications with the University of Nottingham may be monitored
>     > where permitted by law.
>     >
>     >
>     >
>     > _______________________________________________
>     > Agda mailing list
>     > Agda at lists.chalmers.se
>     > https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7C2768b321b70d447e178608d82f29f5d7%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637311204557261402&sdata=anyyMqR84gQq2sYHravBjZY0r2fjIeDI1s0%2BVy6o6aw%3D&reserved=0
> 
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7C2768b321b70d447e178608d82f29f5d7%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637311204557261402&sdata=anyyMqR84gQq2sYHravBjZY0r2fjIeDI1s0%2BVy6o6aw%3D&reserved=0
>