@@ -519,7 +519,7 @@ infer' (Abs (Left arg) ret) = do
519519infer' (Abs (Right _) _) = error "Binder was not desugared"
520520infer' (App f arg) = do
521521 f'@(TypedValue _ _ ft) <- infer f
522− (ret, app) <- checkFunctionApplication f' ft arg
522+ (ret, app) <- checkFunctionApplication f' ft arg Nothing
523523 return $ TypedValue True app ret
524524infer' (Var var) = do
525525 Just moduleName <- checkCurrentModule <$> get
@@ -726,8 +726,7 @@ check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) | t == tyFuncti
726726check' (Abs (Right _) _) _ = error "Binder was not desugared"
727727check' (App f arg) ret = do
728728 f'@(TypedValue _ _ ft) <- infer f
729− (ret', app) <- checkFunctionApplication f' ft arg
730− _ <- subsumes Nothing ret' ret
729+ (_, app) <- checkFunctionApplication f' ft arg (Just ret)
731730 return $ TypedValue True app ret
732731check' v@(Var var) ty = do
733732 Just moduleName <- checkCurrentModule <$> get
@@ -822,8 +821,8 @@ checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
822821-- |
823822-- Check the type of a function application, rethrowing errors to provide a better error message
824823--
825−checkFunctionApplication :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)
826−checkFunctionApplication fn fnTy arg = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg
824+checkFunctionApplication :: Value -> Type -> Value -> Maybe Type -> UnifyT Type Check (Type, Value)
825+checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg ret
827826 where
828827 errorMessage msg = "Error applying function of type "
829828 ++ prettyPrintType fnTy
@@ -833,30 +832,32 @@ checkFunctionApplication fn fnTy arg = rethrow errorMessage $ checkFunctionAppli
833832-- |
834833-- Check the type of a function application
835834--
836−checkFunctionApplication' :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)
837−checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg = do
835+checkFunctionApplication' :: Value -> Type -> Value -> Maybe Type -> UnifyT Type Check (Type, Value)
836+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
838837 tyFunction' =?= tyFunction
839− arg' <- check arg argTy
838+ _ <- maybe (return Nothing) (subsumes Nothing retTy) ret
839+ subst <- unifyCurrentSubstitution <$> UnifyT get
840+ arg' <- check arg (subst $? argTy)
840841 return (retTy, App fn arg')
841−checkFunctionApplication' fn (ForAll ident ty _) arg = do
842+checkFunctionApplication' fn (ForAll ident ty _) arg ret = do
842843 replaced <- replaceVarWithUnknown ident ty
843− checkFunctionApplication fn replaced arg
844−checkFunctionApplication' fn u@(TUnknown _) arg = do
844+ checkFunctionApplication fn replaced arg ret
845+checkFunctionApplication' fn u@(TUnknown _) arg ret = do
845846 arg' <- do
846847 TypedValue _ arg' t <- infer arg
847848 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
848849 return $ TypedValue True arg'' t'
849850 let ty = (\(TypedValue _ _ t) -> t) arg'
850− ret <- fresh
851− u =?= function ty ret
852− return (ret, App fn arg')
853−checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg = do
851+ ret' <- maybe fresh return ret
852+ u =?= function ty ret'
853+ return (ret', App fn arg')
854+checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do
854855 ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
855− checkFunctionApplication fn ty arg
856−checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg = do
856+ checkFunctionApplication fn ty arg ret
857+checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
857858 dicts <- getTypeClassDictionaries
858− checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) constraints)) fnTy arg
859−checkFunctionApplication' _ fnTy arg = throwError $ "Cannot apply a function of type "
859+ checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) constraints)) fnTy arg ret
860+checkFunctionApplication' _ fnTy arg _ = throwError $ "Cannot apply a function of type "
860861 ++ prettyPrintType fnTy
861862 ++ " to argument " ++ prettyPrintValue arg
862863