Variant of free logic that accepts domain emptiness but rejects non-referring terms

To my naive perspective, domains that might be empty and terms that fail to denote (via constant symbols that don’t refer or partial functions) feel radically different. The former seems ordinary and the latter seems quite novel.

The SEP article on free logic mentions the following passage about free and inclusive logics and the differences between them (emphasis mine).

Classical predicate logic presumes not only that all singular terms
refer to members of the quantificational domain D, but also that D is
nonempty. Free logic rejects the first of these presumptions.
Inclusive logic (sometimes also called empty or universally free
logic) rejects them both. Thus while inclusive logic for a language
containing singular terms must be free, free logics need not be
inclusive.

This leaves open the possibility of accepting domain emptiness and rejecting non-referring terms. I didn’t see any mention of it in that article or the one on second and higher-order logics, which seems to mostly focus on model theory, semantics, and decidability.

Allow empty domains while rejecting partial functions and non-referring constants seems very, very familiar to me and I’m wondering if systems with this property have a name.

---

The following is a personal "notation" of sorts that I’ve been using for years without carefully examining; I’m including it here in the hopes that it’ll be familiar to folks with a similar background and to provide motivation for the question. The purpose for the notation (which is really just higher order logic used without a fixed deductive system accompanying it) is to resolve ambiguities related to quantifier scope in natural language when explaining things or taking notes.

The syntactic convention I’m most familiar with for informal/quasiformal use is cobbled together from some experience I have with programming, basic type theory, math, and semantics of natural languages. Anything vaguely collection-like can appear after the : and → builds larger types or "things that can be quantified over" by making a collection of functions. Maybe others use a similar notation informally, I’m not sure.

∀x:A→B.P(x)∧Q(x)

In such a system, empty domains do not cause any problems. A forall statement is always true when the domain is empty and an exists statement is always false.

Terms that don’t refer however, cause serious problems because the whole resulting well-formed formula will fail to "type check". I usually handled them with relations or a special sort that included a designated bottom element (similar to an option type in programming).