;;; Type inference, layer 0: the type representation and unification.
;;;
;;; Nothing in the compiler calls this unit yet. It is the ground floor
;;; of the pass described in Type-inference.org -- built and tested on
;;; its own before a single form is routed through it.
;;;
;;; Two representations meet here. *Surface* types are the forms the
;;; rest of the compiler passes around -- `int', `(* const char)',
;;; `(¤ int 16)', `(fn ((int)) int)'. They are what the reader
;;; produces, what the C writer consumes and what `type-match' compares
;;; with `equal?', and they are hopeless for unification. The *IR*
;;; below is the other one: mutable cells, so that solving a type
;;; variable is a side effect rather than a substitution rebuilt at
;;; every step.
;;;
;;; `parse-type' and `unparse-type' are the boundary between the two,
;;; and they carry the whole compatibility burden: `unparse-type' must
;;; produce the exact spelling `type-match' compares against, or the
;;; reflection macros break by silently falling into their `else'
;;; branch. That is what the round-trip test in tests/infer.scm is for,
;;; and why it is driven by every type spelling that appears in the
;;; repository.

(import
  scheme
  (scheme base)
  (chicken base)
  matchable
  srfi-1
  srfi-69
  types
  utils)

;;; ---------------------------------------------------------------
;;; The IR
;;; ---------------------------------------------------------------

;;; A type variable is a mutable cell. `ref' is #f while unsolved and
;;; the type it stands for once bound -- union-find, with the path
;;; compression done in `resolve'.
;;;
;;; `classes' is the list of type classes the variable must satisfy
;;; (`numeric', and one day `ord'); see "constraints" below. `rigid?'
;;; marks a variable that must not unify with anything but itself --
;;; unused until a `fn' grows type parameters, and five lines now
;;; against an IR change later.
(define-record-type <tvar>
  (%make-tvar id ref classes rigid?)
  tvar?
  (id tvar-id)
  (ref tvar-ref tvar-ref-set!)
  (classes tvar-classes tvar-classes-set!)
  (rigid? tvar-rigid?))

;;; A primitive or otherwise nominal type. `name' is the list of words
;;; making it up, so `int', `(unsigned int)' and `(long long)' are all
;;; one node, and so is a name we have never parsed a declaration for
;;; (`size-t', `GLuint'). The two cases are told apart by
;;; `c-primitive?', which is what keeps a constraint over an unparsed C
;;; typedef from being an error.
(define-record-type <prim>
  (make-prim name quals)
  prim-type?
  (name prim-name)
  (quals prim-quals))

(define-record-type <ptr>
  (make-ptr target quals)
  ptr-type?
  (target ptr-target)
  (quals ptr-quals))

;;; `size' is an integer, or #f for `(¤ int)' -- an array of unwritten
;;; length.
(define-record-type <array>
  (make-array-type elt size)
  array-type?
  (elt array-elt)
  (size array-size))

(define-record-type <fn>
  (make-fn-type ret args variadic?)
  fn-type?
  (ret fn-ret)
  (args fn-args)
  (variadic? fn-variadic?))

;;; struct / union / enum. Nominal: two of them are the same type when
;;; they are the same kind and the same name. `spelling' is the surface
;;; form it was written as, kept verbatim so that an aggregate defined
;;; inline in a type position round-trips unchanged.
(define-record-type <agg>
  (make-agg kind name spelling quals)
  agg-type?
  (kind agg-kind)
  (name agg-name)
  (spelling agg-spelling)
  (quals agg-quals))

;;; A typedef. Transparent to unification -- it unifies as whatever it
;;; expands to -- and opaque to printing, so a diagnostic and a
;;; generated declaration both say `size-t' rather than `unsigned long'.
(define-record-type <alias>
  (make-alias name expansion quals)
  alias-type?
  (name alias-name)
  (expansion alias-expansion)
  (quals alias-quals))

;;; `?'. Sex has full C interop, so `printf', `SDL-CreateWindow' and
;;; `size-t' arrive from headers nobody parsed. Rather than reject
;;; every real program, the lattice gets a top element: `?' is
;;; consistent with every type and constrains nothing.
(define-record-type <unknown>
  (%make-unknown)
  unknown-type?)

(define the-unknown-type (%make-unknown))

(define tvar-counter 0)

(define (fresh-tvar . classes)
  (set! tvar-counter (+ tvar-counter 1))
  (%make-tvar tvar-counter #f (if (null? classes) (list) (car classes)) #f))

(define (fresh-rigid-tvar . classes)
  (set! tvar-counter (+ tvar-counter 1))
  (%make-tvar tvar-counter #f (if (null? classes) (list) (car classes)) #t))

;;; Follow a bound variable to what it stands for, compressing the path
;;; on the way out. Every procedure that looks at a type's shape starts
;;; here.
(define (resolve type)
  (if (and (tvar? type) (tvar-ref type))
      (let ((target (resolve (tvar-ref type))))
        (tvar-ref-set! type target)
        target)
      type))

;;; ...and through any typedef as well, for the places that care what a
;;; type *is* rather than what it is called.
(define (underlying type)
  (let ((t (resolve type)))
    (if (alias-type? t)
        (underlying (alias-expansion t))
        t)))

(define (type-quals type)
  (cond ((prim-type? type) (prim-quals type))
        ((ptr-type? type) (ptr-quals type))
        ((agg-type? type) (agg-quals type))
        ((alias-type? type) (alias-quals type))
        (else (list))))

;;; Array-to-pointer and function-to-function-pointer, for the
;;; positions where C decays: a call argument, an operand of `+', the
;;; subscripted half of `(¤ a i)'.
(define (decay type)
  (let ((t (underlying type)))
    (cond ((array-type? t) (make-ptr (array-elt t) (list)))
          ((fn-type? t) (make-ptr t (list)))
          (else (resolve type)))))

(define (free-tvars type)
  (let collect ((t type) (acc (list)))
    (let ((t (resolve t)))
      (cond ((tvar? t) (if (memq t acc) acc (cons t acc)))
            ((ptr-type? t) (collect (ptr-target t) acc))
            ((array-type? t) (collect (array-elt t) acc))
            ((alias-type? t) (collect (alias-expansion t) acc))
            ((fn-type? t) (fold collect (collect (fn-ret t) acc) (fn-args t)))
            (else acc)))))

;;; ---------------------------------------------------------------
;;; Surface -> IR
;;; ---------------------------------------------------------------

(define +qualifiers+ '(const volatile restrict))

(define (qualifier? word) (memq word +qualifiers+))

;;; `(const char)' written as `((const char))' is the same type: a
;;; sublist that merely groups. The C writer unwraps these too.
(define (maybe-unwrap type)
  (if (and (list? type) (= 1 (length type)))
      (car type)
      type))

(define (parse-type surface)
  (cond
   ((symbol? surface) (parse-words (list surface) (list) surface))
   ((not (pair? surface)) (sex-error surface "not a type" surface))
   ((eq? (car surface) '¤) (parse-array surface))
   ((eq? (car surface) 'fn) (parse-fn surface))
   ((memq '* surface) (parse-pointer-chain surface))
   (else (parse-words surface (list) surface))))

;;; A `*'-free run of words: qualifiers, then whatever they qualify.
;;; `form' is only carried along so a complaint can say where it was
;;; written.
(define (parse-words words quals form)
  (cond
   ((null? words) (sex-error form "type is nothing but qualifiers" form))
   ((qualifier? (car words))
    (parse-words (cdr words) (cons (car words) quals) form))
   ;; A single sublist left: grouping parens, as in (* (const struct s))
   ((and (null? (cdr words)) (pair? (car words)))
    (with-quals (parse-type (car words)) (reverse quals)))
   ((memq (car words) '(struct union enum)) (parse-agg words (reverse quals)))
   ((eq? (car words) '¤) (parse-array words))
   ((eq? (car words) 'fn) (parse-fn words))
   ((memq '* words) (parse-pointer-chain (append (reverse quals) words)))
   (else (parse-name words (reverse quals) form))))

;;; A name, one word or several: `int', `size-t', `(unsigned int)'.
(define (parse-name words quals form)
  (cond
   ((not (every symbol? words)) (sex-error form "malformed type" form))
   ;; The type-level wildcard. It is a fresh variable wherever it
   ;; appears, which is what makes partial types -- `(* _)', `(¤ _ 4)'
   ;; -- fall out for free rather than needing their own grammar.
   ((equal? words '(_)) (fresh-tvar))
   ((and (null? (cdr words)) (get-underlying-type (car words)))
    => (lambda (target)
         (make-alias (car words) (parse-type target) quals)))
   (else (make-prim words quals))))

;;; ([pub] struct name), (struct name (fields ...)), (struct (fields ...))
(define (parse-agg words quals)
  (let* ((kind (car words))
         (name (and (pair? (cdr words)) (symbol? (cadr words)) (cadr words))))
    (make-agg kind name words quals)))

;;; (¤ elt ... size) -- the size is the last element when it is an
;;; integer, and absent otherwise. The element words are unwrapped the
;;; way the C writer unwraps them, so `[int 16]' and `[(int) 16]' are
;;; one type.
(define (parse-array surface)
  (let* ((rest (cdr surface))
         (sized? (and (pair? rest) (integer? (last rest))))
         (size (and sized? (last rest)))
         (words (if sized? (drop-right rest 1) rest)))
    (when (null? words)
      (sex-error surface "array type without an element type" surface))
    (make-array-type (parse-type (maybe-unwrap words)) size)))

;;; (fn ((int) (float)) void). Argument entries are types, not named
;;; parameters -- a `fn' in type position has no room for names.
(define (parse-fn surface)
  (match surface
    (('fn (? list? arglist) ret)
     (let* ((variadic? (and (pair? arglist) (variadic-marker? (last arglist))))
            (entries (if variadic? (drop-right arglist 1) arglist)))
       (make-fn-type (parse-type ret)
                     (map (lambda (entry) (parse-type (maybe-unwrap entry)))
                          entries)
                     variadic?)))
    (else (sex-error surface "malformed function type" surface))))

;;; `...' in an arglist, written bare or wrapped the way every other
;;; entry is.
(define (variadic-marker? entry)
  (or (eq? entry '...) (equal? entry '(...))))

;;; Pointer chains are written flat and read right to left: the last
;;; `*'-separated run is the pointed-to type, and each run before it
;;; qualifies one level of indirection. `(const * const char)' is a
;;; const pointer to a const char.
(define (parse-pointer-chain words)
  (let* ((segments (list-split words '*))
         (base (last segments))
         (levels (reverse (drop-right segments 1))))
    (when (null? base)
      (sex-error words "pointer to nothing" words))
    (fold (lambda (level acc)
            (unless (every qualifier? level)
              (sex-error words "only qualifiers may sit between two `*'" words))
            (make-ptr acc level))
          (parse-words (maybe-unwrap-segment base) (list) words)
          levels)))

(define (maybe-unwrap-segment segment)
  (let ((s (maybe-unwrap segment)))
    (if (list? s) s (list s))))

;;; Re-qualify a parsed type, for the grouping case `(const (struct s))'
;;; where the qualifier is read before the thing it qualifies.
(define (with-quals type quals)
  (if (null? quals)
      type
      (cond ((prim-type? type) (make-prim (prim-name type)
                                          (append quals (prim-quals type))))
            ((ptr-type? type) (make-ptr (ptr-target type)
                                        (append quals (ptr-quals type))))
            ((agg-type? type) (make-agg (agg-kind type) (agg-name type)
                                        (agg-spelling type)
                                        (append quals (agg-quals type))))
            ((alias-type? type) (make-alias (alias-name type)
                                            (alias-expansion type)
                                            (append quals (alias-quals type))))
            (else type))))

;;; ---------------------------------------------------------------
;;; IR -> surface
;;; ---------------------------------------------------------------

;;; Every result here has to be the spelling the rest of the compiler
;;; already writes by hand, since `type-match' compares with `equal?'
;;; and a near miss is silent.
(define (unparse-type type)
  (let ((t (resolve type)))
    (cond
     ((tvar? t) '_)
     ((unknown-type? t) '?)
     ((alias-type? t) (qualify (alias-quals t) (list (alias-name t))))
     ((prim-type? t) (qualify (prim-quals t) (prim-name t)))
     ((agg-type? t) (qualify (agg-quals t) (agg-spelling t)))
     ((ptr-type? t)
      (append (ptr-quals t) (list '*) (as-words (unparse-type (ptr-target t)))))
     ((array-type? t)
      (let ((elt (as-words (unparse-type (array-elt t)))))
        (append (list '¤)
                (if (and (pair? elt) (eq? (car elt) '¤)) (list elt) elt)
                (if (array-size t) (list (array-size t)) (list)))))
     ((fn-type? t)
      (list 'fn
            (append (map (lambda (arg) (as-arg (unparse-type arg))) (fn-args t))
                    (if (fn-variadic? t) (list '(...)) (list)))
            (unparse-type (fn-ret t))))
     (else (error "unparse-type: not a type" t)))))

;;; A one-word type is written bare, anything longer as a list --
;;; `int', but `(const int)' and `(struct point)'.
(define (qualify quals words)
  (let ((all (append quals words)))
    (if (and (null? quals) (= 1 (length all)))
        (car all)
        all)))

;;; An argument in a `fn' type is written as a list even when it is one
;;; word -- `((int) (float))' -- so only an atom needs wrapping.
(define (as-arg surface)
  (if (pair? surface) surface (list surface)))

;;; Splice a type into a surrounding word list, the way `(* const char)'
;;; and `[* const char]' splice theirs. An array keeps its parentheses:
;;; `(¤ ¤ char 4)' would read back as something else entirely.
(define (as-words surface)
  (cond ((not (pair? surface)) (list surface))
        ((memq (car surface) '(¤ fn)) (list surface))
        (else surface)))

;;; ---------------------------------------------------------------
;;; Constraints
;;; ---------------------------------------------------------------

;;; `(numeric a)' is already a type class, so it is written as one from
;;; the start: one representation, one table, one entailment check. A
;;; trait bound `(ord (struct circle))' is the same shape, discharged
;;; the same way, and reported by the same procedure -- which is the
;;; whole reason to build it this way while there is only one kind of
;;; constraint to build.
;;;
;;; `default' is the type an unresolved constraint falls back to, the
;;; way Haskell defaults `Num a' to Integer. `test' is how the built-in
;;; classes say "every arithmetic type" without enumerating twenty
;;; spellings as instances; a user trait has no test and lives entirely
;;; in the instance table. `strict?' marks a class that must not be
;;; guessed at: static dispatch needs a real instance, so `?' fails it.
(define-record-type <type-class>
  (%make-type-class name default test strict?)
  type-class?
  (name type-class-name)
  (default type-class-default)
  (test type-class-test)
  (strict? type-class-strict?))

(define +classes+ (make-hash-table))
(define +instances+ (make-hash-table))

(define (register-class! name default test strict?)
  (hash-table-set! +classes+ name (%make-type-class name default test strict?)))

(define (get-class name)
  (or (hash-table-ref/default +classes+ name #f)
      (error "no such type class" name)))

;;; Instances key on the *resolved* type, so `(impl show for size-t)'
;;; and `(impl show for unsigned long)' collide rather than quietly
;;; coexisting as two instances of one C type.
(define (instance-key type)
  (unparse-type (underlying type)))

(define (add-instance! class-name type)
  (hash-table-set! +instances+ (cons class-name (instance-key type)) #t))

(define (has-instance? class-name type)
  (hash-table-exists? +instances+ (cons class-name (instance-key type))))

;;; #t, #f, or 'unknown -- and the third answer is the important one.
;;; A C name we never parsed a declaration for might well be numeric;
;;; saying #f there would reject working programs, and saying #t would
;;; invent knowledge. 'unknown means "do not constrain, do not
;;; complain".
(define (entails? class-name type)
  (let ((cls (get-class class-name))
        (t (underlying type)))
    (cond
     ((tvar? t) 'unknown)
     ;; `?' is consistent with every type, but it entails nothing:
     ;; there is no instance to select and no name to mangle.
     ((unknown-type? t) (if (type-class-strict? cls) #f 'unknown))
     ((has-instance? class-name t) #t)
     ((type-class-test cls) => (lambda (test) (test t)))
     (else #f))))

(define +integer-words+ '(char short int long signed unsigned bool _Bool))
(define +float-words+ '(float double))
(define +known-words+ (append '(void) +integer-words+ +float-words+))

;;; A prim built only out of words we recognise. Anything else is a
;;; name from a header, and we have no opinion about it.
(define (c-primitive? t)
  (and (prim-type? t)
       (every (lambda (word) (memq word +known-words+)) (prim-name t))))

(define (void-type? t)
  (and (prim-type? t) (equal? (prim-name t) '(void))))

(define (arithmetic-type? t)
  (cond ((and (agg-type? t) (eq? (agg-kind t) 'enum)) #t) ; an enum is an integer
        ((not (prim-type? t)) #f)
        ((not (c-primitive? t)) 'unknown)
        ((void-type? t) #f)
        (else #t)))

(define (integral-type? t)
  (cond ((and (agg-type? t) (eq? (agg-kind t) 'enum)) #t)
        ((not (prim-type? t)) #f)
        ((not (c-primitive? t)) 'unknown)
        ((void-type? t) #f)
        ((any (lambda (word) (memq word +float-words+)) (prim-name t)) #f)
        (else #t)))

(define (floating-type? t)
  (cond ((not (prim-type? t)) #f)
        ((not (c-primitive? t)) 'unknown)
        (else (and (any (lambda (word) (memq word +float-words+)) (prim-name t))
                   #t))))

(define (scalar-type? t)
  (cond ((ptr-type? t) #t)
        ((array-type? t) #t)            ; decays to one
        ((fn-type? t) #t)               ; likewise
        (else (arithmetic-type? t))))

;;; The built-ins. They are ordinary classes, registered the same way a
;;; trait will be -- that is the point.
(register-class! 'numeric  'int    arithmetic-type? #f)
(register-class! 'integral 'int    integral-type?   #f)
(register-class! 'floating 'double floating-type?   #f)
(register-class! 'scalar   #f      scalar-type?     #f)

;;; A constraint that survives to the end of a function is defaulted:
;;; `(numeric a)' with nothing else known is an `int'. A *strict*
;;; class has no default and no business guessing, so an unresolved one
;;; is an error -- the rule is worth stating while there is only one
;;; kind of constraint to state it about.
(define (default-tvar! v form)
  (let ((strict (find (lambda (c) (type-class-strict? (get-class c)))
                      (tvar-classes v))))
    (cond
     (strict (sex-error form "unresolved constraint" (list strict (unparse-type v))))
     ((find (lambda (c) (type-class-default (get-class c))) (tvar-classes v))
      => (lambda (c)
           (tvar-ref-set! v (parse-type (type-class-default (get-class c))))
           #t))
     (else #f))))

;;; Default every variable still open in TYPE. Returns #t when none is
;;; left unsolved, so a caller can tell "inferred" from "give up and
;;; ask for the type in writing".
(define (default-type-variables! type form)
  (fold (lambda (v ok) (and (default-tvar! v form) ok))
        #t
        (free-tvars type)))

(define (check-classes classes type form)
  (for-each
   (lambda (c)
     (when (eq? #f (entails? c type))
       (sex-error form "type does not satisfy a constraint"
                  (list c (unparse-type type)))))
   classes))

;;; ---------------------------------------------------------------
;;; Unification
;;; ---------------------------------------------------------------

;;; Consistency in the gradual-typing sense rather than equality: `?'
;;; succeeds against anything and binds nothing, which is what keeps
;;; the pass from rejecting every program that includes a C header.
;;;
;;; FORM is carried only so a failure can say where it was written.
(define (unify t1 t2 form)
  (let ((a (resolve t1))
        (b (resolve t2)))
    (cond
     ((eq? a b) #t)
     ((unknown-type? a) #t)
     ((unknown-type? b) #t)
     ;; Whichever side is free takes the binding, so that a rigid
     ;; variable is solved *to* rather than solved, in either order.
     ;; Both rigid and distinct is the mismatch `eq?' above let through.
     ((and (tvar? a) (not (tvar-rigid? a))) (bind-tvar! a b form))
     ((and (tvar? b) (not (tvar-rigid? b))) (bind-tvar! b a form))
     ((or (tvar? a) (tvar? b)) (type-mismatch a b form))
     ;; A typedef unifies as what it stands for. Its name survives in
     ;; whichever side is printed later, since neither side is rebuilt.
     ((alias-type? a) (unify (alias-expansion a) b form))
     ((alias-type? b) (unify a (alias-expansion b) form))
     ((and (prim-type? a) (prim-type? b))
      (check-quals a b form)
      (or (equal? (prim-name a) (prim-name b))
          (type-mismatch a b form)))
     ((and (ptr-type? a) (ptr-type? b))
      (check-quals a b form)
      (unify (ptr-target a) (ptr-target b) form))
     ((and (array-type? a) (array-type? b))
      ;; One of them may be `(¤ int)': an unwritten length constrains
      ;; nothing, the way it does not in C either.
      (when (and (array-size a) (array-size b)
                 (not (= (array-size a) (array-size b))))
        (type-mismatch a b form))
      (unify (array-elt a) (array-elt b) form))
     ((and (fn-type? a) (fn-type? b))
      (unless (and (= (length (fn-args a)) (length (fn-args b)))
                   (eq? (fn-variadic? a) (fn-variadic? b)))
        (type-mismatch a b form))
      (unify (fn-ret a) (fn-ret b) form)
      (for-each (lambda (x y) (unify x y form)) (fn-args a) (fn-args b))
      #t)
     ((and (agg-type? a) (agg-type? b))
      (check-quals a b form)
      (or (and (eq? (agg-kind a) (agg-kind b))
               (if (and (agg-name a) (agg-name b))
                   (eq? (agg-name a) (agg-name b))
                   (equal? (agg-spelling a) (agg-spelling b))))
          (type-mismatch a b form)))
     (else (type-mismatch a b form)))))

(define (type-mismatch a b form)
  (sex-error form "type mismatch: expected"
             (unparse-type a) 'got (unparse-type b)))

;;; Qualifiers are compared, and a mismatch is a warning rather than a
;;; failure: C's const-correctness is not this pass's fight yet, and
;;; making it one would reject programs that compile today.
(define (check-quals a b form)
  (let ((qa (type-quals a))
        (qb (type-quals b)))
    (unless (lset= eq? qa qb)
      (sex-warning form "qualifiers differ between"
                   (unparse-type a) "and" (unparse-type b)))))

(define (bind-tvar! v t form)
  (cond
   ;; Without recursive types this cannot trigger. It is four lines,
   ;; and the alternative to having it is a hang.
   ((occurs? v t) (sex-error form "recursive type" (unparse-type v)))
   ;; A rigid variable is a type *parameter*: inside a generic body it
   ;; stands for one specific unknown type and must not be solved.
   ((tvar-rigid? v) (type-mismatch v t form))
   (else
    (when (tvar? t)
      (tvar-classes-set! t (lset-union eq? (tvar-classes t) (tvar-classes v))))
    (tvar-ref-set! v t)
    (unless (tvar? t)
      (check-classes (tvar-classes v) t form))
    #t)))

(define (occurs? v type)
  (let ((t (resolve type)))
    (cond ((eq? v t) #t)
          ((ptr-type? t) (occurs? v (ptr-target t)))
          ((array-type? t) (occurs? v (array-elt t)))
          ((alias-type? t) (occurs? v (alias-expansion t)))
          ((fn-type? t) (or (occurs? v (fn-ret t))
                            (any (lambda (a) (occurs? v a)) (fn-args t))))
          (else #f))))

;;; ---------------------------------------------------------------
;;; Type schemes
;;; ---------------------------------------------------------------

;;; Nothing generalizes yet -- every `fn' in Sex carries a written
;;; signature and there is no polymorphism to abstract over. These are
;;; here because they are ten lines on top of unification and because
;;; they are exactly what a `fn' with type parameters needs, and
;;; because a scheme without a constraint list is the wrong shape for
;;; every bounded generic. `(forall vars constraints type)' it is,
;;; from the start.
(define-record-type <scheme>
  (make-scheme vars constraints type)
  scheme?
  (vars scheme-vars)
  (constraints scheme-constraints)
  (type scheme-type))

;;; Quantify over everything free in TYPE that is not also free in the
;;; environment, carrying each variable's class constraints along as
;;; the scheme's context.
(define (generalize type env-tvars)
  (let ((vars (lset-difference eq? (free-tvars type) env-tvars)))
    (make-scheme vars
                 (append-map (lambda (v)
                               (map (lambda (c) (cons c v)) (tvar-classes v)))
                             vars)
                 type)))

(define (instantiate scheme)
  (let ((subst (map (lambda (v) (cons v (fresh-tvar (tvar-classes v))))
                    (scheme-vars scheme))))
    (substitute (scheme-type scheme) subst)))

;;; Structural copy with the variables in SUBST replaced. Copying is
;;; how a generic body must be handled anyway -- `form-type' is keyed
;;; by cons cell, one form one type, so an instantiation gets fresh
;;; cells rather than a second type for the same cell.
(define (substitute type subst)
  (let ((t (resolve type)))
    (cond
     ((tvar? t) (let ((hit (assq t subst))) (if hit (cdr hit) t)))
     ((ptr-type? t) (make-ptr (substitute (ptr-target t) subst) (ptr-quals t)))
     ((array-type? t) (make-array-type (substitute (array-elt t) subst)
                                       (array-size t)))
     ((alias-type? t) (make-alias (alias-name t)
                                  (substitute (alias-expansion t) subst)
                                  (alias-quals t)))
     ((fn-type? t) (make-fn-type (substitute (fn-ret t) subst)
                                 (map (lambda (a) (substitute a subst))
                                      (fn-args t))
                                 (fn-variadic? t)))
     (else t))))