@@ -23,8 +23,8 @@ import Data.Maybe (isJust, fromMaybe)
2323import Data.Function
2424import qualified Data.Data as D
2525import Data.Generics
26− (something, everywhere, everywhereM, everything, everywhereBut,
27− mkT, mkM, mkQ, extM, extQ)
26+ (extT, something, everywhere, everywhereM, everything,
27+ everywhereBut, mkT, mkM, mkQ, extM, extQ)
2828
2929import Language.PureScript.Values
3030import Language.PureScript.Types
@@ -196,7 +196,17 @@ setifyAll :: (D.Data d) => d -> d
196196setifyAll = everywhere (mkT setify)
197197
198198varIfUnknown :: Type -> Type
199−varIfUnknown ty = mkForAll (sort . map ((:) 'u' . show) . nub $ unknowns ty) ty
199+varIfUnknown ty =
200+ let unks = nub $ unknowns ty
201+ toName = (:) 't' . show
202+ ty' = everywhere (mkT rowToVar) . everywhere (mkT typeToVar) $ ty
203+ typeToVar :: Type -> Type
204+ typeToVar (TUnknown (Unknown u)) = TypeVar (toName u)
205+ typeToVar t = t
206+ rowToVar :: Row -> Row
207+ rowToVar (RUnknown (Unknown u)) = RowVar (toName u)
208+ rowToVar t = t
209+ in mkForAll (sort . map toName $ unks) ty'
200210
201211replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
202212replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
@@ -705,8 +715,8 @@ checkFunctionApplications :: M.Map Ident Type -> Type -> [[Value]] -> Type -> Su
705715checkFunctionApplications _ _ [] _ = error "Nullary function application"
706716checkFunctionApplications m fnTy [args] ret = checkFunctionApplication m fnTy args ret
707717checkFunctionApplications m fnTy (args:argss) ret = do
708− f <- fresh
709− checkFunctionApplication m fnTy args f
718+ argTys <- mapM (infer m) args
719+ f <- inferFunctionApplication m fnTy argTys
710720 checkFunctionApplications m f argss ret
711721
712722checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
@@ -718,6 +728,26 @@ checkFunctionApplication m fnTy args ret = rethrow errorMessage $ checkFunctionA
718728 ++ ", expecting value of type "
719729 ++ prettyPrintType ret ++ ":\n" ++ msg
720730
731+inferFunctionApplication :: M.Map Ident Type -> Type -> [Type] -> Subst Check Type
732+inferFunctionApplication m (Function argTys retTy) args = do
733+ guardWith "Incorrect number of function arguments" (length args == length argTys)
734+ zipWithM subsumes args argTys
735+ return retTy
736+inferFunctionApplication m (ForAll ident ty) args = do
737+ replaced <- replaceVarWithUnknown ident ty
738+ inferFunctionApplication m replaced args
739+inferFunctionApplication m u@(TUnknown _) args = do
740+ ret <- fresh
741+ args' <- mapM replaceAllVarsWithUnknowns args
742+ u ~~ Function args' ret
743+ return ret
744+inferFunctionApplication m (SaturatedTypeSynonym name tyArgs) args = do
745+ ty <- expandTypeSynonym name tyArgs
746+ inferFunctionApplication m ty args
747+inferFunctionApplication _ fnTy args = throwError $ "Cannot apply function of type "
748+ ++ prettyPrintType fnTy
749+ ++ " to argument(s) of type(s) " ++ intercalate ", " (map prettyPrintType args)
750+
721751checkFunctionApplication' :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
722752checkFunctionApplication' m (Function argTys retTy) args ret = do
723753 guardWith "Incorrect number of function arguments" (length args == length argTys)
@@ -732,10 +762,10 @@ checkFunctionApplication' m u@(TUnknown _) args ret = do
732762checkFunctionApplication' m (SaturatedTypeSynonym name tyArgs) args ret = do
733763 ty <- expandTypeSynonym name tyArgs
734764 checkFunctionApplication' m ty args ret
735−checkFunctionApplication' _ fnTy args ret = throwError $ "Cannot apply function of type "
765+checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of type "
736766 ++ prettyPrintType fnTy
737− ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
738− ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."
767+ ++ " to argument(s) " ++ intercalate ", " (map prettyPrintValue args)
768+ ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."
739769
740770subsumes :: Type -> Type -> Subst Check ()
741771subsumes (ForAll ident ty1) ty2 = do