Proving a type is a Functor - Inference error?

Question

I have the following (simplified) data types, and I'm trying to prove a type is a functor.

  data T (a : Set) : Set where                                                                                                                                                                                                               
    D  : a → T a                                                                                                                                                                                                                             
                                                                                                                                                                                                                                             
  record Functor {a b : Set} (f : Set → Set ) : Set where                                                                                                                                                                                   
    field                                                                                                                                                                                                                                    
      fmap : (a → b) → f a → f b                                                                                                                                                                                                             
                                                                                                                                                                                                                                             
  functor_T : Functor T                                                                                                                                                                                                                      
  functor_T = record                                                                                                                                                                                                                         
    { fmap = fmap'                                                                                                                                                                                                                           
    }                                                                                                                                                                                                                                        
    where                                                                                                                                                                                                                                    
      fmap' : ∀ {a b} → (a → b) → T a → T b                                                                                                                                                                                                  
      fmap' f (D a) = D (f a)                                                                                                                                                                                                                           

Yet the compiler highlights Functor and prompts the following lines.

_a_22 : Set  [ at ... :10,15-22 ]                                                                                                                                                                    
_b_23 : Set  [ at ... :10,15-22 ]  

What is causing this? Is there some inference issue?

Answer 1

Currently your definition of Functor specifies that you have the operator fmap for two specific types a and b. Presumably what you want is that fmap works for all types a and b, so you need to quantify over them in the type of fmap:

  record Functor (f : Set → Set) : Set1 where                                                                                                                                                                                   
    field                                                                                                                                                                                                                                    
      fmap : {a b : Set} → (a → b) → f a → f b   

To make this work, you also need to change the universe level of Functor itself from Set to Set1 (see https://agda.readthedocs.io/en/latest/language/universe-levels.html).

With this changed definition of Functor, your definition of functor_T should be accepted without changes!

P.S.: It is not recommended to use underscores in identifiers in Agda, since they are reserved for mixfix syntax, see https://agda.readthedocs.io/en/latest/language/mixfix-operators.html