558cd4e · rowtype-yoga/purescript-native

git.iko.soy/rowtype-yoga/purescript-native

More bug fixes

commit558cd4e93abc7c65318b31fbaf81d985d3463ded authorPhil Freeman <paf31@cantab.net> dateSun 24 Nov 2013, 23:12 (13 years ago) parent1883dd4

4 files changed+145−129

compare with golang

unifiedsplit

src/Language/PureScript/Pretty/Values.hs+8 src/Language/PureScript/TypeChecker/Kinds.hs+2−2 src/Language/PureScript/TypeChecker/Monad.hs+45−36 src/Language/PureScript/TypeChecker/Types.hs+90−91

src/Language/PureScript/Pretty/Values.hs+8

@@ -28,6 +28,7 @@ import Language.PureScript.Types

2828import Language.PureScript.Values

2929import Language.PureScript.Names

3030import Language.PureScript.Pretty.Common

31+import Language.PureScript.Pretty.Types

3132

3233literals :: Pattern () Value String

3334literals = mkPattern match

@@ -83,6 +84,12 @@ lam = mkPattern match

8384 match (Abs args val) = Just (map show args, val)

8485 match _ = Nothing

8586

87+typed :: Pattern () Value (PolyType, Value)

88+typed = mkPattern match

89+ where

90+ match (TypedValue val ty) = Just (ty, val)

91+ match _ = Nothing

92+

8693unary :: UnaryOperator -> String -> Operator () Value String

8794unary op str = Wrap pattern (++)

8895 where

@@ -113,6 +120,7 @@ prettyPrintValue = fromMaybe (error "Incomplete pattern") . pattern matchValue (

113120 , [ Wrap app $ \args val -> val ++ "(" ++ args ++ ")" ]

114121 , [ Split lam $ \args val -> "\\" ++ intercalate ", " args ++ " -> " ++ prettyPrintValue val ]

115122 , [ Wrap ifThenElse $ \(th, el) cond -> cond ++ " ? " ++ prettyPrintValue th ++ " : " ++ prettyPrintValue el ]

123+ , [ Wrap typed $ \ty val -> val ++ " :: " ++ prettyPrintType ty ]

116124 , [ AssocR indexer (\index val -> val ++ " !! " ++ index) ]

117125 , [ binary LessThan "<" ]

118126 , [ binary LessThanOrEqualTo "<=" ]

src/Language/PureScript/TypeChecker/Kinds.hs+2−2

@@ -62,10 +62,10 @@ instance Unifiable Kind where

6262 unknowns _ = []

6363

6464kindOf :: Type -> Check Kind

65−kindOf ty = runSubst $ starIfUnknown <$> infer Nothing M.empty ty

65+kindOf ty = fmap (\(k, _, _) -> k) . runSubst $ starIfUnknown <$> infer Nothing M.empty ty

6666

6767kindsOf :: Maybe ProperName -> [String] -> [Type] -> Check Kind

68−kindsOf name args ts = fmap starIfUnknown $ runSubst $ do

68+kindsOf name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . runSubst $ do

6969 tyCon <- fresh

7070 kargs <- replicateM (length args) fresh

7171 ks <- inferAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args kargs)) ts

src/Language/PureScript/TypeChecker/Monad.hs+45−36

@@ -13,7 +13,7 @@

1313-----------------------------------------------------------------------------

1414

1515{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances, RankNTypes, DeriveDataTypeable,

16− StandaloneDeriving, MultiParamTypeClasses, FlexibleContexts #-}

16+ GADTs, StandaloneDeriving, MultiParamTypeClasses, FlexibleContexts #-}

1717

1818module Language.PureScript.TypeChecker.Monad where

1919

@@ -49,6 +49,9 @@ data Environment = Environment

4949emptyEnvironment :: Environment

5050emptyEnvironment = Environment M.empty M.empty M.empty M.empty M.empty

5151

52+data AnyUnifiable where

53+ AnyUnifiable :: forall t. (Unifiable t) => t -> AnyUnifiable

54+

5255data CheckState = CheckState { checkEnv :: Environment

5356 , checkNextVar :: Int

5457 , checkModulePath :: ModulePath

@@ -57,21 +60,53 @@ data CheckState = CheckState { checkEnv :: Environment

5760newtype Check a = Check { unCheck :: StateT CheckState (Either String) a }

5861 deriving (Functor, Monad, Applicative, MonadPlus, MonadState CheckState, MonadError String)

5962

63+getEnv :: Check Environment

64+getEnv = fmap checkEnv get

65+

66+putEnv :: Environment -> Check ()

67+putEnv env = modify (\s -> s { checkEnv = env })

68+

69+modifyEnv :: (Environment -> Environment) -> Check ()

70+modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })

71+

72+runCheck :: Check a -> Either String (a, Environment)

73+runCheck c = do

74+ (a, s) <- flip runStateT (CheckState emptyEnvironment 0 global) $ unCheck c

75+ return (a, checkEnv s)

76+

77+guardWith :: (MonadError e m) => e -> Bool -> m ()

78+guardWith _ True = return ()

79+guardWith e False = throwError e

80+

81+rethrow :: (MonadError e m) => (e -> e) -> m a -> m a

82+rethrow f = flip catchError $ \e -> throwError (f e)

83+

84+withModule :: ProperName -> Check a -> Check a

85+withModule name act = do

86+ original <- checkModulePath `fmap` get

87+ modify $ \s -> s { checkModulePath = subModule (checkModulePath s) name }

88+ a <- act

89+ modify $ \s -> s { checkModulePath = original }

90+ return a

91+

6092newtype Substitution = Substitution { runSubstitution :: forall t. (Unifiable t) => Unknown t -> t }

6193

6294instance Monoid Substitution where

6395 mempty = Substitution unknown

6496 s1 `mappend` s2 = Substitution $ \u -> apply s1 (apply s2 (unknown u))

6597

66−newtype Subst m a = Subst { unSubst :: StateT Substitution m a }

98+data SubstState = SubstState { substSubst :: Substitution

99+ , substFutureEscapeChecks :: [AnyUnifiable] }

100+

101+newtype Subst m a = Subst { unSubst :: StateT SubstState m a }

67102 deriving (Functor, Monad, Applicative, MonadPlus, MonadTrans)

68103

69104deriving instance (MonadError String m) => MonadError String (Subst m)

70105

71−runSubst :: (Unifiable a, Monad m) => Subst m a -> m a

106+runSubst :: (Unifiable a, Monad m) => Subst m a -> m (a, Substitution, [AnyUnifiable])

72107runSubst subst = do

73− (a, s) <- flip runStateT mempty . unSubst $ subst

74− return $ apply s a

108+ (a, s) <- flip runStateT (SubstState mempty []) . unSubst $ subst

109+ return (apply (substSubst s) a, substSubst s, substFutureEscapeChecks s)

75110

76111substituteWith :: (Typeable t) => (Unknown t -> t) -> Substitution

77112substituteWith f = Substitution $ \u -> fromMaybe (unknown u) $ do

@@ -86,16 +121,16 @@ substituteOne u t = substituteWith $ \u1 ->

86121

87122replace :: (Unifiable t) => Unknown t -> t -> Subst Check ()

88123replace u t' = do

89− sub <- Subst get

124+ sub <- substSubst <$> Subst get

90125 let t = apply sub t'

91126 occursCheck u t

92127 let current = apply sub $ unknown u

93128 case isUnknown current of

94129 Just u1 | u1 == u -> return ()

95130 _ -> current ~~ t

96− Subst . modify $ \s -> substituteOne u t <> s

131+ Subst . modify $ \s -> s { substSubst = substituteOne u t <> substSubst s }

97132

98−class (Typeable t, Data t) => Unifiable t where

133+class (Typeable t, Data t, Show t) => Unifiable t where

99134 unknown :: Unknown t -> t

100135 (~~) :: t -> t -> Subst Check ()

101136 isUnknown :: t -> Maybe (Unknown t)

@@ -108,15 +143,6 @@ occursCheck (Unknown u) t =

108143 Nothing -> guardWith "Occurs check fails" (u `notElem` unknowns t)

109144 _ -> return ()

110145

111−getEnv :: Check Environment

112−getEnv = fmap checkEnv get

113−

114−putEnv :: Environment -> Check ()

115−putEnv env = modify (\s -> s { checkEnv = env })

116−

117−modifyEnv :: (Environment -> Environment) -> Check ()

118−modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })

119−

120146fresh' :: Subst Check Int

121147fresh' = do

122148 n <- lift $ checkNextVar <$> get

@@ -126,22 +152,5 @@ fresh' = do

126152fresh :: (Unifiable t) => Subst Check t

127153fresh = unknown . Unknown <$> fresh'

128154

129−runCheck :: Check a -> Either String (a, Environment)

130−runCheck c = do

131− (a, s) <- flip runStateT (CheckState emptyEnvironment 0 global) $ unCheck c

132− return (a, checkEnv s)

133−

134−guardWith :: (MonadError e m) => e -> Bool -> m ()

135−guardWith _ True = return ()

136−guardWith e False = throwError e

137−

138−rethrow :: (MonadError e m) => (e -> e) -> m a -> m a

139−rethrow f = flip catchError $ \e -> throwError (f e)

140−

141−withModule :: ProperName -> Check a -> Check a

142−withModule name act = do

143− original <- checkModulePath `fmap` get

144− modify $ \s -> s { checkModulePath = subModule (checkModulePath s) name }

145− a <- act

146− modify $ \s -> s { checkModulePath = original }

147− return a

155+escapeCheckLater :: (Unifiable t) => t -> Subst Check ()

156+escapeCheckLater t = Subst . modify $ \s -> s { substFutureEscapeChecks = AnyUnifiable t : substFutureEscapeChecks s }

src/Language/PureScript/TypeChecker/Types.hs+90−91

@@ -19,7 +19,7 @@ module Language.PureScript.TypeChecker.Types (

1919) where

2020

2121import Data.List

22−import Data.Maybe (fromMaybe)

22+import Data.Maybe (isJust, fromMaybe)

2323import Data.Function

2424import qualified Data.Data as D

2525import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)

@@ -147,48 +147,25 @@ isFunction _ = False

147147

148148typeOf :: Maybe Ident -> Value -> Check Type

149149typeOf name val = do

150− ty <- runSubst $ case name of

151− Just ident -> do me <- fresh

152− ty <- infer (M.singleton ident me) val

153− me ~~ ty

154− return ty

155− Nothing -> infer M.empty val

156− --desugared <- replaceAllTypeSynonyms cs

157− --TODO: allUnknownsBecameQuantified desugared solution ty

150+ (ty, sub, checks) <- runSubst $ case name of

151+ Just ident | isFunction val ->

152+ do me <- fresh

153+ ty <- infer (M.singleton ident me) val

154+ me ~~ ty

155+ return ty

156+ _ -> infer M.empty val

157+ escapeCheck checks ty sub

158158 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty

159159

160−{-

161−allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()

162−allUnknownsBecameQuantified cs solution ty = do

160+escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()

161+escapeCheck checks ty sub =

163162 let

164− typesMentioned = findUnknownTypes ty

165− unknownTypes = nub $ flip concatMap cs $ \c -> case c of

166− TypeConstraint u t _ -> u : findUnknownTypes t

167− RowConstraint _ r _ -> findUnknownTypes r

168− unsolvedTypes = filter (\n -> TUnknown n == fst (runTypeSolution solution) n) unknownTypes

169− guardWith "Unsolved type variable" $ null $ unsolvedTypes \\ typesMentioned

170− let

171− rowsMentioned = findUnknownRows ty

172− unknownRows = nub $ flip concatMap cs $ \c -> case c of

173− TypeConstraint _ t _ -> findUnknownRows t

174− RowConstraint u r _ -> u : findUnknownRows r

175− unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows

176− guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned

177−

178−findUnknownTypes :: (D.Data d) => d -> [Unknown Type]

179−findUnknownTypes = everything (++) (mkQ [] f)

180− where

181− f :: Type -> [Unknown Type]

182− f (TUnknown n) = [n]

183− f _ = []

184−

185−findUnknownRows :: (D.Data d) => d -> [Unknown Row]

186−findUnknownRows = everything (++) (mkQ [] f)

187− where

188− f :: Row -> [Unknown Row]

189− f (RUnknown n) = [n]

190− f _ = []

191−-}

163+ visibleUnknowns = nub $ unknowns ty

164+ in

165+ forM_ checks $ \check -> case check of

166+ AnyUnifiable t -> do

167+ let unsolvedUnknowns = nub . unknowns $ apply sub t

168+ guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns

192169

193170setify :: Row -> Row

194171setify = rowFromList . first (M.toList . M.fromList) . rowToList

@@ -287,7 +264,10 @@ ensureNoDuplicateProperties :: [(String, Value)] -> Check ()

287264ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps

288265

289266infer :: M.Map Ident Type -> Value -> Subst Check Type

290−infer m val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ infer' m val

267+infer m val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ do

268+ ty <- infer' m val

269+ escapeCheckLater ty

270+ return ty

291271

292272infer' _ (NumericLiteral _) = return Number

293273infer' _ (StringLiteral _) = return String

@@ -327,17 +307,17 @@ infer' m (Accessor prop val) = do

327307 rest <- fresh

328308 check m val (Object (RCons prop field rest))

329309 return field

330−infer' m v@(Abs args ret) = do

310+infer' m (Abs args ret) = do

331311 ts <- replicateM (length args) fresh

332312 let m' = m `M.union` M.fromList (zip args ts)

333313 body <- infer m' ret

334314 return $ Function ts body

335−infer' m v@(App f xs) = do

315+infer' m (App f xs) = do

336316 t1 <- infer m f

337317 ret <- fresh

338318 checkFunctionApplication m t1 xs ret

339319 return ret

340−infer' m v@(Var var@(Qualified mp name)) = do

320+infer' m (Var var@(Qualified mp name)) = do

341321 case mp of

342322 ModulePath [] ->

343323 case M.lookup name m of

@@ -356,7 +336,7 @@ infer' m (Block ss) = do

356336 (allCodePathsReturn, _) <- checkBlock m M.empty ret ss

357337 guardWith "Block is missing a return statement" allCodePathsReturn

358338 return ret

359−infer' m v@(Constructor c) = do

339+infer' m (Constructor c) = do

360340 env <- lift getEnv

361341 modulePath <- checkModulePath `fmap` lift get

362342 case M.lookup (qualify modulePath c) (dataConstructors env) of

@@ -367,13 +347,13 @@ infer' m (Case val binders) = do

367347 ret <- fresh

368348 checkBinders m t1 ret binders

369349 return ret

370−infer' m v@(IfThenElse cond th el) = do

350+infer' m (IfThenElse cond th el) = do

371351 check m cond Boolean

372352 t2 <- infer m th

373353 t3 <- infer m el

374354 t2 ~~ t3

375355 return t2

376−infer' m v@(TypedValue val ty) = do

356+infer' m (TypedValue val ty) = do

377357 kind <- lift $ kindOf ty

378358 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

379359 ty' <- lift $ replaceAllTypeSynonyms ty

@@ -464,7 +444,7 @@ inferBinder val (NullaryBinder ctor) = do

464444 ty `subsumes` val

465445 return M.empty

466446 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"

467−inferBinder val b@(UnaryBinder ctor binder) = do

447+inferBinder val (UnaryBinder ctor binder) = do

468448 env <- lift getEnv

469449 modulePath <- checkModulePath `fmap` lift get

470450 case M.lookup (qualify modulePath ctor) (dataConstructors env) of

@@ -473,7 +453,7 @@ inferBinder val b@(UnaryBinder ctor binder) = do

473453 ty `subsumes` (Function [obj] val)

474454 inferBinder obj binder

475455 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"

476−inferBinder val b@(ObjectBinder props) = do

456+inferBinder val (ObjectBinder props) = do

477457 row <- fresh

478458 rest <- fresh

479459 m1 <- inferRowProperties row rest props

@@ -501,7 +481,7 @@ inferBinder val (NamedBinder name binder) = do

501481 return $ M.insert name val m

502482

503483inferGuardedBinder :: M.Map Ident Type -> Type -> Binder -> Subst Check (M.Map Ident Type)

504−inferGuardedBinder m val b@(GuardedBinder cond binder) = do

484+inferGuardedBinder m val (GuardedBinder cond binder) = do

505485 m1 <- inferBinder val binder

506486 ty <- infer (m `M.union` m1) cond

507487 ty ~~ Boolean

@@ -591,24 +571,46 @@ skolemize ident ty = do

591571 return $ replaceRowVars (M.singleton ident rsk) $ replaceTypeVars (M.singleton ident tsk) ty

592572

593573check :: M.Map Ident Type -> Value -> Type -> Subst Check ()

594−check m (NumericLiteral _) Number = return ()

595−check m (StringLiteral _) String = return ()

596−check m (BooleanLiteral _) Boolean = return ()

597−check m (Unary op val) ty = checkUnary m op val ty

598−check m (Binary op left right) ty = checkBinary m op left right ty

599−check m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)

600−check m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)

601−check m (Abs args ret) (Function argTys retTy) = do

574+check m val ty = rethrow errorMessage $ check' m val ty

575+ where

576+ errorMessage msg =

577+ "Error checking type of term " ++

578+ prettyPrintValue val ++

579+ " against type " ++

580+ prettyPrintType ty ++

581+ ":\n" ++

582+ msg

583+

584+check' :: M.Map Ident Type -> Value -> Type -> Subst Check ()

585+check' m val (ForAll idents ty) = do

586+ sk <- skolemize idents ty

587+ check m val sk

588+check' m val (SaturatedTypeSynonym name args) = do

589+ env <- lift getEnv

590+ modulePath <- checkModulePath `fmap` lift get

591+ case M.lookup (qualify modulePath name) (typeSynonyms env) of

592+ Just (synArgs, body) -> do

593+ let replaced = replaceTypeVars (M.fromList (zip synArgs args)) body

594+ check m val replaced

595+ Nothing -> error "Type synonym was not defined"

596+check' m val u@(TUnknown _) = do

597+ ty <- infer m val

598+ ty ~~ u

599+check' m (NumericLiteral _) Number = return ()

600+check' m (StringLiteral _) String = return ()

601+check' m (BooleanLiteral _) Boolean = return ()

602+check' m (Unary op val) ty = checkUnary m op val ty

603+check' m (Binary op left right) ty = checkBinary m op left right ty

604+check' m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)

605+check' m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)

606+check' m (Abs args ret) (Function argTys retTy) = do

602607 guardWith "Incorrect number of function arguments" (length args == length argTys)

603608 let bindings = M.fromList (zip args argTys)

604609 check (bindings `M.union` m) ret retTy

605−check m (App f xs) ret = do

610+check' m (App f xs) ret = do

606611 ft <- infer m f

607612 checkFunctionApplication m ft xs ret

608−check m val (ForAll idents ty) = do

609− sk <- skolemize idents ty

610− check m val sk

611−check m v@(Var var@(Qualified mp name)) ty = do

613+check' m v@(Var var@(Qualified mp name)) ty = do

612614 case mp of

613615 ModulePath [] ->

614616 case M.lookup name m of

@@ -626,36 +628,32 @@ check m v@(Var var@(Qualified mp name)) ty = do

626628 Just (ty1, _) -> do

627629 repl <- lift $ replaceAllTypeSynonyms ty1

628630 repl `subsumes` ty

629−check m val u@(TUnknown _) = do

630− ty <- infer m val

631− ty ~~ u

632− return ()

633−check m (TypedValue val ty1) ty2 = do

631+check' m (TypedValue val ty1) ty2 = do

634632 kind <- lift $ kindOf ty1

635633 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

636634 ty1 `subsumes` ty2

637635 check m val ty1

638−check m (Case val binders) ret = do

636+check' m (Case val binders) ret = do

639637 t1 <- infer m val

640638 checkBinders m t1 ret binders

641−check m (IfThenElse cond th el) ty = do

639+check' m (IfThenElse cond th el) ty = do

642640 check m cond Boolean

643641 check m th ty

644642 check m el ty

645−check m (ObjectLiteral ps) (Object row) = do

643+check' m (ObjectLiteral ps) (Object row) = do

646644 lift $ ensureNoDuplicateProperties ps

647645 checkProperties m ps row False

648−check m (ObjectUpdate obj ps) objTy@(Object row) = do

646+check' m (ObjectUpdate obj ps) objTy@(Object row) = do

649647 lift $ ensureNoDuplicateProperties ps

650648 check m obj objTy

651649 checkProperties m ps row True

652−check m (Accessor prop val) ty = do

650+check' m (Accessor prop val) ty = do

653651 rest <- fresh

654652 check m val (Object (RCons prop ty rest))

655−check m (Block ss) ret = do

653+check' m (Block ss) ret = do

656654 (allCodePathsReturn, _) <- checkBlock m M.empty ret ss

657655 guardWith "Block is missing a return statement" allCodePathsReturn

658−check m (Constructor c) ty = do

656+check' m (Constructor c) ty = do

659657 env <- lift getEnv

660658 modulePath <- checkModulePath `fmap` lift get

661659 case M.lookup (qualify modulePath c) (dataConstructors env) of

@@ -663,15 +661,7 @@ check m (Constructor c) ty = do

663661 Just ty1 -> do

664662 repl <- lift $ replaceAllTypeSynonyms ty1

665663 repl `subsumes` ty

666−check m val (SaturatedTypeSynonym name args) = do

667− env <- lift getEnv

668− modulePath <- checkModulePath `fmap` lift get

669− case M.lookup (qualify modulePath name) (typeSynonyms env) of

670− Just (synArgs, body) -> do

671− let replaced = replaceTypeVars (M.fromList (zip synArgs args)) body

672− check m val replaced

673− Nothing -> error "Type synonym was not defined"

674−check _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty

664+check' _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty

675665

676666checkProperties :: M.Map Ident Type -> [(String, Value)] -> Row -> Bool -> Subst Check ()

677667checkProperties m ps row lax = let (ts, r') = rowToList row in go ps ts r' where

@@ -699,17 +689,26 @@ checkProperties m ps row lax = let (ts, r') = rowToList row in go ps ts r' where

699689 go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (Object row)

700690

701691checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()

702−checkFunctionApplication m (Function argTys retTy) args ret = do

692+checkFunctionApplication m fnTy args ret = rethrow errorMessage $ checkFunctionApplication' m fnTy args ret

693+ where

694+ errorMessage msg = "Error applying function of type "

695+ ++ prettyPrintType fnTy

696+ ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)

697+ ++ ", expecting value of type "

698+ ++ prettyPrintType ret ++ ":\n" ++ msg

699+

700+checkFunctionApplication' :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()

701+checkFunctionApplication' m (Function argTys retTy) args ret = do

703702 guardWith "Incorrect number of function arguments" (length args == length argTys)

704703 zipWithM (check m) args argTys

705− ret ~~ retTy

706−checkFunctionApplication m (ForAll ident ty) args ret = do

704+ retTy `subsumes` ret

705+checkFunctionApplication' m (ForAll ident ty) args ret = do

707706 replaced <- replaceVarsWithUnknowns [ident] ty

708707 checkFunctionApplication m replaced args ret

709−checkFunctionApplication m u@(TUnknown _) args ret = do

710− tyArgs <- replicateM (length args) fresh

711− u ~~ Function tyArgs ret

712−checkFunctionApplication _ fnTy args ret = throwError $ "Cannot apply function of type "

708+checkFunctionApplication' m u@(TUnknown _) args ret = do

709+ tyArgs <- mapM (infer m) args

710+ u `subsumes` Function tyArgs ret

711+checkFunctionApplication' _ fnTy args ret = throwError $ "Cannot apply function of type "

713712 ++ prettyPrintType fnTy

714713 ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)

715714 ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."