Summary

Renaming issue with "the"

Metadata

Description

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)))

Changes and comments

[2019-01-20 14:48:44 UTC] sjamaan changed status from new to closed

[2019-01-20 14:48:44 UTC] sjamaan set resolution to fixed

[2019-01-20 14:48:44 UTC] sjamaan wrote:

Fixed by 339ca57996c94295d828398eb6217c1168ca10dd