Code as data is, while not simple in a type theoretic context, pretty well researched. I think the most promising method for achieving semantics relatively close to Lisp's `code type` is the modal type theory work from the early 2000's. It starts (according to most accounts) with Pfenning and Davies work from '94-'95 [1], then moves over to Taha,Sheard,et al's work circa 2000 on MetaML[2]. Then I think the work by Kim, et al in 2006[3] which led to Murase's work in 2017[4].

This line of work delves pretty deeply into the proof-theoretic foundations and type-theoretic of macros as a well founded element of programming languages. However, I am a firm believer in the theory of best fit for this sort of problem. A large amount of the work is based on a relatively small amount of primitive concepts, and in a language like Lisp with imperative features and mutable state, a safe implementation that is algorithmically checkable should be possible, without attempting to prove the categorical semantics of the construct.

Long story short, I think that a 'safe' and useable typed syntactic macro construct should not be thought of as intractable, but approached with sensible guide rails to implementation and then used as needed by developers.

[1] - https://dl.acm.org/doi/pdf/10.1145/237721.237788 (A Modal Analysis of Staged Computation [Davies,Pfenning 2001] [2] - https://www.sciencedirect.com/science/article/pii/S030439750... (MetaML and multi-stage programming with explicit annotations [Taha,Sheard 2000] [3] - http://kwangkeunyi.snu.ac.kr/paper/06-popl-kiyicr.pdf (A Polymorphic Modal Type System for Lisp-Like Multi-Staged Languages [Kim,etal 2006]) [4] - https://lfmtp.org/workshops/2017/inc/slides/murase.pdf (slides from a talk)