Fixed inference with typed functions

diff --git a/examples/higher.spl b/examples/higher.spl
index 0cd83de..1237743 100644 (file)
--- a/examples/higher.spl
+++ b/examples/higher.spl
@@ -37,12 +37,12 @@ intList(x){
 }
 
 printIntList(l) :: [Int] -> Void{
-       print('[');
+    print('[');
        if(!isEmpty(l)){
                print(l.hd);
                l = l.tl;
        }
-       while(isEmpty(l)){
+       while(!isEmpty(l)){
                print(", ", l.hd);
                l = l.tl;
        }
@@ -54,4 +54,5 @@ main(){
        print("sum of 1..5 is: ", foldr(\x y->x+y, 0, intList(5)));
        print("filter evens from 0..12 is: ");
        printIntList(filter(\x->x%2 == 0, intList(12)));
+    printIntList(1:2:3:[]);
 }

diff --git a/sem.icl b/sem.icl
index 2f9e7d6..b000eac 100644 (file)
--- a/sem.icl
+++ b/sem.icl
@@ -427,22 +427,28 @@ instance type VarDecl where
 
 instance type FunDecl where
     type fd=:(FunDecl p f args expected vds stmts) = 
-        //if (f=="main") (abort (toString fd)) (pure ()) >>|
         gamma >>= \outerScope-> //functions are infered in their own scopde
         introduce f >>|
         mapM introduce args >>= \argTs->
+        fresh >>= \tempTv ->
+        let temp = foldr (->>) tempTv argTs in 
+        (case expected of
+            Just expected_ = lift (unify expected_ temp)
+            _   = pure zero
+        ) >>= \s0->
+        applySubst s0 >>|
         type vds >>= \(s1, tVds)->
         applySubst s1 >>|
         infer stmts >>= \(s2, result, stmts_)->
         applySubst s1 >>|
-        let argTs_ = map (subst $ compose s2 s1) argTs in 
+        let argTs_ = map (subst $ compose s2 $ compose s1 s0) argTs in 
         let given = foldr (->>) result argTs_ in 
         (case expected of
             Nothing = pure zero
             Just (FuncType expected_) = lift (unify expected_ given)
             Just expected_ = lift (unify expected_ given)
         ) >>= \s3 ->
-        let ftype = subst (compose s3 $ compose s2 s1) given in
+        let ftype = subst (compose s3 $ compose s2 $ compose s1 s0) given in
         (case ftype of
             _ ->> _ = pure ftype
             _       = pure $ FuncType ftype
@@ -450,7 +456,8 @@ instance type FunDecl where
         generalize ftype_ >>= \t->
         putGamma outerScope >>|
         changeGamma (extend f t) >>| 
-        pure (compose s3 $ compose s2 s1, FunDecl p f args (Just ftype_) tVds stmts_)
+        pure (compose s3 $ compose s2 $ compose s1 s0, 
+                FunDecl p f args (Just ftype_) tVds stmts_)
 
 instance type [a] | type a where
     type []     = pure (zero, [])