[Chicken-janitors] #1563: Renaming issue with "the"

[Chicken Trac]

#1563: Renaming issue with "the"
-------------------------------------+-------------------------------------
 Reporter:  megane                   |                 Owner:
     Type:  defect                   |                Status:  new
 Priority:  major                    |             Milestone:  5.1
Component:  expander                 |               Version:  5.0.0
 Keywords:  er-macro-transformer     |  Estimated difficulty:
  scrutinizer                        |
-------------------------------------+-------------------------------------
 The first argument to `##core#the` should be the validated type as
 returned by `check-and-validate-type`. In the validated type all type
 variables have been replaced with gensymed new names.

 Here's the code for the `the` macro in its entirety:
 {{{
 (##sys#extend-macro-environment
  'the '()
  (##sys#er-transformer
   (lambda (x r c)
     (##sys#check-syntax 'the x '(_ _ _))
     (if (not (memq #:compiling ##sys#features))
         (caddr x)
         `(##core#the ,(chicken.compiler.scrutinizer#check-and-validate-
 type (cadr x) 'the)
                      #t
                      ,(caddr x))))))
 }}}

 Add a debug print to `check-and-validate-type` to confirm typevariables
 are being renamed:
 {{{
 (define (check-and-validate-type type loc #!optional name)
   (let-values (((t pred pure) (validate-type (strip-syntax type) name)))
    (when t (dd "type validated ~a => ~a" type t)) ; <- new line
     (or t
         (error loc "invalid type specifier" type))))
 }}}

 Now try this example:

 {{{
 (import (chicken type))
 (compiler-typecase (the (forall (a) (pair symbol a)) (pair 'sym 1))
   ((forall (a) (pair a fixnum)) 1))
 }}}

 This should compile without errors. One `a` should unify with `symbol`
 and the other with `fixnum`.

 Instead of that you get the error:

 {{{
 Error: at toplevel:
   (que.scm:20) no clause applies in `compiler-typecase' for expression of
 type `(forall (a) (pair symbol a))':
     (forall (a) (pair a fixnum))
 }}}

 If you check the debug output for scrutinizer you can see that both
 `a`'s have actually the same name! (You can try renaming one pair of
 `a`s to see it indeed compiles without errors.)

 You can see `check-and-validate-type` correctly renamed the variables:
 {{{
 [debug|0] type validated (forall (a) (pair a fixnum)) => (forall (a18)
 (pair a18 fixnum))
 [debug|0] type validated (forall (a) (pair symbol a)) => (forall (a20)
 (pair symbol a20))
 }}}

 But if you check the canonicalized form you see:
 {{{
 $ csc -debug 2 -O3 que.scm
 [canonicalized]
 (##core#callunit library)

 (##core#callunit eval)

 (##core#callunit expand)

 (##core#undefined)

 (##core#undefined)

 (##core#undefined)

 (##core#undefined)

 (##core#undefined)

 (let ((g1719 (##core#the (forall (a) (pair symbol a)) #t (pair 'sym '1))))
 <--- no renaming here!
   (##core#typecase "que.scm:20" g1719 ((forall (a) (pair a fixnum)) '1)))
 }}}

--
Ticket URL: <https://bugs.call-cc.org/ticket/1563>
CHICKEN Scheme <https://www.call-cc.org/>
CHICKEN Scheme is a compiler for the Scheme programming language.