Allow instance field declarations

[janmasrovira]

There should be a way to define a field to be an instance argument. E.g. we would like the applicative field in the Monad record to be an instance argument rather than an explicit argument.

trait
type Monad (M : Type -> Type) :=
  mkMonad  {
    applicative : Applicative M;
    bind : {A B : Type} -> M A -> (A -> M B) -> M B;
  };

Moreover, if we have the {{Monad M}} instance in scope, it should be possible to automatically infer the {{Applicative M}} and {{Functor M}} instances automatically.

Syntax

• In Add builtin Functor / Applicative / Monad #2354 some possible syntaxes were proposed. I'll make a followup proposal here.

Options:

1. Wrap only the name of the field with braces.

   trait
   type Monad (M : Type -> Type) :=
     mkMonad  {
       {{applicative}} : Applicative M;
       bind : {A B : Type} -> M A -> (A -> M B) -> M B;
     };
   

2. Wrap only the field type with braces.

   trait
   type Monad (M : Type -> Type) :=
     mkMonad  {
       applicative : {{Applicative M}};
       bind : {A B : Type} -> M A -> (A -> M B) -> M B;
     };
   

3. Wrap the whole field with braces.

   trait
   type Monad (M : Type -> Type) :=
     mkMonad  {
       {{applicative : Applicative M}};
       bind : {A B : Type} -> M A -> (A -> M B) -> M B;
     };
   

I'd personally argue that Option 1 is the best. It is easy to identify that the field is an instance argument and we do not add any potentially confusing braces to the type.