> There’s the technical aspects of the fact that every language has to have some notion of “type”

This isn't true. There are no types in lisp or untyped lambda calculus.

Common Lisp has a primitive type system. Some implementations use that for compile-time type checks:

An integer type I1 from 0 to 65535.

    (deftype i1 (&optional (min 0) (max 65535))
      `(integer ,min ,max))

The function foo gets an integer and returns an I1:

    (declaim (ftype (function (integer) i1)
                    foo))

    (defun foo (i)
      (mod i 65536))

    (defun test ()
      (foo 6712312)       ; okay
      (foo 311212.2))     ; wrong call

Let's compile it in SBCL, a Common Lisp compiler:

    ; compiling file "/private/tmp/test.lisp" (written 08 JUL 2017 11:10:09 AM):
    ; compiling (DEFTYPE I1 ...)
    ; compiling (DECLAIM (FTYPE # ...))
    ; compiling (DEFUN FOO ...)
    ; compiling (DEFUN TEST ...)
    ; file: /private/tmp/test.lisp
    ; in: DEFUN TEST
    ;     (FOO 311212.2)
    ; 
    ; note: deleting unreachable code
    ; 
    ; caught WARNING:
    ;   Constant 311212.2 conflicts with its asserted type INTEGER.
    ;   See also:
    ;     The SBCL Manual, Node "Handling of Types"
    ; 
    ; compilation unit finished
    ;   caught 1 WARNING condition
    ;   printed 1 note

As you can see that it detects the type error.

The type system has been defined for Common Lisp with its first version in 1984. It had been used to allow the compiler to generate optimized code or to do more precise runtime checks. Early on in the mod 80s the CMUCL compiler then added the idea to use these type declarations as type assertions and to check those at compile time.

Actually, there's one type.

If you're going to shove the system into a typed model, then sure there is one type. But then you've kind of missed the point...

If you're going to answer the question of whether a language has types, then you're already trying to see how it can be shoved into types. It's presupposed by the question itself.

You literally have to count the types by analyzing the grammar. So for the lambda calculus, you have lambda=1, halt. So does a single type mean no types or literally one type?

What's the advantage of thinking that 1 type actually equals 0 types? I don't see any, so in my mind, all languages are unityped or have a richer type structure. Whether a richer type structure is desirable is a separate question.