Fixed inference with typed functions

[cc1516.git] / sem.icl

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, [])