There are a number of issues to be addressed from clarity of the written code to efficiency of the compiled code. For beginners, I think the clarity issue is more important so I'll address that first.
Before I begin, though, I'll also note that the inferred typing of variables in C# is still static (compile time), strong (types don't change) typing. That hasn't changed. Inferred typing is just a syntactic hack (syntactic sugar) that appear to make the programmer's job easier. However, that is only true when you are writing the program the first time, not when you are updating/modifying/maintaining the program.
I'll note also, that programming languages are for people, not for computers. Compilers take the human-understandable code that we write and transform it into something that a machine can utilize.
Specifying the type of a variable in a declaration, while not always required introduces a kind of good redundancy. Much redundancy in programming is bad (repeating a sequence of statements) but redundancy in typing is good since it makes the intent of the programmer clearer and also, in some situations finds errors in a program at compile time that could otherwise only become noticeable at run-time. This lets the programmer fix issues earlier in the development process, which, research shows, reduces cost.
Think of the phases of program development as follows: conceptualization, analysis, design, coding, testing, deployment, maintenance (maybe not a universally agreed list, I realize). Research shows an order of magnitude increase in the cost of correction for each phase transition. If you catch the error in the conceptualization phase it costs nearly nothing to fix. (Sorry, I don't have a reference to the research - it is quite old).
When you say that a variable is int and later (or immediately) assign it an int value the compiler can check correctness. But you the program reader are also assured that your intent (x is an int) is faithfully represented in the code.
var x = 5;
reduces the redundancy. Note also that 5 is a valid value of the following C# types: byte, sbyte, int, uint, long, ulong, short, and ushort. What is your intention here. The declaration above doesn't say. The compiler will choose something it "thinks" is appropriate. By saying less about your intent you give less information to the compiler, which may then provide a less-than-optimal translation of your code. So this sort of redundancy is a good thing.
When used with objects (or otherwise polymorphic types) there is an additional consideration.
If you say
var x = new Horse("Trigger");
then the compiler has little recourse than to give x the most specific possible type. It might, in fact be preferable to give x a more general type, such as an interface type used to create the Horse class. It is generally good programming practice to give variables interface (as opposed to class) types, though this requires other rules about how interfaces are used - a separate discussion. But, in some contexts
Animal x = new Horse("Trigger");
might be preferable and it also better clarifies your intent.
None of the above uses of var is necessarily a mind-killer, but an alternative use of what I want to call sloppy typing is.
Suppose you declare a new object reference as follows:
Object x = new Horse("Trigger");
Now you have likely introduced a mess into your program. Later on, you will probably want to say
int howMany = x.count();
(We know, horses like Trigger can count, of course). The compiler will complain about this, of course since x is only known as an Object reference, not a Horse reference. The sloppy typer will then cast x to quiet the complaints of the compiler:
int howMany = ((Horse)x).count();
which is, of course ugly. We need to assure the compiler that x is, indeed, a Horse so that the count method is available. However, this cast introduces a check into the runtime code, which is both inefficient and can be wrong. What if somewhere else prior to this x was reassigned to an Aardvark object. Then whether or not Aardvarks can count or not, the run-time type check will flag an error.
This sloppy typing combined with casting is an attempt to replace the normal static type checking with dynamic type checking (as is done in, say Python). But that is misuse of the language.
Moreover, it introduces a maintenance nightmare into your program. You declare a variable in your program to have a given type, but in use it has a different (more specific) type. The compiler isn't going to remember those actual types for you, so you have to do this yourself. You can't look back to the declaration of x to find out what sort of thing it represents, you have to keep the details of the dynamic system in mind for every use of the variable. In a program of any size this is obviously infeasible. It is why we have types (and also polymorphism) in the first place.
Again, this sort of casting (down casting) is a recognized Code Smell, indicating poor design. Every explicit cast in a program is a potential point of error. Just Say No.
For completeness, let me give a few rules here that will lead to better design and better code.
When you declare a variable give it an interface type (rather than a class type) - a good but not essential rule. Interfaces define concepts.
When you implement that interface the only public methods of the class should be those defined in the interface. You won't need to cast. - an essential rule.
When you extend a class (create a subclass) the only public methods in the subclass should be those declared in the superclass. Essential. If you need more methods then you have a different concept than the superclass, so extend the interface of the original class to define the new concept and then have the subclass also implement the new interface.
When you declare a variable to have some (object) type, don't try to send messages defined only in some subtype, requiring casting.
The above rules are intended to make your programs easier to understand, hence easier to update and maintain. When tempted to break the rules, spend a bit of time asking why, and looking to see if you can come up with a better design. Breaking the rules tends to make your overall program into a Big Ball of Mud.
All of the above has focused, primarily, on clarity of the code for the programmer's benefit. But efficiency is also a consideration.
The more you can inform the compiler of your intent, the better job it can do in its translation. Some languages optimize for expressing intent rather than process, in fact. Database languages and Logic languages do this explicitly. If you tell a compiler how to do something it will be constrained to follow your directions. But if you tell it what you want, rather than how to achieve it, it has more options and can do better optimizations. So, explicit typing in programs is also a way to communicate intent (what) to the compiler rather than forcing later checks (casts). So, maybe x in our first example really only needs to be a short, or even a byte. But the declaration using var probably won't achieve that.
I also realize that "abstract" names like
x are a poor choice. I only use it here as I don't have a context in which to provide an intention revealing name.
Implicit typing is probably an incorrect term for this. FORTRAN had implicit typing where the type of a variable depends on the spelling of the name. Names beginning with I through N were implicitly Integer unless a specific declaration implied otherwise. Other names indicated Real variables.
On the other hand, Standard ML and related languages have a subsystem in the compiler that could infer types (type inference). ML has strong static typing also, but programmers seldom need to specify a type since the compiler can ordinarily figure it out.
But use of var isn't dynamic typing either. In dynamic typing (Python, Ruby), variables (names) don't have type. Only values have type. Dynamic typing can still be strong typing, but it is done at run-time, not compile-time. Errors are found later unless they are rigorously rooted out through testing during development.
The biological classification of Carl Linnaeus is probably a poor analogy to use for subclassing and polymorphism. Each entry in the classification tree is a different concept and all are abstract. There is no such thing as a pure Mammal. Moreover, classes define behavior of objects (via public methods) and the Linnaeus classification system is nothing about behavior. Trying to use it to generate examples of subclassing is one of the reasons students get terrible ideas about what should be done in a subclass.