@@ -143,7 +143,7 @@ typeConstructorsAreEqual env moduleName = (==) `on` canonicalizeType moduleName
143143
144144typesOf :: ModuleName -> [(Ident, Value)] -> Check [Type]
145145typesOf moduleName vals = do
146− (tys, sub, checks) <- runSubst (SubstContext moduleName) $ do
146+ (tys, sub) <- runSubst (SubstContext moduleName) $ do
147147 let es = map isTyped vals
148148 typed = filter (isJust . snd . snd) es
149149 untyped = filter (isNothing . snd . snd) es
@@ -160,7 +160,7 @@ typesOf moduleName vals = do
160160 bindNames dict $ check val ty'
161161 return ty'
162162 (ident, (val, Nothing)) -> do
163− ty <- bindNames dict $ infer val
163+ TypedValue _ ty <- bindNames dict $ infer val
164164 ty ~~ fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
165165 return ty
166166 when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do
@@ -168,7 +168,7 @@ typesOf moduleName vals = do
168168 ty ~~ TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a
169169 return ty
170170 return tys
171− forM tys $ flip (escapeCheck checks) sub
171+ --forM tys $ flip (escapeCheck checks) sub
172172 forM tys $ skolemEscapeCheck
173173 return $ map (varIfUnknown . desaturateAllTypeSynonyms . setifyAll) tys
174174
@@ -176,7 +176,7 @@ isTyped :: (Ident, Value) -> (Ident, (Value, Maybe Type))
176176isTyped (name, TypedValue value ty) = (name, (value, Just ty))
177177isTyped (name, value) = (name, (value, Nothing))
178178
179−escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()
179+{-escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()
180180escapeCheck checks ty sub =
181181 let
182182 visibleUnknowns = nub $ unknowns ty
@@ -185,6 +185,7 @@ escapeCheck checks ty sub =
185185 AnyUnifiable t -> do
186186 let unsolvedUnknowns = nub . unknowns $ apply sub t
187187 guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
188+-}
188189
189190skolemEscapeCheck :: Type -> Check ()
190191skolemEscapeCheck ty =
@@ -247,100 +248,99 @@ expandTypeSynonym name args = do
247248ensureNoDuplicateProperties :: (MonadError String m) => [(String, Value)] -> m ()
248249ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
249250
250−infer :: Value -> Subst Type
251−infer val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ do
252− ty <- infer' val
253− escapeCheckLater ty
254− return ty
251+infer :: Value -> Subst Value
252+infer val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ infer' val
255253
256−infer' :: Value -> Subst Type
257−infer' (NumericLiteral _) = return Number
258−infer' (StringLiteral _) = return String
259−infer' (BooleanLiteral _) = return Boolean
254+infer' :: Value -> Subst Value
255+infer' v@(NumericLiteral _) = return $ TypedValue v Number
256+infer' v@(StringLiteral _) = return $ TypedValue v String
257+infer' v@(BooleanLiteral _) = return $ TypedValue v Boolean
260258infer' (ArrayLiteral vals) = do
261− ts <- mapM (infer) vals
259+ ts <- mapM infer vals
262260 els <- fresh
263− forM_ ts $ \t -> els ~~ Array t
264− return els
261+ forM_ ts $ \(TypedValue _ t) -> els ~~ Array t
262+ return $ TypedValue (ArrayLiteral ts) els
265263infer' (Unary op val) = do
266− t <- infer val
267− inferUnary op t
264+ v <- infer val
265+ inferUnary op v
268266infer' (Binary op left right) = do
269− t1 <- infer left
270− t2 <- infer right
271− inferBinary op t1 t2
267+ v1 <- infer left
268+ v2 <- infer right
269+ inferBinary op v1 v2
272270infer' (ObjectLiteral ps) = do
273271 ensureNoDuplicateProperties ps
274272 ts <- mapM (infer . snd) ps
275− let fields = zipWith (\(name, _) t -> (name, t)) ps ts
276− return $ Object $ rowFromList (fields, REmpty)
273+ let fields = zipWith (\name (TypedValue _ t) -> (name, t)) (map fst ps) ts
274+ ty = Object $ rowFromList (fields, REmpty)
275+ return $ TypedValue (ObjectLiteral (zip (map fst ps) ts)) ty
277276infer' (ObjectUpdate o ps) = do
278277 ensureNoDuplicateProperties ps
279278 row <- fresh
280− newTys <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps
279+ newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps
280+ let newTys = map (\(name, TypedValue _ ty) -> (name, ty)) newVals
281281 oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh
282− check o $ Object $ rowFromList (oldTys, row)
283− return $ Object $ rowFromList (newTys, row)
282+ o' <- check o $ Object $ rowFromList (oldTys, row)
283+ return $ TypedValue (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)
284284infer' (Indexer index val) = do
285285 el <- fresh
286286 check index Number
287287 check val (Array el)
288− return el
288+ return $ TypedValue (Indexer (TypedValue index Number) (TypedValue val (Array el))) el
289289infer' (Accessor prop val) = do
290− obj <- infer val
291− propTy <- inferProperty obj prop
290+ typed@(TypedValue _ objTy) <- infer val
291+ propTy <- inferProperty objTy prop
292292 case propTy of
293293 Nothing -> do
294294 field <- fresh
295295 rest <- fresh
296− obj `subsumes` Object (RCons prop field rest)
297− return field
298− Just ty -> return ty
296+ objTy `subsumes` Object (RCons prop field rest)
297+ return $ TypedValue (Accessor prop typed) field
298+ Just ty -> return $ TypedValue (Accessor prop typed) ty
299299infer' (Abs args ret) = do
300300 ts <- replicateM (length args) fresh
301301 moduleName <- substCurrentModule <$> ask
302302 bindLocalVariables moduleName (zip args ts) $ do
303− body <- infer' ret
304− return $ Function ts body
305−infer' app@(App _ _) = do
306− let (f, argss) = unfoldApplication app
307− ft <- infer f
303+ (TypedValue body bodyTy) <- infer' ret
304+ return $ TypedValue (Abs args body) $ Function ts bodyTy
305+infer' (App f args) = do
306+ (TypedValue f' ft) <- infer f
308307 ret <- fresh
309− checkFunctionApplications ft argss ret
310− return ret
308+ args' <- checkFunctionApplication ft args ret
309+ return $ TypedValue (App f' args') ret
311310infer' (Var var) = do
312311 moduleName <- substCurrentModule <$> ask
313312 ty <- lookupVariable moduleName var
314− replaceAllTypeSynonyms ty
313+ ty' <- replaceAllTypeSynonyms ty
314+ return $ TypedValue (Var var) ty'
315315infer' (Block ss) = do
316316 ret <- fresh
317− (allCodePathsReturn, _) <- checkBlock M.empty ret ss
317+ (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss
318318 guardWith "Block is missing a return statement" allCodePathsReturn
319− return ret
320−infer' (Constructor c) = do
319+ return $ TypedValue (Block ss') ret
320+infer' v@(Constructor c) = do
321321 env <- getEnv
322322 moduleName <- substCurrentModule `fmap` ask
323323 case M.lookup (qualify moduleName c) (dataConstructors env) of
324324 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
325− Just (ty, _) -> replaceAllTypeSynonyms ty
325+ Just (ty, _) -> do ty' <- replaceAllTypeSynonyms ty
326+ return $ TypedValue v ty'
326327infer' (Case vals binders) = do
327328 ts <- mapM infer vals
328329 ret <- fresh
329− checkBinders ts ret binders
330− return ret
330+ binders' <- checkBinders (map (\(TypedValue _ t) -> t) ts) ret binders
331+ return $ TypedValue (Case ts binders') ret
331332infer' (IfThenElse cond th el) = do
332333 check cond Boolean
333− t2 <- infer th
334− t3 <- infer el
334+ TypedValue v2 t2 <- infer th
335+ TypedValue v3 t3 <- infer el
335336 t2 ~~ t3
336− return t2
337+ return $ TypedValue (IfThenElse cond v2 v3) t2
337338infer' (TypedValue val ty) = do
338339 moduleName <- substCurrentModule <$> ask
339340 kind <- liftCheck $ kindOf moduleName ty
340341 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
341342 ty' <- replaceAllTypeSynonyms ty
342343 check val ty'
343− return ty'
344344infer' _ = error "Invalid argument to infer"
345345
346346inferProperty :: Type -> String -> Subst (Maybe Type)
@@ -355,14 +355,15 @@ inferProperty (ForAll ident ty) prop = do
355355 inferProperty replaced prop
356356inferProperty _ _ = return Nothing
357357
358−inferUnary :: UnaryOperator -> Type -> Subst Type
359−inferUnary op val =
358+inferUnary :: UnaryOperator -> Value -> Subst Value
359+inferUnary op (TypedValue val valTy) =
360360 case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
361− (valTy, resTy) -> do
362− val ~~ valTy
363− return resTy
361+ (valTy', resTy) -> do
362+ valTy' ~~ valTy
363+ return $ TypedValue (Unary op val) resTy
364+inferUnary _ _ = error "Invalid arguments to inferUnary"
364365
365−checkUnary :: UnaryOperator -> Value -> Type -> Subst ()
366+checkUnary :: UnaryOperator -> Value -> Type -> Subst Value
366367checkUnary op val res =
367368 case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
368369 (valTy, resTy) -> do
@@ -375,29 +376,32 @@ unaryOps = [ (Negate, (Number, Number))
375376 , (BitwiseNot, (Number, Number))
376377 ]
377378
378−inferBinary :: BinaryOperator -> Type -> Type -> Subst Type
379−inferBinary op left right | isEqualityTest op = do
380− left ~~ right
381− return Boolean
382−inferBinary op left right =
379+inferBinary :: BinaryOperator -> Value -> Value -> Subst Value
380+inferBinary op left@(TypedValue _ leftTy) right@(TypedValue _ rightTy) | isEqualityTest op = do
381+ leftTy ~~ rightTy
382+ return $ TypedValue (Binary op left right) Boolean
383+inferBinary op left@(TypedValue _ leftTy) right@(TypedValue _ rightTy) =
383384 case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
384385 (valTy, resTy) -> do
385− left ~~ valTy
386− right ~~ valTy
387− return resTy
386+ leftTy ~~ valTy
387+ rightTy ~~ valTy
388+ return $ TypedValue (Binary op left right) resTy
389+inferBinary _ _ _ = error "Invalid arguments to inferBinary"
388390
389−checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst ()
391+checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst Value
390392checkBinary op left right res | isEqualityTest op = do
391393 res ~~ Boolean
392− t1 <- infer left
393− t2 <- infer right
394+ TypedValue v1 t1 <- infer left
395+ TypedValue v2 t2 <- infer right
394396 t1 ~~ t2
397+ return $ TypedValue (Binary op v1 v2) $ res
395398checkBinary op left right res =
396399 case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
397400 (valTy, resTy) -> do
398401 res ~~ resTy
399− check left valTy
400− check right valTy
402+ v1 <- check left valTy
403+ v2 <- check right valTy
404+ return $ TypedValue (Binary op v1 v2) $ res
401405
402406isEqualityTest :: BinaryOperator -> Bool
403407isEqualityTest EqualTo = True
@@ -480,17 +484,20 @@ inferBinder val (NamedBinder name binder) = do
480484 m <- inferBinder val binder
481485 return $ M.insert name val m
482486
483−checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> Subst ()
484−checkBinders _ _ [] = return ()
487+checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> Subst [([Binder], Maybe Guard, Value)]
488+checkBinders _ _ [] = return []
485489checkBinders nvals ret ((binders, grd, val):bs) = do
486490 moduleName <- substCurrentModule <$> ask
487491 m1 <- M.unions <$> zipWithM inferBinder nvals binders
488− bindLocalVariables moduleName (M.toList m1) $ do
489− check val ret
492+ r <- bindLocalVariables moduleName (M.toList m1) $ do
493+ val' <- check val ret
490494 case grd of
491− Nothing -> return ()
492− Just g -> check g Boolean
493− checkBinders nvals ret bs
495+ Nothing -> return (binders, Nothing, val')
496+ Just g -> do
497+ g' <- check g Boolean
498+ return (binders, Just g', val')
499+ rs <- checkBinders nvals ret bs
500+ return $ r : rs
494501
495502assignVariable :: Ident -> Subst ()
496503assignVariable name = do
@@ -500,66 +507,70 @@ assignVariable name = do
500507 Just (_, LocalVariable) -> throwError $ "Variable with name " ++ show name ++ " already exists."
501508 _ -> return ()
502509
503−checkStatement :: M.Map Ident Type -> Type -> Statement -> Subst (Bool, M.Map Ident Type)
510+checkStatement :: M.Map Ident Type -> Type -> Statement -> Subst (Bool, M.Map Ident Type, Statement)
504511checkStatement mass _ (VariableIntroduction name val) = do
505512 assignVariable name
506− t <- infer val
507− return (False, M.insert name t mass)
513+ val'@(TypedValue _ t) <- infer val
514+ return (False, M.insert name t mass, VariableIntroduction name val')
508515checkStatement mass _ (Assignment ident val) = do
509− t <- infer val
516+ val'@(TypedValue _ t) <- infer val
510517 case M.lookup ident mass of
511518 Nothing -> throwError $ "No local variable with name " ++ show ident
512519 Just ty -> do t ~~ ty
513− return (False, mass)
520+ return (False, mass, Assignment ident val')
514521checkStatement mass ret (While val inner) = do
515− check val Boolean
516− (allCodePathsReturn, _) <- checkBlock mass ret inner
517− return (allCodePathsReturn, mass)
522+ val' <- check val Boolean
523+ (allCodePathsReturn, _, inner') <- checkBlock mass ret inner
524+ return (allCodePathsReturn, mass, While val' inner')
518525checkStatement mass ret (If ifst) = do
519− allCodePathsReturn <- checkIfStatement mass ret ifst
520− return (allCodePathsReturn, mass)
526+ (allCodePathsReturn, ifst') <- checkIfStatement mass ret ifst
527+ return (allCodePathsReturn, mass, If ifst')
521528checkStatement mass ret (For ident start end inner) = do
522529 moduleName <- substCurrentModule <$> ask
523530 assignVariable ident
524− check start Number
525− check end Number
526− (allCodePathsReturn, _) <- bindLocalVariables moduleName [(ident, Number)] $ checkBlock mass ret inner
527− return (allCodePathsReturn, mass)
531+ start' <- check start Number
532+ end' <- check end Number
533+ (allCodePathsReturn, _, inner') <- bindLocalVariables moduleName [(ident, Number)] $ checkBlock mass ret inner
534+ return (allCodePathsReturn, mass, For ident start' end' inner')
528535checkStatement mass ret (Return val) = do
529− check val ret
530− return (True, mass)
536+ val' <- check val ret
537+ return (True, mass, Return val')
531538
532−checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> Subst Bool
539+checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> Subst (Bool, IfStatement)
533540checkIfStatement mass ret (IfStatement val thens Nothing) = do
534− check val Boolean
535− _ <- checkBlock mass ret thens
536− return False
541+ val' <- check val Boolean
542+ (_, _, thens') <- checkBlock mass ret thens
543+ return (False, IfStatement val' thens' Nothing)
537544checkIfStatement mass ret (IfStatement val thens (Just elses)) = do
538− check val Boolean
539− (allCodePathsReturn1, _) <- checkBlock mass ret thens
540− allCodePathsReturn2 <- checkElseStatement mass ret elses
541− return $ allCodePathsReturn1 && allCodePathsReturn2
542−
543−checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> Subst Bool
544−checkElseStatement mass ret (Else elses) = fst <$> checkBlock mass ret elses
545−checkElseStatement mass ret (ElseIf ifst) = checkIfStatement mass ret ifst
546−
547−checkBlock :: M.Map Ident Type -> Type -> [Statement] -> Subst (Bool, M.Map Ident Type)
548−checkBlock mass _ [] = return (False, mass)
545+ val' <- check val Boolean
546+ (allCodePathsReturn1, _, thens') <- checkBlock mass ret thens
547+ (allCodePathsReturn2, elses') <- checkElseStatement mass ret elses
548+ return (allCodePathsReturn1 && allCodePathsReturn2, IfStatement val' thens' (Just elses'))
549+
550+checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> Subst (Bool, ElseStatement)
551+checkElseStatement mass ret (Else elses) = do
552+ (allCodePathsReturn, _, elses') <- checkBlock mass ret elses
553+ return (allCodePathsReturn, Else elses')
554+checkElseStatement mass ret (ElseIf ifst) = (id *** ElseIf) <$> checkIfStatement mass ret ifst
555+
556+checkBlock :: M.Map Ident Type -> Type -> [Statement] -> Subst (Bool, M.Map Ident Type, [Statement])
557+checkBlock mass _ [] = return (False, mass, [])
549558checkBlock mass ret (s:ss) = do
550559 moduleName <- substCurrentModule <$> ask
551− (b1, mass1) <- checkStatement mass ret s
560+ (b1, mass1, s') <- checkStatement mass ret s
552561 bindLocalVariables moduleName (M.toList mass1) $ case (b1, ss) of
553− (True, []) -> return (True, mass1)
562+ (True, []) -> return (True, mass1, [s'])
554563 (True, _) -> throwError "Unreachable code"
555− (False, ss') -> checkBlock mass1 ret ss'
564+ (False, ss') -> do
565+ (b, m, ss'') <- checkBlock mass1 ret ss'
566+ return (b, m, s':ss'')
556567
557568skolemize :: String -> Type -> Subst Type
558569skolemize ident ty = do
559570 tsk <- Skolem <$> fresh'
560571 return $ replaceTypeVars ident tsk ty
561572
562−check :: Value -> Type -> Subst ()
573+check :: Value -> Type -> Subst Value
563574check val ty = rethrow errorMessage $ check' val ty
564575 where
565576 errorMessage msg =
@@ -570,65 +581,73 @@ check val ty = rethrow errorMessage $ check' val ty
570581 ":\n" ++
571582 msg
572583
573−check' :: Value -> Type -> Subst ()
584+check' :: Value -> Type -> Subst Value
574585check' val (ForAll idents ty) = do
575586 sk <- skolemize idents ty
576587 check val sk
577588check' val u@(TUnknown _) = do
578− ty <- infer val
589+ val'@(TypedValue _ ty) <- infer val
579590 -- Don't unify an unknown with an inferred polytype
580591 ty' <- replaceAllVarsWithUnknowns ty
581592 ty' ~~ u
582−check' (NumericLiteral _) Number = return ()
583−check' (StringLiteral _) String = return ()
584−check' (BooleanLiteral _) Boolean = return ()
593+ return val'
594+check' v@(NumericLiteral _) Number = return $ TypedValue v Number
595+check' v@(StringLiteral _) String = return $ TypedValue v String
596+check' v@(BooleanLiteral _) Boolean = return $ TypedValue v Boolean
585597check' (Unary op val) ty = checkUnary op val ty
586598check' (Binary op left right) ty = checkBinary op left right ty
587−check' (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check val ty)
599+check' (ArrayLiteral vals) (Array ty) = TypedValue <$> (ArrayLiteral <$> forM vals (\val -> check val ty)) <*> pure (Array ty)
588600check' (Indexer index vals) ty = check index Number >> check vals (Array ty)
589601check' (Abs args ret) (Function argTys retTy) = do
590602 moduleName <- substCurrentModule <$> ask
591603 guardWith "Incorrect number of function arguments" (length args == length argTys)
592604 bindLocalVariables moduleName (zip args argTys) $ check ret retTy
593−check' app@(App _ _) ret = do
594− let (f, argss) = unfoldApplication app
595− ft <- infer f
596− checkFunctionApplications ft argss ret
605+check' (App f args) ret = do
606+ f'@(TypedValue _ ft) <- infer f
607+ args' <- checkFunctionApplication ft args ret
608+ return $ TypedValue (App f' args') ret
597609check' (Var var) ty = do
598610 moduleName <- substCurrentModule <$> ask
599611 ty1 <- lookupVariable moduleName var
600612 repl <- replaceAllTypeSynonyms ty1
601613 repl `subsumes` ty
602−check' (TypedValue val ty1) ty2 = do
614+ return $ TypedValue (Var var) ty
615+check' v@(TypedValue val ty1) ty2 = do
603616 moduleName <- substCurrentModule <$> ask
604617 kind <- liftCheck $ kindOf moduleName ty1
605618 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
606619 ty1 `subsumes` ty2
607620 check val ty1
621+ return v
608622check' (Case vals binders) ret = do
609− ts <- mapM infer vals
610− checkBinders ts ret binders
623+ vals' <- mapM infer vals
624+ let ts = map (\(TypedValue _ t) -> t) vals'
625+ binders' <- checkBinders ts ret binders
626+ return $ TypedValue (Case vals' binders') ret
611627check' (IfThenElse cond th el) ty = do
612628 check cond Boolean
613629 check th ty
614630 check el ty
615−check' (ObjectLiteral ps) (Object row) = do
631+check' (ObjectLiteral ps) t@(Object row) = do
616632 ensureNoDuplicateProperties ps
617− checkProperties ps row False
618−check' (ObjectUpdate obj ps) (Object row) = do
633+ ps' <- checkProperties ps row False
634+ return $ TypedValue (ObjectLiteral ps') t
635+check' (ObjectUpdate obj ps) t@(Object row) = do
619636 ensureNoDuplicateProperties ps
620637 us <- zip (map fst ps) <$> replicateM (length ps) fresh
621638 let (propsToCheck, rest) = rowToList row
622639 propsToRemove = map fst ps
623640 remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck
624− check obj (Object (rowFromList (us ++ remainingProps, rest)))
625− checkProperties ps row True
641+ obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))
642+ ps' <- checkProperties ps row True
643+ return $ TypedValue (ObjectUpdate obj' ps') t
626644check' (Accessor prop val) ty = do
627645 rest <- fresh
628646 check val (Object (RCons prop ty rest))
629647check' (Block ss) ret = do
630− (allCodePathsReturn, _) <- checkBlock M.empty ret ss
648+ (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss
631649 guardWith "Block is missing a return statement" allCodePathsReturn
650+ return $ TypedValue (Block ss') ret
632651check' (Constructor c) ty = do
633652 env <- getEnv
634653 moduleName <- substCurrentModule <$> ask
@@ -637,51 +656,42 @@ check' (Constructor c) ty = do
637656 Just (ty1, _) -> do
638657 repl <- replaceAllTypeSynonyms ty1
639658 repl `subsumes` ty
659+ return $ TypedValue (Constructor c) ty
640660check' val (SaturatedTypeSynonym name args) = do
641661 ty <- expandTypeSynonym name args
642662 check val ty
643663check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
644664
645−checkProperties :: [(String, Value)] -> Type -> Bool -> Subst ()
665+checkProperties :: [(String, Value)] -> Type -> Bool -> Subst [(String, Value)]
646666checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
647− go [] [] REmpty = return ()
648− go [] [] u@(TUnknown _) = u ~~ REmpty
649− go [] [] (Skolem _) | lax = return ()
650− go [] ((p, _): _) _ | lax = return ()
667+ go [] [] REmpty = return []
668+ go [] [] u@(TUnknown _) = do u ~~ REmpty
669+ return []
670+ go [] [] (Skolem _) | lax = return []
671+ go [] ((p, _): _) _ | lax = return []
651672 | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p
652673 go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row
653674 go ((p,v):ps') [] u@(TUnknown _) = do
654− ty <- infer v
675+ v'@(TypedValue _ ty) <- infer v
655676 rest <- fresh
656677 u ~~ RCons p ty rest
657− go ps' [] rest
678+ ps'' <- go ps' [] rest
679+ return $ (p, v') : ps''
658680 go ((p,v):ps') ts r =
659681 case lookup p ts of
660682 Nothing -> do
661− ty <- infer v
683+ v'@(TypedValue _ ty) <- infer v
662684 rest <- fresh
663685 r ~~ RCons p ty rest
664− go ps' ts rest
686+ ps'' <- go ps' ts rest
687+ return $ (p, v') : ps''
665688 Just ty -> do
666− check v ty
667− go ps' (delete (p, ty) ts) r
689+ v' <- check v ty
690+ ps'' <- go ps' (delete (p, ty) ts) r
691+ return $ (p, v') : ps''
668692 go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (Object row)
669693
670−unfoldApplication :: Value -> (Value, [[Value]])
671−unfoldApplication = go []
672− where
673− go argss (App f args) = go (args:argss) f
674− go argss f = (f, argss)
675−
676−checkFunctionApplications :: Type -> [[Value]] -> Type -> Subst ()
677−checkFunctionApplications _ [] _ = error "Nullary function application"
678−checkFunctionApplications fnTy [args] ret = checkFunctionApplication fnTy args ret
679−checkFunctionApplications fnTy (args:argss) ret = do
680− argTys <- mapM (infer) args
681− f <- inferFunctionApplication fnTy argTys
682− checkFunctionApplications f argss ret
683−
684−checkFunctionApplication :: Type -> [Value] -> Type -> Subst ()
694+checkFunctionApplication :: Type -> [Value] -> Type -> Subst [Value]
685695checkFunctionApplication fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fnTy args ret
686696 where
687697 errorMessage msg = "Error applying function of type "
@@ -699,7 +709,6 @@ inferFunctionApplication (ForAll ident ty) args = do
699709 replaced <- replaceVarWithUnknown ident ty
700710 inferFunctionApplication replaced args
701711inferFunctionApplication u@(TUnknown _) args = do
702−
703712 ret <- fresh
704713 args' <- mapM replaceAllVarsWithUnknowns args
705714 u ~~ Function args' ret
@@ -711,17 +720,20 @@ inferFunctionApplication fnTy args = throwError $ "Cannot apply function of type
711720 ++ prettyPrintType fnTy
712721 ++ " to argument(s) of type(s) " ++ intercalate ", " (map prettyPrintType args)
713722
714−checkFunctionApplication' :: Type -> [Value] -> Type -> Subst ()
723+checkFunctionApplication' :: Type -> [Value] -> Type -> Subst [Value]
715724checkFunctionApplication' (Function argTys retTy) args ret = do
716725 guardWith "Incorrect number of function arguments" (length args == length argTys)
717− zipWithM (check) args argTys
726+ args' <- zipWithM check args argTys
718727 retTy `subsumes` ret
728+ return args'
719729checkFunctionApplication' (ForAll ident ty) args ret = do
720730 replaced <- replaceVarWithUnknown ident ty
721731 checkFunctionApplication replaced args ret
722732checkFunctionApplication' u@(TUnknown _) args ret = do
723− tyArgs <- mapM (\arg -> infer arg >>= replaceAllVarsWithUnknowns) args
724− u ~~ Function tyArgs ret
733+ args' <- mapM (\arg -> infer arg >>= \(TypedValue v t) -> TypedValue v <$> replaceAllVarsWithUnknowns t) args
734+ let tys = map (\(TypedValue _ t) -> t) args'
735+ u ~~ Function tys ret
736+ return args'
725737checkFunctionApplication' (SaturatedTypeSynonym name tyArgs) args ret = do
726738 ty <- expandTypeSynonym name tyArgs
727739 checkFunctionApplication' ty args ret