@@ -292,7 +292,7 @@ infer' (Abs (Left arg) ret) = do
292infer' (Abs (Right _) _) = internalError "Binder was not desugared"
292infer' (Abs (Right _) _) = internalError "Binder was not desugared"
293infer' (App f arg) = do
293infer' (App f arg) = do
294 f'@(TypedValue _ _ ft) <- infer f
294 f'@(TypedValue _ _ ft) <- infer f
295− (ret, app) <- checkFunctionApplication f' ft arg Nothing
295+ (ret, app) <- checkFunctionApplication f' ft arg
296 return $ TypedValue True app ret
296 return $ TypedValue True app ret
297infer' (Var var) = do
297infer' (Var var) = do
298 checkVisibility var
298 checkVisibility var
@@ -567,8 +567,11 @@ check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) = do
567check' (Abs (Right _) _) _ = internalError "Binder was not desugared"
567check' (Abs (Right _) _) _ = internalError "Binder was not desugared"
568check' (App f arg) ret = do
568check' (App f arg) ret = do
569 f'@(TypedValue _ _ ft) <- infer f
569 f'@(TypedValue _ _ ft) <- infer f
570− (_, app) <- checkFunctionApplication f' ft arg (Just ret)
570+ (retTy, app) <- checkFunctionApplication f' ft arg
571+ v' <- subsumes (Just app) retTy ret
573+ Nothing -> internalError "check: unable to check the subsumes relation."
571− return $ TypedValue True app ret
574+ Just app' -> return $ TypedValue True app' ret
572check' v@(Var var) ty = do
575check' v@(Var var) ty = do
573 checkVisibility var
576 checkVisibility var
574 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable $ var
577 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
692 return $ (p, v') : ps''
695 return $ (p, v') : ps''
693 go _ _ _ = throwError . errorMessage $ ExprDoesNotHaveType expr (TypeApp tyRecord row)
696 go _ _ _ = throwError . errorMessage $ ExprDoesNotHaveType expr (TypeApp tyRecord row)
695−-- | Check the type of a function application, rethrowing errors to provide a better error message
698+-- | Check the type of a function application, rethrowing errors to provide a better error message.
696−checkFunctionApplication ::
699+--
700+-- This judgment takes three inputs:
702+-- * The expression of the function we are applying
703+-- * The type of that function
704+-- * The expression we are applying it to
706+-- and synthesizes two outputs:
709+-- * The elaborated expression for the function application (since we might need to
710+-- insert type class dictionaries, etc.)
711+checkFunctionApplication
697− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
712+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
699− Type ->
714+ -- ^ The function expression
716+ -- ^ The type of the function
701− Maybe Type ->
718+ -- ^ The argument expression
702− m (Type, Expr)
719+ -> m (Type, Expr)
720+ -- ^ The result type, and the elaborated term
703−checkFunctionApplication fn fnTy arg ret = withErrorMessageHint (ErrorInApplication fn fnTy arg) $ do
721+checkFunctionApplication fn fnTy arg = withErrorMessageHint (ErrorInApplication fn fnTy arg) $ do
704 subst <- gets checkSubstitution
722 subst <- gets checkSubstitution
705− checkFunctionApplication' fn (substituteType subst fnTy) arg (substituteType subst <$> ret)
723+ checkFunctionApplication' fn (substituteType subst fnTy) arg
707-- | Check the type of a function application
725-- | Check the type of a function application
708−checkFunctionApplication' ::
726+checkFunctionApplication'
709− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
727+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
714− m (Type, Expr)
731+ -> m (Type, Expr)
715−checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
732+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg = do
716 unifyTypes tyFunction' tyFunction
733 unifyTypes tyFunction' tyFunction
717 arg' <- check arg argTy
734 arg' <- check arg argTy
719− Nothing -> return (retTy, App fn arg')
735+ return (retTy, App fn arg')
721− Just app' <- subsumes (Just (App fn arg')) retTy ret'
722− return (retTy, app')
723−checkFunctionApplication' fn (ForAll ident ty _) arg ret = do
736+checkFunctionApplication' fn (ForAll ident ty _) arg = do
724 replaced <- replaceVarWithUnknown ident ty
737 replaced <- replaceVarWithUnknown ident ty
725− checkFunctionApplication fn replaced arg ret
738+ checkFunctionApplication fn replaced arg
726−checkFunctionApplication' fn u@(TUnknown _) arg ret = do
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
727 arg' <- do
748 arg' <- do
728 TypedValue _ arg' t <- infer arg
749 TypedValue _ arg' t <- infer arg
729 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
750 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
730 return $ TypedValue True arg'' t'
751 return $ TypedValue True arg'' t'
731 let ty = (\(TypedValue _ _ t) -> t) arg'
752 let ty = (\(TypedValue _ _ t) -> t) arg'
732− ret' <- maybe freshType return ret
753+ ret <- freshType
733− unifyTypes u (function ty ret')
754+ unifyTypes u (function ty ret)
734− return (ret', App fn arg')
755+ 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
746-- Ensure a set of property names and value does not contain duplicate labels
758-- Ensure a set of property names and value does not contain duplicate labels