[racket] typed racket cps, state machines

Thanks for occasional help learning typed racket on IRC. I'm still
finding the pitfalls that await those of us used to dynamically typed
programs.

The other day I posted some cps patterns I figured out:
  http://pasterack.org/pastes/49759

Extending that to simple state machines that loop through various states
gets me into trouble. The simplest example is just looping through one
state, or not:

(define #:∀ (B0V B1V)
  (p0 (branch0 : (-> B0V))
      (branch1 : (-> B1V)))
  : (U B0V B1V)

  ;; This one is fine:
  (define (no-loop) : (U B0V B1V)
    (branch0))

  ;; insufficient type information to typecheck this one:
  (define (loop) : (U B0V B1V)
    (loop))

  ;; insufficient type information to typecheck this one too:
  (define (loop*) : (U B0V B1V)
    ((inst loop* B0V B1V)))

  ;; insufficient type information to typecheck this one too:
  (define (loop**) : (U B0V B1V)
    ((inst loop** (U B0V B1V) (U B0V B1V))))

  (no-loop)
  (loop)
  (loop*)
  (loop**))

I'm still thinking about this problem, but since I have distilled it to
the simplest cases, I thought I'd post. I have the intuition that this
has something to do with the nested instantiation of polymorphic types.
The unions would "obviously" (to a human) collapse, but I suppose the
type checker isn't picking up on this.

-- 
Anthony Carrico

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <http://lists.racket-lang.org/users/archive/attachments/20140905/95d33a87/attachment.sig>