[clean-list] appeal for explanation to Curry-type assignment algorithm

[Jigang Sun]

I have problems of understanding Curry-type assignment algorithm page 196 chapter 6 Type Assignment System Functional of Rinus book Programming and Parallel Graph Rewriting. 

It is obviously "rest" in function check_assumptn mean other elements of  the basis. So if basis=[(y,τ)], should rest=[]?

Should freshtypevars be supposed as an infinite list of type variables when apply function curry? e.g., for λx.x, it is Curry: [φ0, φ1, φ2, φ3…] λx.x 

Bellow is my work using Curry_type Assignment algorithm on λx.x. I think the result is obviously wrong: the basis in typeresults got is empty set, final type is φ1-> φ1. Should the final result be expected as ([φ1, φ2, φ3], [x,φ0], φ0-> φ0)?


Curry: [φ0, φ1, φ2, φ3…] λx.x 
= (ftvs’, basis, s φ0->τ)
=> ([φ2, φ3…], [], (sub φ0 φ1) φ0-> φ1)
=> ([φ2, φ3…], [], φ1-> φ1)


Where 
(basis,s)=check_assmptn ( x, φ0) bas
=> check_assmptn ( x, φ0) [(x, φ1)]
=>check_assmptn ( x, φ0) [ (x, φ1):[] ]
=> (substitute (s2•s1) bas1, s2•s1 ) ) //because x==x
=> (substitute (s2•(sub φ0 φ1)) bas1, s2• (sub φ0 φ1) )) 
=> (substitute (s2•(sub φ0 φ1)) [], s2• (sub φ0 φ1) ))
=> (substitute ((identisub • (sub φ0 φ1)) [] , identisub • (sub φ0 φ1) )
=> (substitute (sub φ0 φ1) [] ,identisub (sub φ0 φ1)) 
=> ([],identisub (sub φ0 φ1))
=> ([],sub φ0 φ1)

        Where s1=unify φ0 φ1
                =>sub φ0 φ1

            (bas1, s2)=check_assmptn(x, s1 φ0) [] //rest is empty 
                      =>([], identisub) 


(ftvs’,bas, τ) =curry [φ1, φ2, φ3…] x
=> ([φ2, φ3…], [(x, φ1)], φ1)
 


Many thanks.

Jigang