@@ -292,7 +292,7 @@ infer' (Abs (Left arg) ret) = do
292292infer' (Abs (Right _) _) = internalError "Binder was not desugared"
293293infer' (App f arg) = do
294294 f'@(TypedValue _ _ ft) <- infer f
295− (ret, app) <- checkFunctionApplication f' ft arg Nothing
295+ (ret, app) <- checkFunctionApplication f' ft arg
296296 return $ TypedValue True app ret
297297infer' (Var var) = do
298298 checkVisibility var
@@ -567,8 +567,11 @@ check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) = do
567567check' (Abs (Right _) _) _ = internalError "Binder was not desugared"
568568check' (App f arg) ret = do
569569 f'@(TypedValue _ _ ft) <- infer f
570− (_, app) <- checkFunctionApplication f' ft arg (Just ret)
571− return $ TypedValue True app ret
570+ (retTy, app) <- checkFunctionApplication f' ft arg
571+ v' <- subsumes (Just app) retTy ret
572+ case v' of
573+ Nothing -> internalError "check: unable to check the subsumes relation."
574+ Just app' -> return $ TypedValue True app' ret
572575check' v@(Var var) ty = do
573576 checkVisibility var
574577 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable $ var
@@ -692,55 +695,64 @@ checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' wh
692695 return $ (p, v') : ps''
693696 go _ _ _ = throwError . errorMessage $ ExprDoesNotHaveType expr (TypeApp tyRecord row)
694697
695−-- | Check the type of a function application, rethrowing errors to provide a better error message
696−checkFunctionApplication ::
697− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
698− Expr ->
699− Type ->
700− Expr ->
701− Maybe Type ->
702− m (Type, Expr)
703−checkFunctionApplication fn fnTy arg ret = withErrorMessageHint (ErrorInApplication fn fnTy arg) $ do
698+-- | Check the type of a function application, rethrowing errors to provide a better error message.
699+--
700+-- This judgment takes three inputs:
701+--
702+-- * The expression of the function we are applying
703+-- * The type of that function
704+-- * The expression we are applying it to
705+--
706+-- and synthesizes two outputs:
707+--
708+-- * The return type
709+-- * The elaborated expression for the function application (since we might need to
710+-- insert type class dictionaries, etc.)
711+checkFunctionApplication
712+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
713+ => Expr
714+ -- ^ The function expression
715+ -> Type
716+ -- ^ The type of the function
717+ -> Expr
718+ -- ^ The argument expression
719+ -> m (Type, Expr)
720+ -- ^ The result type, and the elaborated term
721+checkFunctionApplication fn fnTy arg = withErrorMessageHint (ErrorInApplication fn fnTy arg) $ do
704722 subst <- gets checkSubstitution
705− checkFunctionApplication' fn (substituteType subst fnTy) arg (substituteType subst <$> ret)
723+ checkFunctionApplication' fn (substituteType subst fnTy) arg
706724
707725-- | Check the type of a function application
708−checkFunctionApplication' ::
709− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
710− Expr ->
711− Type ->
712− Expr ->
713− Maybe Type ->
714− m (Type, Expr)
715−checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
726+checkFunctionApplication'
727+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
728+ => Expr
729+ -> Type
730+ -> Expr
731+ -> m (Type, Expr)
732+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg = do
716733 unifyTypes tyFunction' tyFunction
717734 arg' <- check arg argTy
718− case ret of
719− Nothing -> return (retTy, App fn arg')
720− Just ret' -> do
721− Just app' <- subsumes (Just (App fn arg')) retTy ret'
722− return (retTy, app')
723−checkFunctionApplication' fn (ForAll ident ty _) arg ret = do
735+ return (retTy, App fn arg')
736+checkFunctionApplication' fn (ForAll ident ty _) arg = do
724737 replaced <- replaceVarWithUnknown ident ty
725− checkFunctionApplication fn replaced arg ret
726−checkFunctionApplication' fn u@(TUnknown _) arg ret = do
738+ checkFunctionApplication fn replaced arg
739+checkFunctionApplication' fn (KindedType ty _) arg =
740+ checkFunctionApplication fn ty arg
741+checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg = do
742+ dicts <- getTypeClassDictionaries
743+ hints <- gets checkHints
744+ checkFunctionApplication' (foldl App fn (map (\cs -> TypeClassDictionary cs dicts hints) constraints)) fnTy arg
745+checkFunctionApplication' fn fnTy dict@TypeClassDictionary{} =
746+ return (fnTy, App fn dict)
747+checkFunctionApplication' fn u arg = do
727748 arg' <- do
728749 TypedValue _ arg' t <- infer arg
729750 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
730751 return $ TypedValue True arg'' t'
731752 let ty = (\(TypedValue _ _ t) -> t) arg'
732− ret' <- maybe freshType return ret
733− unifyTypes u (function ty ret')
734− return (ret', App fn arg')
735−checkFunctionApplication' fn (KindedType ty _) arg ret =
736− checkFunctionApplication fn ty arg ret
737−checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
738− dicts <- getTypeClassDictionaries
739− hints <- gets checkHints
740− checkFunctionApplication' (foldl App fn (map (\cs -> TypeClassDictionary cs dicts hints) constraints)) fnTy arg ret
741−checkFunctionApplication' fn fnTy dict@TypeClassDictionary{} _ =
742− return (fnTy, App fn dict)
743−checkFunctionApplication' _ fnTy arg _ = throwError . errorMessage $ CannotApplyFunction fnTy arg
753+ ret <- freshType
754+ unifyTypes u (function ty ret)
755+ return (ret, App fn arg')
744756
745757-- |
746758-- Ensure a set of property names and value does not contain duplicate labels