Typeclass instance problem?

Stream: lean4

[Joseph O]

Why am I getting this error?
MWE:

inductive HList : List Type → Type 1 where
  | nil : HList []
  | cons {α : Type} (x : α) {αs : List Type} (xs : HList αs) : HList (α :: αs)

syntax (name := hlist) "[" term,* "]" : term
macro_rules (kind := hlist)
  | `([]) => `(HList.nil)
  | `([$x]) => `(HList.cons $x HList.nil)
  | `([$x, $xs,*]) => `(HList.cons $x [$xs,*])

infixr:67 " :: " => HList.cons

def map {α : Type} {αs : List Type} (f : α → β) : HList (α::αs) → HList (β::αs)
  | a::as => (f a)::as

instance : Functor (λ α => HList (α::αs)) where
 map := HList.map

#eval let h : HList [Nat, String, Int] := [7, "hi", -2]; Functor.map (·*2) h

Error:

typeclass instance problem is stuck, it is often due to metavariables
  Functor ?m.3922

[Mario Carneiro]

what instance are you expecting to find?

[Joseph O]

A functor instance?

[Mario Carneiro]

the use of Functor.map _ h means that there should be an instance of Functor HList

[Mario Carneiro]

or rather, it would be that but this doesn't typecheck

[Mario Carneiro]

which is why the error is not even mentioning HList

[Mario Carneiro]

it has no idea what functor you are talking about

[Sebastian Ullrich]

In short, you cannot specify the functorial structure per-instance like this

[Joseph O]

Mario Carneiro said:

the use of Functor.map _ h means that there should be an instance of Functor HList

But i have such functor instance

[Joseph O]

Sebastian Ullrich said:

In short, you cannot specify the functorial structure per-instance like this

You mean like on the first item?

[Mario Carneiro]

No, you have Functor (λ α => HList (α::αs))

[Mario Carneiro]

Lean will not do the necessary higher order unification to find such instances

[Mario Carneiro]

If you want to use Functor on a thing of type T A then you need Functor T, not Functor (id T) or Functor (fun _ => T A) or something else

[Mario Carneiro]

Alternatively, you could rewrite h to have type (λ α => HList (α::[String, Int])) Nat

[Mario Carneiro]

Actually that doesn't seem to work either. It works if you specify f explicitly:

#check
  let h : HList [Nat, String, Int] := [7, "hi", -2]
  Functor.map (f := λ α => HList [α, String, Int]) (·*2) h

[Mario Carneiro]

You can also make a definition for the type function and use that

def FirstList (αs α) := HList (α::αs)
instance : Functor (FirstList αs) where
 map := HList.map

#check
  let h : FirstList [String, Int] Nat := [7, "hi", -2]
  Functor.map (·*2) h

[Joseph O]

Got it. So it seems there isn’t really a nice alternative.