something_about_instances.v

Require Import canonical_names.

Class Foo A := foo: A → A.

Instance kaas0 X : Foo X := @id X.
(* kaas0 = λ X : Type, id
         : ∀ X : Type, Foo X
    
   Argument scope is [type_scope] *)

Instance kaas1 : ∀ X, Foo X := λ X, @id X.
(* kaas1 = λ X : Type, id
         : ∀ X : Type, Foo X
 
   Argument scope is [type_scope] *)

Instance kaas2 : Foo X := fun X => @id X.
(* kaas2 = λ X : Type, id
         : ∀ X : Type, Foo X
    
   Argument X is implicit and maximally inserted
   Argument scope is [type_scope] *)