[racket] delimiting of type variables in plai-typed?

In lab yesterday I was pretty astonished when students were turning in programs something like this:

(define (its-magic [s : 'a]) : 'b
  (list s))

“Wait!” I said. "That can’t possibly typecheck!”

But then I realized that you can certainly unify ‘a -> ‘b with ‘a -> (listof ‘a).

Then I tried 

#lang plai-typed

(define its-magic : ('a -> 'b)
  (lambda (s) 34))

… but this also type-checked.

More generally, there’s no way to delimit the quantification of type variables. The grammar for types doesn’t suggest any way to do this.

Would it be easy and/or sensible to allow an explicit forall, so you could write

#lang plai-typed

(define its-magic : (forall ‘a ‘b ('a -> ‘b))
  (lambda (s) 34))

?

I see the appeal of the simplicity of the current system, but I’m seeing students writing 

(define (zip [a : (listof ‘a)] [b : (listof ‘a)]) : (listof ‘a)
  …)

… and my head explodes. It’s very clear to me that they have no idea what the type should be, so it’s a bit painful that this typechecks.

Any suggestions appreciated.

John