let f1 : 1 = 0; let f2 : U = 1; -- Since we have dependent types, types can be arbitrary expressions let f3 : f2 = f1;