I typed Eval cbv in id. in CoqIde and received the message
= fun x : ?a => x
: ?a -> ?a`
What does this mean? What does the question mark mean?
A name prefixed with a question mark is called a metavariable. It's an unknown term, which may become known later during the typechecking process, but here there is nothing else to typecheck outside of id, so it remains unknown.
id has an implicit argument. Try the command About id. It will tell you that id has type forall a, a -> a, and also that the first argument a is implicit and maximally inserted. When you type id, the interpreter expands it to id _, inserting an hole _ for that first argument, and then fresh metavariables ?a are generated in place of holes.
id ?a has type ?a -> ?a and evaluates to fun x : ?a => x.