@@ -519,7 +519,7 @@ infer' (Abs (Left arg) ret) = do
519infer' (Abs (Right _) _) = error "Binder was not desugared"
519infer' (Abs (Right _) _) = error "Binder was not desugared"
520infer' (App f arg) = do
520infer' (App f arg) = do
521 f'@(TypedValue _ _ ft) <- infer f
521 f'@(TypedValue _ _ ft) <- infer f
522− (ret, app) <- checkFunctionApplication f' ft arg
522+ (ret, app) <- checkFunctionApplication f' ft arg Nothing
523 return $ TypedValue True app ret
523 return $ TypedValue True app ret
524infer' (Var var) = do
524infer' (Var var) = do
525 Just moduleName <- checkCurrentModule <$> get
525 Just moduleName <- checkCurrentModule <$> get
@@ -726,8 +726,7 @@ check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) | t == tyFuncti
726check' (Abs (Right _) _) _ = error "Binder was not desugared"
726check' (Abs (Right _) _) _ = error "Binder was not desugared"
727check' (App f arg) ret = do
727check' (App f arg) ret = do
728 f'@(TypedValue _ _ ft) <- infer f
728 f'@(TypedValue _ _ ft) <- infer f
729− (ret', app) <- checkFunctionApplication f' ft arg
729+ (_, app) <- checkFunctionApplication f' ft arg (Just ret)
730− _ <- subsumes Nothing ret' ret
731 return $ TypedValue True app ret
730 return $ TypedValue True app ret
732check' v@(Var var) ty = do
731check' v@(Var var) ty = do
733 Just moduleName <- checkCurrentModule <$> get
732 Just moduleName <- checkCurrentModule <$> get
@@ -822,8 +821,8 @@ checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
823-- Check the type of a function application, rethrowing errors to provide a better error message
822-- Check the type of a function application, rethrowing errors to provide a better error message
825−checkFunctionApplication :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)
824+checkFunctionApplication :: Value -> Type -> Value -> Maybe Type -> UnifyT Type Check (Type, Value)
826−checkFunctionApplication fn fnTy arg = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg
825+checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg ret
828 errorMessage msg = "Error applying function of type "
827 errorMessage msg = "Error applying function of type "
829 ++ prettyPrintType fnTy
828 ++ prettyPrintType fnTy
@@ -833,30 +832,32 @@ checkFunctionApplication fn fnTy arg = rethrow errorMessage $ checkFunctionAppli
834-- Check the type of a function application
833-- Check the type of a function application
836−checkFunctionApplication' :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)
835+checkFunctionApplication' :: Value -> Type -> Value -> Maybe Type -> UnifyT Type Check (Type, Value)
837−checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg = do
836+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
838 tyFunction' =?= tyFunction
837 tyFunction' =?= tyFunction
838+ _ <- maybe (return Nothing) (subsumes Nothing retTy) ret
839+ subst <- unifyCurrentSubstitution <$> UnifyT get
839− arg' <- check arg argTy
840+ arg' <- check arg (subst $? argTy)
840 return (retTy, App fn arg')
841 return (retTy, App fn arg')
841−checkFunctionApplication' fn (ForAll ident ty _) arg = do
842+checkFunctionApplication' fn (ForAll ident ty _) arg ret = do
842 replaced <- replaceVarWithUnknown ident ty
843 replaced <- replaceVarWithUnknown ident ty
843− checkFunctionApplication fn replaced arg
844+ checkFunctionApplication fn replaced arg ret
844−checkFunctionApplication' fn u@(TUnknown _) arg = do
845+checkFunctionApplication' fn u@(TUnknown _) arg ret = do
845 arg' <- do
846 arg' <- do
846 TypedValue _ arg' t <- infer arg
847 TypedValue _ arg' t <- infer arg
847 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
848 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
848 return $ TypedValue True arg'' t'
849 return $ TypedValue True arg'' t'
849 let ty = (\(TypedValue _ _ t) -> t) arg'
850 let ty = (\(TypedValue _ _ t) -> t) arg'
850− ret <- fresh
851+ ret' <- maybe fresh return ret
851− u =?= function ty ret
852+ u =?= function ty ret'
852− return (ret, App fn arg')
853+ return (ret', App fn arg')
853−checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg = do
854+checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do
854 ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
855 ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
855− checkFunctionApplication fn ty arg
856+ checkFunctionApplication fn ty arg ret
856−checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg = do
857+checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
857 dicts <- getTypeClassDictionaries
858 dicts <- getTypeClassDictionaries
858− checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) constraints)) fnTy arg
859+ checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) constraints)) fnTy arg ret
859−checkFunctionApplication' _ fnTy arg = throwError $ "Cannot apply a function of type "
860+checkFunctionApplication' _ fnTy arg _ = throwError $ "Cannot apply a function of type "
860 ++ prettyPrintType fnTy
861 ++ prettyPrintType fnTy
861 ++ " to argument " ++ prettyPrintValue arg
862 ++ " to argument " ++ prettyPrintValue arg