@@ -157,7 +157,7 @@ typeOf name val = do
157157 Just ident | isFunction val ->
158158 do me <- fresh
159159 ty <- infer (M.singleton ident me) val
160− me ~~ ty
160+ ty `subsumes` me
161161 return ty
162162 _ -> infer M.empty val
163163 escapeCheck checks ty sub
@@ -230,6 +230,10 @@ replaceRowVars m = everywhere (mkT replace)
230230 _ -> RowVar v
231231 replace t = t
232232
233+replaceAllVarsWithUnknowns :: Type -> Subst Check Type
234+replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarsWithUnknowns [ident] ty >>= replaceAllVarsWithUnknowns
235+replaceAllVarsWithUnknowns ty = return ty
236+
233237replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type
234238replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
235239 where
@@ -318,10 +322,11 @@ infer' m (Abs args ret) = do
318322 let m' = m `M.union` M.fromList (zip args ts)
319323 body <- infer m' ret
320324 return $ Function ts body
321−infer' m (App f xs) = do
322− t1 <- infer m f
325+infer' m app@(App _ _) = do
326+ let (f, argss) = unfoldApplication app
327+ ft <- infer m f
323328 ret <- fresh
324− checkFunctionApplication m t1 xs ret
329+ checkFunctionApplications m ft argss ret
325330 return ret
326331infer' m (Var var@(Qualified mp name)) = do
327332 case mp of
@@ -601,7 +606,9 @@ check' m val (SaturatedTypeSynonym name args) = do
601606 Nothing -> error "Type synonym was not defined"
602607check' m val u@(TUnknown _) = do
603608 ty <- infer m val
604− ty ~~ u
609+ -- Don't unify an unknown with an inferred polytype
610+ ty' <- replaceAllVarsWithUnknowns ty
611+ ty' ~~ u
605612check' m (NumericLiteral _) Number = return ()
606613check' m (StringLiteral _) String = return ()
607614check' m (BooleanLiteral _) Boolean = return ()
@@ -613,9 +620,10 @@ check' m (Abs args ret) (Function argTys retTy) = do
613620 guardWith "Incorrect number of function arguments" (length args == length argTys)
614621 let bindings = M.fromList (zip args argTys)
615622 check (bindings `M.union` m) ret retTy
616−check' m (App f xs) ret = do
623+check' m app@(App _ _) ret = do
624+ let (f, argss) = unfoldApplication app
617625 ft <- infer m f
618− checkFunctionApplication m ft xs ret
626+ checkFunctionApplications m ft argss ret
619627check' m v@(Var var@(Qualified mp name)) ty = do
620628 case mp of
621629 ModulePath [] ->
@@ -694,6 +702,20 @@ checkProperties m ps row lax = let (ts, r') = rowToList row in go ps ts r' where
694702 go ps (delete (p, ty) ts) r
695703 go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (Object row)
696704
705+unfoldApplication :: Value -> (Value, [[Value]])
706+unfoldApplication = go []
707+ where
708+ go argss (App f args) = go (args:argss) f
709+ go argss f = (f, argss)
710+
711+checkFunctionApplications :: M.Map Ident Type -> Type -> [[Value]] -> Type -> Subst Check ()
712+checkFunctionApplications _ _ [] _ = error "Nullary function application"
713+checkFunctionApplications m fnTy [args] ret = checkFunctionApplication m fnTy args ret
714+checkFunctionApplications m fnTy (args:argss) ret = do
715+ f <- fresh
716+ checkFunctionApplication m fnTy args f
717+ checkFunctionApplications m f argss ret
718+
697719checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
698720checkFunctionApplication m fnTy args ret = rethrow errorMessage $ checkFunctionApplication' m fnTy args ret
699721 where
@@ -712,8 +734,8 @@ checkFunctionApplication' m (ForAll ident ty) args ret = do
712734 replaced <- replaceVarsWithUnknowns [ident] ty
713735 checkFunctionApplication m replaced args ret
714736checkFunctionApplication' m u@(TUnknown _) args ret = do
715− tyArgs <- mapM (infer m) args
716− u `subsumes` Function tyArgs ret
737+ tyArgs <- mapM (\arg -> infer m arg >>= replaceAllVarsWithUnknowns) args
738+ u ~~ Function tyArgs ret
717739checkFunctionApplication' _ fnTy args ret = throwError $ "Cannot apply function of type "
718740 ++ prettyPrintType fnTy
719741 ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)