changeGamma (extend k (Forall [] (subst s varType))) >>| 
         pure (s, VoidType)
 
-    FunStmt f es _ = pure (zero, VoidType) 
+    FunStmt f es _ = pure (zero, VoidType) //Fix for print & check number of args
+    FunStmt f args fs = 
+        lookup f >>= \expected ->
+        let accST = (\(s,ts) e->infer e >>= \(s_,et)->pure (compose s_ s,ts++[et])) in
+        foldM accST (zero,[]) args >>= \(s1, argTs)->
+        fresh >>= \tv->
+        let given = foldr (->>) tv argTs in
+        lift (unify expected given) >>= \s2->
+        let fReturnType = subst s2 tv in
+        foldM foldFieldSelectors fReturnType fs >>= \_ ->
+        pure (compose s2 s1, VoidType)
 
     ReturnStmt Nothing = pure (zero, VoidType)
     ReturnStmt (Just e) = infer e
         infer stmts >>= \(s2, result)->
         applySubst s1 >>|
         let argTs_ = map (subst $ compose s2 s1) argTs in 
-        //abort (concat $ intersperse "\n" $ map toString argTs_) >>|
         let given = foldr (->>) result argTs_ in 
         (case expected of
             Nothing = pure zero