format-id1.rkt

#lang racket

(begin-for-syntax
  (require
   racket
   racket/syntax))

(define-for-syntax (typed-identifier x body)
  (format-id x "~a1" x #:props (syntax-property
                                (syntax-property
                                 x 'definition body #t)
                                'not-free-identifier=? #t #t)))

(define-syntax (define^ syn)
  (syntax-case syn ()
    [(_ id body)
     (with-syntax ([x (typed-identifier #'id #'body)])
       #`(begin
           (define x body)
           (define-syntax id
             (make-rename-transformer #'x))))]))

(define-syntax (define^^ syn)
  (syntax-case syn ()
    [(_ id body)
     (with-syntax ([x (generate-temporary)])
       #`(begin
           (define x body)
           (define-syntax id
             (make-rename-transformer
              (syntax-property
               (syntax-property #'x 'definition #'body #t)
               'not-free-identifier=? #t #t)))))]))

(define-for-syntax (equal^? e1 e2)
  (free-identifier=? (syntax-property e1 'definition) e2))

(define-for-syntax (my-expand e)
  (local-expand e 'expression '()))

(define-syntax (:: syn)
  (syntax-case syn ()
    [(_ x e)
     (unless (equal^? (my-expand #'x) #'e)
       (error (format "Type error ~a ~a" #'x #'e)))
     #`(void)]))

(define id^ (lambda (x) x))

(define^ id id^)

(define^^ id2 id^)

(:: id2 id^)
(:: id id^)

(provide :: id id2 id^)