Thank-you for "nerdsnipe". Now I will always wonder if typelevel is nerdsniping me. For example, "at that point you're just emitting Strings." I still have a sneaking suspicion that typelevel folks would really rather be stringlevel, just comparing the names of things. In fact, I think the whole syntactic orientation of names first, optionally inferred type second, says that really we program in terms of names, with types as a backstop. Possibly we think nominally, investing names with meanings they may or may not possess, the proof of which is derived secondarily (via types).