From: pimjager <pim@pimjager.nl>
Date: Thu, 26 May 2016 17:46:17 +0000 (+0200)
Subject: Fixed inference with typed functions
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=390ba8971ff6f912c9e5cb01b3a663738de11704;p=cc1516.git

Fixed inference with typed functions
---

diff --git a/examples/higher.spl b/examples/higher.spl
index 0cd83de..1237743 100644
--- 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
--- 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, [])