558cd4e · rowtype-yoga/purescript-native

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

on golang help sign in

More bug fixes

558cd4ePhil Freeman13 years ago

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

compare with golang

unifiedsplit

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

28import Language.PureScript.Values

29import Language.PureScript.Names

30import Language.PureScript.Pretty.Common

31+import Language.PureScript.Pretty.Types

32literals :: Pattern () Value String

33literals :: Pattern () Value String

33literals = mkPattern match

34literals = mkPattern match

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

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

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

84 match _ = Nothing

85 match _ = Nothing

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

88+typed = mkPattern match

89+ where

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

91+ match _ = Nothing

92+

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

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

87unary op str = Wrap pattern (++)

94unary op str = Wrap pattern (++)

88 where

95 where

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

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

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

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

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

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

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

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

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

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

117 , [ binary LessThan "<" ]

125 , [ binary LessThan "<" ]

118 , [ binary LessThanOrEqualTo "<=" ]

126 , [ binary LessThanOrEqualTo "<=" ]

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

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

62 unknowns _ = []

64kindOf :: 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

67kindsOf :: 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

69 tyCon <- fresh

70 kargs <- replicateM (length args) fresh

71 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 @@

13-----------------------------------------------------------------------------

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

16− StandaloneDeriving, MultiParamTypeClasses, FlexibleContexts #-}

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

18module Language.PureScript.TypeChecker.Monad where

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

49emptyEnvironment :: Environment

50emptyEnvironment = Environment M.empty M.empty M.empty M.empty M.empty

52+data AnyUnifiable where

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

54+

52data CheckState = CheckState { checkEnv :: Environment

55data CheckState = CheckState { checkEnv :: Environment

53 , checkNextVar :: Int

56 , checkNextVar :: Int

54 , checkModulePath :: ModulePath

57 , checkModulePath :: ModulePath

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

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

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

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

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

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+

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

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

62instance Monoid Substitution where

94instance Monoid Substitution where

63 mempty = Substitution unknown

95 mempty = Substitution unknown

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

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

98+data SubstState = SubstState { substSubst :: Substitution

99+ , substFutureEscapeChecks :: [AnyUnifiable] }

100+

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

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

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

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

103

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

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

105

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

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

72runSubst subst = do

107runSubst subst = do

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

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

74− return $ apply s a

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

110

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

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

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

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

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

121

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

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

88replace u t' = do

123replace u t' = do

89− sub <- Subst get

124+ sub <- substSubst <$> Subst get

90 let t = apply sub t'

125 let t = apply sub t'

91 occursCheck u t

126 occursCheck u t

92 let current = apply sub $ unknown u

127 let current = apply sub $ unknown u

93 case isUnknown current of

128 case isUnknown current of

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

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

95 _ -> current ~~ t

130 _ -> current ~~ t

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

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

132

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

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

99 unknown :: Unknown t -> t

134 unknown :: Unknown t -> t

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

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

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

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

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

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

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

109 _ -> return ()

144 _ -> return ()

110

145

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−

120fresh' :: Subst Check Int

146fresh' :: Subst Check Int

121fresh' = do

147fresh' = do

122 n <- lift $ checkNextVar <$> get

148 n <- lift $ checkNextVar <$> get

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

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

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

127fresh = unknown . Unknown <$> fresh'

153fresh = unknown . Unknown <$> fresh'

128

154

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

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

130−runCheck c = do

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

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

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

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

19) where

21import Data.List

22−import Data.Maybe (fromMaybe)

22+import Data.Maybe (isJust, fromMaybe)

23import Data.Function

24import qualified Data.Data as D

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

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

147

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

149typeOf name val = do

150− ty <- runSubst $ case name of

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

151+ Just ident | isFunction val ->

151− Just ident -> do me <- fresh

152+ do me <- fresh

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

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

153− me ~~ ty

154+ me ~~ ty

154− return ty

155+ return ty

155− Nothing -> infer M.empty val

156+ _ -> infer M.empty val

156− --desugared <- replaceAllTypeSynonyms cs

157+ escapeCheck checks ty sub

157− --TODO: allUnknownsBecameQuantified desugared solution ty

158 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty

159

160−{-

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

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

161+escapeCheck checks ty sub =

162−allUnknownsBecameQuantified cs solution ty = do

163 let

162 let

164− typesMentioned = findUnknownTypes ty

163+ visibleUnknowns = nub $ unknowns ty

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

164+ in

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

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

167− RowConstraint _ r _ -> findUnknownTypes r

166+ AnyUnifiable t -> do

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

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

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

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

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−-}

192

169

193setify :: Row -> Row

170setify :: Row -> Row

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

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

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

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

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

288

265

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

266infer :: 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

291

271

292infer' _ (NumericLiteral _) = return Number

272infer' _ (NumericLiteral _) = return Number

293infer' _ (StringLiteral _) = return String

273infer' _ (StringLiteral _) = return String

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

327 rest <- fresh

307 rest <- fresh

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

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

329 return field

309 return field

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

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

331 ts <- replicateM (length args) fresh

311 ts <- replicateM (length args) fresh

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

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

333 body <- infer m' ret

313 body <- infer m' ret

334 return $ Function ts body

314 return $ Function ts body

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

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

336 t1 <- infer m f

316 t1 <- infer m f

337 ret <- fresh

317 ret <- fresh

338 checkFunctionApplication m t1 xs ret

318 checkFunctionApplication m t1 xs ret

339 return ret

319 return ret

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

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

341 case mp of

321 case mp of

342 ModulePath [] ->

322 ModulePath [] ->

343 case M.lookup name m of

323 case M.lookup name m of

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

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

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

357 guardWith "Block is missing a return statement" allCodePathsReturn

337 guardWith "Block is missing a return statement" allCodePathsReturn

358 return ret

338 return ret

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

339+infer' m (Constructor c) = do

360 env <- lift getEnv

340 env <- lift getEnv

361 modulePath <- checkModulePath `fmap` lift get

341 modulePath <- checkModulePath `fmap` lift get

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

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

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

367 ret <- fresh

347 ret <- fresh

368 checkBinders m t1 ret binders

348 checkBinders m t1 ret binders

369 return ret

349 return ret

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

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

371 check m cond Boolean

351 check m cond Boolean

372 t2 <- infer m th

352 t2 <- infer m th

373 t3 <- infer m el

353 t3 <- infer m el

374 t2 ~~ t3

354 t2 ~~ t3

375 return t2

355 return t2

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

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

377 kind <- lift $ kindOf ty

357 kind <- lift $ kindOf ty

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

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

379 ty' <- lift $ replaceAllTypeSynonyms ty

359 ty' <- lift $ replaceAllTypeSynonyms ty

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

464 ty `subsumes` val

444 ty `subsumes` val

465 return M.empty

445 return M.empty

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

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

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

447+inferBinder val (UnaryBinder ctor binder) = do

468 env <- lift getEnv

448 env <- lift getEnv

469 modulePath <- checkModulePath `fmap` lift get

449 modulePath <- checkModulePath `fmap` lift get

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

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

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

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

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

474 inferBinder obj binder

454 inferBinder obj binder

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

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

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

456+inferBinder val (ObjectBinder props) = do

477 row <- fresh

457 row <- fresh

478 rest <- fresh

458 rest <- fresh

479 m1 <- inferRowProperties row rest props

459 m1 <- inferRowProperties row rest props

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

501 return $ M.insert name val m

481 return $ M.insert name val m

502

482

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

483inferGuardedBinder :: 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

505 m1 <- inferBinder val binder

485 m1 <- inferBinder val binder

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

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

507 ty ~~ Boolean

487 ty ~~ Boolean

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

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

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

592

572

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

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

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

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

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

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

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

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

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

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

602+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

603+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)

604+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)

605+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

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

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

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

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

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

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

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

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

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

606 ft <- infer m f

611 ft <- infer m f

607 checkFunctionApplication m ft xs ret

612 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

612 case mp of

614 case mp of

613 ModulePath [] ->

615 ModulePath [] ->

614 case M.lookup name m of

616 case M.lookup name m of

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

626 Just (ty1, _) -> do

628 Just (ty1, _) -> do

627 repl <- lift $ replaceAllTypeSynonyms ty1

629 repl <- lift $ replaceAllTypeSynonyms ty1

628 repl `subsumes` ty

630 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

634 kind <- lift $ kindOf ty1

632 kind <- lift $ kindOf ty1

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

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

636 ty1 `subsumes` ty2

634 ty1 `subsumes` ty2

637 check m val ty1

635 check m val ty1

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

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

639 t1 <- infer m val

637 t1 <- infer m val

640 checkBinders m t1 ret binders

638 checkBinders m t1 ret binders

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

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

642 check m cond Boolean

640 check m cond Boolean

643 check m th ty

641 check m th ty

644 check m el ty

642 check m el ty

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

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

646 lift $ ensureNoDuplicateProperties ps

644 lift $ ensureNoDuplicateProperties ps

647 checkProperties m ps row False

645 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

649 lift $ ensureNoDuplicateProperties ps

647 lift $ ensureNoDuplicateProperties ps

650 check m obj objTy

648 check m obj objTy

651 checkProperties m ps row True

649 checkProperties m ps row True

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

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

653 rest <- fresh

651 rest <- fresh

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

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

655−check m (Block ss) ret = do

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

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

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

657 guardWith "Block is missing a return statement" allCodePathsReturn

655 guardWith "Block is missing a return statement" allCodePathsReturn

658−check m (Constructor c) ty = do

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

659 env <- lift getEnv

657 env <- lift getEnv

660 modulePath <- checkModulePath `fmap` lift get

658 modulePath <- checkModulePath `fmap` lift get

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

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

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

663 Just ty1 -> do

661 Just ty1 -> do

664 repl <- lift $ replaceAllTypeSynonyms ty1

662 repl <- lift $ replaceAllTypeSynonyms ty1

665 repl `subsumes` ty

663 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

675

665

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

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

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

667checkProperties 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

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

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

700

690

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

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

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 ()

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

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

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

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

704 zipWithM (check m) args argTys

703 zipWithM (check m) args argTys

705− ret ~~ retTy

704+ retTy `subsumes` ret

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

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

707 replaced <- replaceVarsWithUnknowns [ident] ty

706 replaced <- replaceVarsWithUnknowns [ident] ty

708 checkFunctionApplication m replaced args ret

707 checkFunctionApplication m replaced args ret

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

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

710− tyArgs <- replicateM (length args) fresh

709+ tyArgs <- mapM (infer m) args

711− u ~~ Function tyArgs ret

710+ u `subsumes` Function tyArgs ret

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

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

713 ++ prettyPrintType fnTy

712 ++ prettyPrintType fnTy

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

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

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

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