Can Typed Racket Treat Types as Runtime Values?

Questions & Answers
,
1

I want to refine types without relying on predicates, so I attempted to implement ⊔, ann* and type-case. Here are usage examples of these operators:

(: flexible-length (→ (⊔ String (Listof Any)) Index))
(define (flexible-length v)
  (type-case v n
    [String (string-length n)]
    [(Listof Any) (length n)]))
(flexible-length (ann* "abc" String))        ; 3
(flexible-length (ann* '(1 2) (Listof Any))) ; 2
(flexible-length (ann* #"abc" Bytes))        ; FAIL

Below is my implementation attempt:

(define-syntax (cast* stx)
  (syntax-parse stx
    #:datum-literals (Any)
    [(_ e Any) (syntax/loc stx e)]
    [(_ e T) (syntax/loc stx (cast e T))]))

(struct (a ...) variant ([value : (∪ a ...)] [tag : Type])
  #:transparent
  #:type-name ⊔)

(define-syntax-rule (ann* e T)
  (let ([v : T e])
    (variant v (type T))))

(define-syntax (type-case stx)
  (syntax-parse stx
    [(_ e name:id [T body ...+] ...+)
     (syntax/loc stx
       (let* ([v (assert e variant?)]
              [t (variant-tag v)])
         (cond
           [(type<= t (type T))
            (define name (cast* (variant-value v) T))
            body ...]
           ...
           [else (error "FAIL")])))]))

As shown, implementing ⊔, ann* and type-case requires Type, type, and type<=. I tried representing Type as Sexp:

(define-type Type Sexp)
(define-syntax-rule (type e) (quote e))
(: type<= (→ Type Type Boolean))
(define (type<= t1 t2) (equal? t1 t2))

However, this implementation can only perform type comparison through equal?. I'm wondering if Typed Racket could provide them natively?