@@ -1,32 +1,172 @@
-@@type = fun(x){
-  if _isint(x): "int"
-  else if _isstr(x): "str" 
-  else: "any"
-};
-
-def binop(a,b,c) {
-  fun(x,y){@value(
-    if( _isbot( @type(x) ) || _isbot( @type(y) ) ) then @type(...) else
-      if( @type(x)==a && @type(y)==b ) then c else "error"
-  )}
+# Lift to types
+@@type (x)
+{
+	if _isint(x): "int"
+	else if _isstr(x): "str"
+	else if _isbot(x): "RE"
+	else if _istbl(x):
+		if x.?car && x.?cdr:
+			let xa = x.car in let xd = x.cdr in
+				mergeType( {list: @type(xa)}, @type(xd) )
+		else
+			{list: "RE"} # tenuki
+	else ...
 };
 
-@type "+" = binop("int", "int", "int");
-@type "-" = binop("int", "int", "int");
-@type "<" = binop("int", "int", "int");
-@type ">" = binop("int", "int", "int");
-
-def mergeType(a,b) {
-  if( _isbot(a) ): ( if( _isbot(b) ):"error" else b  ) else ( a )
+# unify two types
+def mergeType(a, b)
+{
+	if a == "RE": b
+	else if b == "RE": a
+	else if _istbl(a) && _istbl(b):
+		if  a.?list && b.?list:
+			let rt = mergeType(a.list, b.list) in
+				if rt=="TE" || rt=="RE" then rt else {list: rt}
+		else:
+			"TE" # type error
+	else if a == b: a
+	else "TE"  # type error
 };
 
-@type "if" = fun(c,t,e) {@value(
- if(@type(c)=="int" ): mergeType(@type(t()), @type(e())) else : "error"
-)};
-
-def fib(x)
+# helper function
+def Tuni(t1, t0)
+{
+	fun(x) {@value(
+		if @type(x)=="RE": "RE"
+		else if @type(x)=="TE": "TE"
+		else if @type(x)==t1: t0
+		else "TE"
+	)}
+};
+def Tuniany(t0)
+{
+	fun(x) {@value(
+		if @type(x)=="RE": "RE"
+		else if @type(x)=="TE": "TE"
+		else t0
+	)}
+};
+def Tbin(t1, t2, t0)
+{
+	fun(x,y) {@value(
+		if @type(x)=="RE" || @type(y)=="RE": "RE"
+		else if @type(x)=="TE" || @type(y)=="TE": "TE"
+		else if @type(x)==t1 && @type(y)==t2: t0
+		else "TE"
+	)}
+};
+def Tbinany(t0)
 {
-	if x<2 then 1 else fib(x-1) + fib(x-2)
+	fun(x,y){@value(
+		if @type(x)=="RE" || @type(y)=="RE": "RE"
+		else if @type(x)=="TE" || @type(y)=="TE": "TE"
+		else t0
+	)}
+};
+
+# type annotation for built-in ops
+@type "+" = Tbin("int", "int", "int");
+@type "-" = Tbin("int", "int", "int");
+@type "*" = Tbin("int", "int", "int");
+@type "/" = Tbin("int", "int", "int");
+@type "%" = Tbin("int", "int", "int");
+@type "&&" = Tbin("int", "int", "int");
+@type "||" = Tbin("int", "int", "int");
+@type print = fun(x){x};
+@type gensym = fun(){"str"};
+@type argv = {list: "str"};
+@type rand = Tuni("int","int");
+@type "~" = Tbinany("str");
+@type "<" = Tbinany("int");
+@type "<=" = Tbinany("int");
+@type ">" = Tbinany("int");
+@type ">=" = Tbinany("int");
+@type "==" = Tbinany("int");
+@type "!=" = Tbinany("int");
+@type "if" (c,t,e) {@value(
+	if @type(c)=="RE": "RE"
+	else if @type(c)!="int": "TE"
+	else mergeType( @type(t()), @type(e()) );
+)};
+@type _isint = Tuniany("int");
+@type _isstr = Tuniany("int");
+@type _isfun = Tuniany("int");
+@type _istbl = Tuniany("int");
+@type _isbot = Tuniany("int");
+
+###################################
+
+# for lists
+@type "{}"() {@value( {list: "RE"} )};
+@type ".?"(t, s) {@value(
+	if @type(t)=="RE": "RE"
+	else if @type(t)=="TE": "TE"
+	else if _istbl( @type(t) ): "int"
+	else "TE"
+)};
+@type ".="(t, s@value, v) {@value(
+	var tt = @type(t);
+	if tt == "TE": "TE"
+	else if tt == "RE": "RE"
+	else if _istbl(tt) && tt.?list:
+		if s == "car":
+			mergeType(tt, {list: @type(v)})
+		else if s == "cdr":
+			mergeType(tt, @type(v))
+		else:
+			tt
+	else:
+		"TE"
+)};
+@type "."(t, s@value) {@value(
+	var tt = @type(t);
+	if tt == "TE": "TE"
+	else if tt == "RE": "RE"
+	else if _istbl(tt) && tt.?list:
+		if s == "car":
+			tt.list
+		else if s == "cdr":
+			tt
+		else:
+			"TE"
+	else:
+		"TE"
+)};
+
+###################################
+
+def fib(x) { if x < 2 then 1 else fib(x-1) + fib(x-2) };
+def fibE1(x) { if "true!" then 1 else fib(x-1) + fib(x-2) };
+def fibE2(x) { if x<2 then "ichi" else fib(x-1) + fib(x-2) };
+def fibE3(x) { if x<2 then 1 else fib(x-1) ~ fib(x-2) };
+def fibS(x) { if x<2 then "1" else fib(x-1) ~ fib(x-2) };
+def fibBadButTypeIsOK(x) { if x < "2" then 1 else fib(x-1) + fib(x-2) };
+
+print( @type(fib(999)) );
+print( @type(fibE1(999)) );
+print( @type(fibE2(999)) );
+print( @type(fibE3(999)) );
+print( @type(fibS(999)) );
+print( @type(fibBadButTypeIsOK(999)) );
+
+###################################
+
+def nil = {};
+def cons(a, d) { {car: a, cdr: d} };
+
+print( @type(nil) );
+print( @type(cons(1,nil)) );
+print( @type(cons("foo",nil)) );
+print( @type(cons(123, cons("foo",nil))) ); # TE
+
+def rev(xs) {
+	def revi(xs, ys) {
+		case xs
+			when {car: x, cdr: xs}: revi(xs, cons(x,ys))
+			when {}: ys
+	};
+	revi(xs, {})
 };
 
-print( @type(fib(10)) );
+var xs = cons(1, cons(2, cons(3, nil)));
+print( @type( rev(xs) ) );