Type constructor parameter inference

I'm going through "Scala with cats". In 3.5.2 (p. 58, bottom) there is an example:

def doMath[F[_]](start: F[Int])(implicit functor: Functor[F]): F[Int] =
    start.map(n => n + 1 * 2)

And the usage is pretty straightforward:

import cats.instances.option._ // for Functor
import cats.instances.list._
// for Functor
doMath(Option(20))
// res3: Option[Int] = Some(22)
doMath(List(1, 2, 3))
// res4: List[Int] = List(3, 4, 5)

How should I understand the type constructor in the method signature (F[_])? A couple of pages earlier it was said, that the type parameter should be provided to create a type. Here the whole thing (F[_]) is a type parameter and it looks, that _ is a wildcard, so that the compiler can infer the type parameter of F.

The type constructor F[_] is required to be a member of the Functor typeclass. This constraint is put on F by the implicit parameter list

(implicit functor: Functor[F])

The whole signature

def doMath[F[_]](start: F[Int])(implicit functor: Functor[F]): F[Int]

might be interpreted as follows

Given any type constructor F that is a member of Functor typeclass, then doMath can transform effectful value of type F[Int] to another effectful value of type F[Int].

where I use the phrase effectful value to emphasise that it is not a value of raw type such as Int but instead a value of type constructed after applying type constructor F to type argument Int, namely F[Int].

Furthermore I use the phrase member of in the sense of

forms a, or participates in, or has a relationship

Note the usage of underscore _ in this context is not related to inference. The F[X] and F[_] type constructor notations mean exactly the same thing. The type argument X is not used anywhere in the rest of the method signature, and for that reason by convention we use the underscore syntax F[_]. Another convention is to use lower-case x in F[x], as opposed to F[X], to emphasise x is not used.

Indeed F[_] is a type parameter in its own right and when type constructor Functor is applied to it we get proper type Functor[F] even though both F and Functor are type constructors, for example

scala> :kind -v List
List's kind is F[+A]
* -(+)-> *
This is a type constructor: a 1st-order-kinded type.

scala> :kind -v cats.Functor
cats.Functor's kind is X[F[A]]
(* -> *) -> *
This is a type constructor that takes type constructor(s): a higher-kinded type.

scala> :kind -v cats.Functor[List]
cats.Functor[List]'s kind is A
*
This is a proper type.