Exchanging recursive types for a bug
After all it seems that it wasn't the type's lack of expressiveness that explained the wrong typing described yesterday. Actually, the expression 'defrec ^f = fun ^x -> case x of <#a=^a> in f(a) or <#b=^b> in b' should not be accepted by the type checker: it was really a bug, as Prof. Wadler pointed it out. Of course, this means one can't use recursive functions to create or parse data structures such as trees anymore, and that the solution drafted Tuesday for the expression problem wouldn't work: recursive types would be needed for that.
But for now, it is enough to have the simple non-recursive types. So I fixed this new bug (it was a problem with the type inference rule I was using for letrec in algorithm W, the expression above now raises a type error), and started working on a way to make SLinks execute SQL queries.