e580678 · rowtype-yoga/purescript-native

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

on golang help sign in

Use Environment to store types of local variables.

e580678Phil Freeman13 years ago

examples/failing/LocalVars.pursnew file+3

compare with golang

unifiedsplit

@@ -0,0 +1,3 @@

1+bad = \x -> do

2+ x = x + 1

3+ return x

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

@@ -78,10 +78,10 @@ starIfUnknown (KUnknown _) = Star

78starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)

79starIfUnknown k = k

81−inferAll :: Maybe (ProperName, Kind) -> M.Map String Kind -> [Type] -> Subst Check [Kind]

81+inferAll :: Maybe (ProperName, Kind) -> M.Map String Kind -> [Type] -> Subst [Kind]

82inferAll name m = mapM (infer name m)

84−infer :: Maybe (ProperName, Kind) -> M.Map String Kind -> Type -> Subst Check Kind

84+infer :: Maybe (ProperName, Kind) -> M.Map String Kind -> Type -> Subst Kind

85infer name m (Array t) = do

86 k <- infer name m t

87 k ~~ Star

@@ -102,8 +102,8 @@ infer _ m (TypeVar v) =

102 Nothing -> throwError $ "Unbound type variable " ++ v

103infer (Just (name, k)) m c@(TypeConstructor v@(Qualified (ModulePath []) pn)) | name == pn = return k

104infer name m (TypeConstructor v) = do

105− env <- lift getEnv

105+ env <- liftCheck getEnv

106− modulePath <- checkModulePath `fmap` lift get

106+ modulePath <- checkModulePath `fmap` get

107 case M.lookup (qualify modulePath v) (types env) of

108 Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"

109 Just (kind, _) -> return kind

@@ -118,7 +118,7 @@ infer name m (ForAll ident ty) = do

118 infer name (M.insert ident k m) ty

119infer _ m t = return Star

120

121−inferRow :: Maybe (ProperName, Kind) -> M.Map String Kind -> Row -> Subst Check Kind

121+inferRow :: Maybe (ProperName, Kind) -> M.Map String Kind -> Row -> Subst Kind

122inferRow _ m (RowVar v) = do

123 case M.lookup v m of

124 Just k -> return k

src/Language/PureScript/TypeChecker/Monad.hs+37−17

@@ -34,7 +34,7 @@ import Control.Arrow ((***), first, second)

35import qualified Data.Map as M

37−data NameKind = Value | Extern | Alias ModulePath Ident deriving Show

37+data NameKind = Value | Extern | Alias ModulePath Ident | LocalVariable deriving Show

39data TypeDeclarationKind = Data | ExternData | TypeSynonym deriving Show

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

49emptyEnvironment :: Environment

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

52+bindNames :: (MonadState CheckState m) => M.Map (ModulePath, Ident) (Type, NameKind) -> m a -> m a

53+bindNames newNames action = do

54+ orig <- get

55+ modify $ \st -> st { checkEnv = (checkEnv st) { names = newNames `M.union` (names . checkEnv $ st) } }

56+ a <- action

57+ modify $ \st -> st { checkEnv = (checkEnv st) { names = names . checkEnv $ orig } }

58+ return a

59+

60+bindLocalVariables :: (Functor m, MonadState CheckState m) => [(Ident, Type)] -> m a -> m a

61+bindLocalVariables bindings action = do

62+ modulePath <- checkModulePath `fmap` get

63+ bindNames (M.fromList $ flip map bindings $ \(name, ty) -> ((modulePath, name), (ty, LocalVariable))) action

64+

52data AnyUnifiable where

65data AnyUnifiable where

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

66 AnyUnifiable :: forall t. (Unifiable t) => t -> AnyUnifiable

@@ -60,13 +73,13 @@ data CheckState = CheckState { checkEnv :: Environment

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

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

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

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

63−getEnv :: Check Environment

76+getEnv :: (Functor m, MonadState CheckState m) => m Environment

64−getEnv = fmap checkEnv get

77+getEnv = checkEnv <$> get

66−putEnv :: Environment -> Check ()

79+putEnv :: (MonadState CheckState m) => Environment -> m ()

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

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

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

82+modifyEnv :: (MonadState CheckState m) => (Environment -> Environment) -> m ()

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

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

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

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

@@ -98,12 +111,19 @@ instance Monoid Substitution where

98data SubstState = SubstState { substSubst :: Substitution

111data SubstState = SubstState { substSubst :: Substitution

99 , substFutureEscapeChecks :: [AnyUnifiable] }

112 , substFutureEscapeChecks :: [AnyUnifiable] }

100

113

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

114+newtype Subst a = Subst { unSubst :: StateT SubstState Check a }

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

115+ deriving (Functor, Monad, Applicative, MonadPlus)

116+

117+instance MonadState CheckState Subst where

118+ get = Subst . lift $ get

119+ put = Subst . lift . put

120+

121+deriving instance MonadError String Subst

103

122

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

123+liftCheck :: Check a -> Subst a

124+liftCheck = Subst . lift

105

125

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

126+runSubst :: (Unifiable a) => Subst a -> Check (a, Substitution, [AnyUnifiable])

107runSubst subst = do

127runSubst subst = do

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

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

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

129 return (apply (substSubst s) a, substSubst s, substFutureEscapeChecks s)

@@ -119,7 +139,7 @@ substituteOne u t = substituteWith $ \u1 ->

119 u2 | u2 == u -> t

139 u2 | u2 == u -> t

120 | otherwise -> unknown u2

140 | otherwise -> unknown u2

121

141

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

142+replace :: (Unifiable t) => Unknown t -> t -> Subst ()

123replace u t' = do

143replace u t' = do

124 sub <- substSubst <$> Subst get

144 sub <- substSubst <$> Subst get

125 let t = apply sub t'

145 let t = apply sub t'

@@ -132,25 +152,25 @@ replace u t' = do

132

152

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

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

134 unknown :: Unknown t -> t

154 unknown :: Unknown t -> t

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

155+ (~~) :: t -> t -> Subst ()

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

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

137 apply :: Substitution -> t -> t

157 apply :: Substitution -> t -> t

138 unknowns :: t -> [Int]

158 unknowns :: t -> [Int]

139

159

140−occursCheck :: (Unifiable t) => Unknown s -> t -> Subst Check ()

160+occursCheck :: (Unifiable t) => Unknown s -> t -> Subst ()

141occursCheck (Unknown u) t =

161occursCheck (Unknown u) t =

142 case isUnknown t of

162 case isUnknown t of

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

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

144 _ -> return ()

164 _ -> return ()

145

165

146−fresh' :: Subst Check Int

166+fresh' :: Subst Int

147fresh' = do

167fresh' = do

148− n <- lift $ checkNextVar <$> get

168+ n <- checkNextVar <$> get

149− lift . modify $ \s -> s { checkNextVar = succ (checkNextVar s) }

169+ modify $ \s -> s { checkNextVar = succ (checkNextVar s) }

150 return n

170 return n

151

171

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

172+fresh :: (Unifiable t) => Subst t

153fresh = unknown . Unknown <$> fresh'

173fresh = unknown . Unknown <$> fresh'

154

174

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

175+escapeCheckLater :: (Unifiable t) => t -> Subst ()

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

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

src/Language/PureScript/TypeChecker/Types.hs+242−260

@@ -12,7 +12,7 @@

12--

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

15−{-# LANGUAGE DeriveDataTypeable #-}

15+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts #-}

17module Language.PureScript.TypeChecker.Types (

18 typeOf

@@ -82,7 +82,7 @@ instance Unifiable Row where

82 forM_ int (uncurry (~~))

83 unifyRows sd1 r1' sd2 r2'

84 where

85− unifyRows :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Subst Check ()

85+ unifyRows :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Subst ()

86 unifyRows [] (RUnknown u) sd r = replace u (rowFromList (sd, r))

87 unifyRows sd r [] (RUnknown u) = replace u (rowFromList (sd, r))

88 unifyRows ns@((name, ty):row) r others u@(RUnknown un) = do

@@ -102,7 +102,7 @@ instance Unifiable Row where

102 unknowns (RCons _ ty r) = unknowns ty ++ unknowns r

103 unknowns _ = []

104

105−unifyTypes :: Type -> Type -> Subst Check ()

105+unifyTypes :: Type -> Type -> Subst ()

106unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 ++ " with type " ++ prettyPrintType t2 ++ ":\n" ++ e) $ do

107 unifyTypes' t1 t2

108 where

@@ -134,7 +134,7 @@ unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 +

134 ret1 `unifyTypes` ret2

135 unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()

136 unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do

137− modulePath <- checkModulePath `fmap` lift get

137+ modulePath <- checkModulePath `fmap` get

138 guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)

139 unifyTypes' (TypeApp t1 t2) (TypeApp t3 t4) = do

140 t1 `unifyTypes` t3

@@ -153,17 +153,19 @@ typeOf name val = do

153 Just ident | isFunction val ->

154 case val of

155 TypedValue val ty -> do

156− kind <- lift $ kindOf ty

156+ kind <- liftCheck $ kindOf ty

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

158− ty' <- lift $ replaceAllTypeSynonyms ty

158+ ty' <- replaceAllTypeSynonyms ty

159+ modulePath <- checkModulePath <$> get

159− check (M.singleton ident ty) val ty'

160+ bindNames (M.singleton (modulePath, ident) (ty, LocalVariable)) $ check val ty'

160 return ty'

161 return ty'

161 _ -> do

162 _ -> do

162 me <- fresh

163 me <- fresh

164+ modulePath <- checkModulePath <$> get

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

165+ ty <- bindNames (M.singleton (modulePath, ident) (me, LocalVariable)) $ infer val

164 ty ~~ me

166 ty ~~ me

165 return ty

167 return ty

166− _ -> infer M.empty val

168+ _ -> infer val

167 escapeCheck checks ty sub

169 escapeCheck checks ty sub

168 skolemEscapeCheck ty

170 skolemEscapeCheck ty

169 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty

171 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty

@@ -225,17 +227,17 @@ replaceRowVars name r = everywhere (mkT replace)

225 replace (RowVar v) | v == name = r

227 replace (RowVar v) | v == name = r

226 replace t = t

228 replace t = t

227

229

228−replaceAllVarsWithUnknowns :: Type -> Subst Check Type

230+replaceAllVarsWithUnknowns :: Type -> Subst Type

229replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns

231replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns

230replaceAllVarsWithUnknowns ty = return ty

232replaceAllVarsWithUnknowns ty = return ty

231

233

232−replaceVarWithUnknown :: String -> Type -> Subst Check Type

234+replaceVarWithUnknown :: String -> Type -> Subst Type

233replaceVarWithUnknown ident ty = do

235replaceVarWithUnknown ident ty = do

234 tu <- fresh

236 tu <- fresh

235 ru <- fresh

237 ru <- fresh

236 return $ replaceRowVars ident ru . replaceTypeVars ident tu $ ty

238 return $ replaceRowVars ident ru . replaceTypeVars ident tu $ ty

237

239

238−replaceAllTypeSynonyms :: (D.Data d) => d -> Check d

240+replaceAllTypeSynonyms :: (Functor m, MonadState CheckState m, MonadError String m) => (D.Data d) => d -> m d

239replaceAllTypeSynonyms d = do

241replaceAllTypeSynonyms d = do

240 env <- getEnv

242 env <- getEnv

241 let syns = map (\((path, name), (args, _)) -> (Qualified path name, length args)) . M.toList $ typeSynonyms env

243 let syns = map (\((path, name), (args, _)) -> (Qualified path name, length args)) . M.toList $ typeSynonyms env

@@ -247,61 +249,62 @@ desaturateAllTypeSynonyms = everywhere (mkT replace)

247 replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args

249 replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args

248 replace t = t

250 replace t = t

249

251

250−expandAllTypeSynonyms :: Type -> Subst Check Type

252+expandAllTypeSynonyms :: Type -> Subst Type

251expandAllTypeSynonyms (SaturatedTypeSynonym name args) = expandTypeSynonym name args >>= expandAllTypeSynonyms

253expandAllTypeSynonyms (SaturatedTypeSynonym name args) = expandTypeSynonym name args >>= expandAllTypeSynonyms

252expandAllTypeSynonyms ty = return ty

254expandAllTypeSynonyms ty = return ty

253

255

254−expandTypeSynonym :: Qualified ProperName -> [Type] -> Subst Check Type

256+expandTypeSynonym :: Qualified ProperName -> [Type] -> Subst Type

255expandTypeSynonym name args = do

257expandTypeSynonym name args = do

256− env <- lift getEnv

258+ env <- getEnv

257− modulePath <- checkModulePath `fmap` lift get

259+ modulePath <- checkModulePath `fmap` get

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

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

259 Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body

261 Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body

260 Nothing -> error "Type synonym was not defined"

262 Nothing -> error "Type synonym was not defined"

261

263

262−ensureNoDuplicateProperties :: [(String, Value)] -> Check ()

264+ensureNoDuplicateProperties :: (MonadError String m) => [(String, Value)] -> m ()

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

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

264

266

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

267+infer :: Value -> Subst Type

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

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

267− ty <- infer' m val

269+ ty <- infer' val

268 escapeCheckLater ty

270 escapeCheckLater ty

269 return ty

271 return ty

270

272

273+infer' :: Value -> Subst Type

271−infer' _ (NumericLiteral _) = return Number

274+infer' (NumericLiteral _) = return Number

272−infer' _ (StringLiteral _) = return String

275+infer' (StringLiteral _) = return String

273−infer' _ (BooleanLiteral _) = return Boolean

276+infer' (BooleanLiteral _) = return Boolean

274−infer' m (ArrayLiteral vals) = do

277+infer' (ArrayLiteral vals) = do

275− ts <- mapM (infer m) vals

278+ ts <- mapM (infer) vals

276 arr <- fresh

279 arr <- fresh

277 forM_ ts $ \t -> arr ~~ Array t

280 forM_ ts $ \t -> arr ~~ Array t

278 return arr

281 return arr

279−infer' m (Unary op val) = do

282+infer' (Unary op val) = do

280− t <- infer m val

283+ t <- infer val

281 inferUnary op t

284 inferUnary op t

282−infer' m (Binary op left right) = do

285+infer' (Binary op left right) = do

283− t1 <- infer m left

286+ t1 <- infer left

284− t2 <- infer m right

287+ t2 <- infer right

285 inferBinary op t1 t2

288 inferBinary op t1 t2

286−infer' m (ObjectLiteral ps) = do

289+infer' (ObjectLiteral ps) = do

287− lift $ ensureNoDuplicateProperties ps

290+ ensureNoDuplicateProperties ps

288− ts <- mapM (infer m . snd) ps

291+ ts <- mapM (infer . snd) ps

289 let fields = zipWith (\(name, _) t -> (name, t)) ps ts

292 let fields = zipWith (\(name, _) t -> (name, t)) ps ts

290 return $ Object $ rowFromList (fields, REmpty)

293 return $ Object $ rowFromList (fields, REmpty)

291−infer' m (ObjectUpdate o ps) = do

294+infer' (ObjectUpdate o ps) = do

292− lift $ ensureNoDuplicateProperties ps

295+ ensureNoDuplicateProperties ps

293 row <- fresh

296 row <- fresh

294− newTys <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer m . snd) ps

297+ newTys <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps

295 oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh

298 oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh

296− check m o $ Object $ rowFromList (oldTys, row)

299+ check o $ Object $ rowFromList (oldTys, row)

297 return $ Object $ rowFromList (newTys, row)

300 return $ Object $ rowFromList (newTys, row)

298−infer' m (Indexer index val) = do

301+infer' (Indexer index val) = do

299 el <- fresh

302 el <- fresh

300− check m index Number

303+ check index Number

301− check m val (Array el)

304+ check val (Array el)

302 return el

305 return el

303−infer' m (Accessor prop val) = do

306+infer' (Accessor prop val) = do

304− obj <- infer m val

307+ obj <- infer val

305 propTy <- inferProperty obj prop

308 propTy <- inferProperty obj prop

306 case propTy of

309 case propTy of

307 Nothing -> do

310 Nothing -> do

@@ -310,61 +313,53 @@ infer' m (Accessor prop val) = do

310 obj `subsumes` Object (RCons prop field rest)

313 obj `subsumes` Object (RCons prop field rest)

311 return field

314 return field

312 Just ty -> return ty

315 Just ty -> return ty

313−infer' m (Abs args ret) = do

316+infer' (Abs args ret) = do

314 ts <- replicateM (length args) fresh

317 ts <- replicateM (length args) fresh

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

318+ bindLocalVariables (zip args ts) $ do

316− body <- infer m' ret

319+ body <- infer' ret

317− return $ Function ts body

320+ return $ Function ts body

318−infer' m app@(App _ _) = do

321+infer' app@(App _ _) = do

319 let (f, argss) = unfoldApplication app

322 let (f, argss) = unfoldApplication app

320− ft <- infer m f

323+ ft <- infer f

321 ret <- fresh

324 ret <- fresh

322− checkFunctionApplications m ft argss ret

325+ checkFunctionApplications ft argss ret

323 return ret

326 return ret

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

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

325− case mp of

326− ModulePath [] ->

327− case M.lookup name m of

328− Just ty -> lift $ replaceAllTypeSynonyms ty

329− Nothing -> lookupGlobal

330− _ -> lookupGlobal

331− where

332− lookupGlobal = do

333− env <- lift getEnv

328+ env <- getEnv

334− modulePath <- checkModulePath `fmap` lift get

329+ modulePath <- checkModulePath `fmap` get

335− case M.lookup (qualify modulePath var) (names env) of

330+ case M.lookup (qualify modulePath var) (names env) of

336− Nothing -> throwError $ show var ++ " is undefined"

331+ Nothing -> throwError $ show var ++ " is undefined"

337− Just (ty, _) -> lift $ replaceAllTypeSynonyms ty

332+ Just (ty, _) -> replaceAllTypeSynonyms ty

338−infer' m (Block ss) = do

333+infer' (Block ss) = do

339 ret <- fresh

334 ret <- fresh

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

335+ (allCodePathsReturn, _) <- checkBlock M.empty ret ss

341 guardWith "Block is missing a return statement" allCodePathsReturn

336 guardWith "Block is missing a return statement" allCodePathsReturn

342 return ret

337 return ret

343−infer' m (Constructor c) = do

338+infer' (Constructor c) = do

344− env <- lift getEnv

339+ env <- getEnv

345− modulePath <- checkModulePath `fmap` lift get

340+ modulePath <- checkModulePath `fmap` get

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

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

347 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

342 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

348− Just ty -> lift $ replaceAllTypeSynonyms ty

343+ Just ty -> replaceAllTypeSynonyms ty

349−infer' m (Case val binders) = do

344+infer' (Case val binders) = do

350− t1 <- infer m val

345+ t1 <- infer val

351 ret <- fresh

346 ret <- fresh

352− checkBinders m t1 ret binders

347+ checkBinders t1 ret binders

353 return ret

348 return ret

354−infer' m (IfThenElse cond th el) = do

349+infer' (IfThenElse cond th el) = do

355− check m cond Boolean

350+ check cond Boolean

356− t2 <- infer m th

351+ t2 <- infer th

357− t3 <- infer m el

352+ t3 <- infer el

358 t2 ~~ t3

353 t2 ~~ t3

359 return t2

354 return t2

360−infer' m (TypedValue val ty) = do

355+infer' (TypedValue val ty) = do

361− kind <- lift $ kindOf ty

356+ kind <- liftCheck $ kindOf ty

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

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

363− ty' <- lift $ replaceAllTypeSynonyms ty

358+ ty' <- replaceAllTypeSynonyms ty

364− check m val ty'

359+ check val ty'

365 return ty'

360 return ty'

366

361

367−inferProperty :: Type -> String -> Subst Check (Maybe Type)

362+inferProperty :: Type -> String -> Subst (Maybe Type)

368inferProperty (Object row) prop = do

363inferProperty (Object row) prop = do

369 let (props, _) = rowToList row

364 let (props, _) = rowToList row

370 return $ lookup prop props

365 return $ lookup prop props

@@ -376,19 +371,19 @@ inferProperty (ForAll ident ty) prop = do

376 inferProperty replaced prop

371 inferProperty replaced prop

377inferProperty _ prop = return Nothing

372inferProperty _ prop = return Nothing

378

373

379−inferUnary :: UnaryOperator -> Type -> Subst Check Type

374+inferUnary :: UnaryOperator -> Type -> Subst Type

380inferUnary op val =

375inferUnary op val =

381 case fromMaybe (error "Invalid operator") $ lookup op unaryOps of

376 case fromMaybe (error "Invalid operator") $ lookup op unaryOps of

382 (valTy, resTy) -> do

377 (valTy, resTy) -> do

383 val ~~ valTy

378 val ~~ valTy

384 return resTy

379 return resTy

385

380

386−checkUnary :: M.Map Ident Type -> UnaryOperator -> Value -> Type -> Subst Check ()

381+checkUnary :: UnaryOperator -> Value -> Type -> Subst ()

387−checkUnary m op val res =

382+checkUnary op val res =

388 case fromMaybe (error "Invalid operator") $ lookup op unaryOps of

383 case fromMaybe (error "Invalid operator") $ lookup op unaryOps of

389 (valTy, resTy) -> do

384 (valTy, resTy) -> do

390 res ~~ resTy

385 res ~~ resTy

391− check m val valTy

386+ check val valTy

392

387

393unaryOps :: [(UnaryOperator, (Type, Type))]

388unaryOps :: [(UnaryOperator, (Type, Type))]

394unaryOps = [ (Negate, (Number, Number))

389unaryOps = [ (Negate, (Number, Number))

@@ -396,7 +391,7 @@ unaryOps = [ (Negate, (Number, Number))

396 , (BitwiseNot, (Number, Number))

391 , (BitwiseNot, (Number, Number))

397 ]

392 ]

398

393

399−inferBinary :: BinaryOperator -> Type -> Type -> Subst Check Type

394+inferBinary :: BinaryOperator -> Type -> Type -> Subst Type

400inferBinary op left right | isEqualityTest op = do

395inferBinary op left right | isEqualityTest op = do

401 left ~~ right

396 left ~~ right

402 return Boolean

397 return Boolean

@@ -407,18 +402,18 @@ inferBinary op left right =

407 right ~~ valTy

402 right ~~ valTy

408 return resTy

403 return resTy

409

404

410−checkBinary :: M.Map Ident Type -> BinaryOperator -> Value -> Value -> Type -> Subst Check ()

405+checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst ()

411−checkBinary m op left right res | isEqualityTest op = do

406+checkBinary op left right res | isEqualityTest op = do

412 res ~~ Boolean

407 res ~~ Boolean

413− t1 <- infer m left

408+ t1 <- infer left

414− t2 <- infer m right

409+ t2 <- infer right

415 t1 ~~ t2

410 t1 ~~ t2

416−checkBinary m op left right res =

411+checkBinary op left right res =

417 case fromMaybe (error "Invalid operator") $ lookup op binaryOps of

412 case fromMaybe (error "Invalid operator") $ lookup op binaryOps of

418 (valTy, resTy) -> do

413 (valTy, resTy) -> do

419 res ~~ resTy

414 res ~~ resTy

420− check m left valTy

415+ check left valTy

421− check m right valTy

416+ check right valTy

422

417

423isEqualityTest :: BinaryOperator -> Bool

418isEqualityTest :: BinaryOperator -> Bool

424isEqualityTest EqualTo = True

419isEqualityTest EqualTo = True

@@ -446,23 +441,23 @@ binaryOps = [ (Add, (Number, Number))

446 , (GreaterThanOrEqualTo, (Number, Boolean))

441 , (GreaterThanOrEqualTo, (Number, Boolean))

447 ]

442 ]

448

443

449−inferBinder :: Type -> Binder -> Subst Check (M.Map Ident Type)

444+inferBinder :: Type -> Binder -> Subst (M.Map Ident Type)

450inferBinder _ NullBinder = return M.empty

445inferBinder _ NullBinder = return M.empty

451inferBinder val (StringBinder _) = val ~~ String >> return M.empty

446inferBinder val (StringBinder _) = val ~~ String >> return M.empty

452inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty

447inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty

453inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty

448inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty

454inferBinder val (VarBinder name) = return $ M.singleton name val

449inferBinder val (VarBinder name) = return $ M.singleton name val

455inferBinder val (NullaryBinder ctor) = do

450inferBinder val (NullaryBinder ctor) = do

456− env <- lift getEnv

451+ env <- getEnv

457− modulePath <- checkModulePath `fmap` lift get

452+ modulePath <- checkModulePath <$> get

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

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

459 Just ty -> do

454 Just ty -> do

460 ty `subsumes` val

455 ty `subsumes` val

461 return M.empty

456 return M.empty

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

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

463inferBinder val (UnaryBinder ctor binder) = do

458inferBinder val (UnaryBinder ctor binder) = do

464− env <- lift getEnv

459+ env <- getEnv

465− modulePath <- checkModulePath `fmap` lift get

460+ modulePath <- checkModulePath <$> get

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

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

467 Just ty -> do

462 Just ty -> do

468 Function [obj] ret <- replaceAllVarsWithUnknowns ty

463 Function [obj] ret <- replaceAllVarsWithUnknowns ty

@@ -476,7 +471,7 @@ inferBinder val (ObjectBinder props) = do

476 val ~~ Object row

471 val ~~ Object row

477 return m1

472 return m1

478 where

473 where

479− inferRowProperties :: Row -> Row -> [(String, Binder)] -> Subst Check (M.Map Ident Type)

474+ inferRowProperties :: Row -> Row -> [(String, Binder)] -> Subst (M.Map Ident Type)

480 inferRowProperties nrow row [] = nrow ~~ row >> return M.empty

475 inferRowProperties nrow row [] = nrow ~~ row >> return M.empty

481 inferRowProperties nrow row ((name, binder):binders) = do

476 inferRowProperties nrow row ((name, binder):binders) = do

482 propTy <- fresh

477 propTy <- fresh

@@ -496,97 +491,95 @@ inferBinder val (NamedBinder name binder) = do

496 m <- inferBinder val binder

491 m <- inferBinder val binder

497 return $ M.insert name val m

492 return $ M.insert name val m

498

493

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

494+inferGuardedBinder :: Type -> Binder -> Subst (M.Map Ident Type)

500−inferGuardedBinder m val (GuardedBinder cond binder) = do

495+inferGuardedBinder val (GuardedBinder cond binder) = do

501 m1 <- inferBinder val binder

496 m1 <- inferBinder val binder

502− check (m1 `M.union` m) cond Boolean

497+ bindLocalVariables (M.toList m1) $ check cond Boolean

503 return m1

498 return m1

504−inferGuardedBinder m val b = inferBinder val b

499+inferGuardedBinder val b = inferBinder val b

505−

500+

506−checkBinders :: M.Map Ident Type -> Type -> Type -> [(Binder, Value)] -> Subst Check ()

501+checkBinders :: Type -> Type -> [(Binder, Value)] -> Subst ()

507−checkBinders _ _ _ [] = return ()

502+checkBinders _ _ [] = return ()

508−checkBinders m nval ret ((binder, val):bs) = do

503+checkBinders nval ret ((binder, val):bs) = do

509− m1 <- inferGuardedBinder m nval binder

504+ m1 <- inferGuardedBinder nval binder

510− check (m1 `M.union` m) val ret

505+ bindLocalVariables (M.toList m1) $ check val ret

511− checkBinders m nval ret bs

506+ checkBinders nval ret bs

512−

507+

513−assignVariable :: Ident -> M.Map Ident Type -> Subst Check ()

508+assignVariable :: Ident -> Subst ()

514−assignVariable name m =

509+assignVariable name = do

510+ env <- checkEnv <$> get

511+ modulePath <- checkModulePath <$> get

515− case M.lookup name m of

512+ case M.lookup (modulePath, name) (names env) of

516− Nothing -> return ()

517− Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."

513+ Just (_, LocalVariable) -> throwError $ "Variable with name " ++ show name ++ " already exists."

518−

514+ _ -> return ()

515+

519−checkStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> Statement -> Subst Check (Bool, M.Map Ident Type)

516+checkStatement :: M.Map Ident Type -> Type -> Statement -> Subst (Bool, M.Map Ident Type)

520−checkStatement m mass ret (VariableIntroduction name val) = do

517+checkStatement mass ret (VariableIntroduction name val) = do

521− assignVariable name (m `M.union` mass)

518+ assignVariable name

522− t <- infer m val

519+ t <- infer val

523 return (False, M.insert name t mass)

520 return (False, M.insert name t mass)

524−checkStatement m mass ret (Assignment ident val) = do

521+checkStatement mass ret (Assignment ident val) = do

525− t <- infer m val

522+ t <- infer val

526 case M.lookup ident mass of

523 case M.lookup ident mass of

527 Nothing -> throwError $ "No local variable with name " ++ show ident

524 Nothing -> throwError $ "No local variable with name " ++ show ident

528 Just ty -> do t ~~ ty

525 Just ty -> do t ~~ ty

529 return (False, mass)

526 return (False, mass)

530−checkStatement m mass ret (While val inner) = do

527+checkStatement mass ret (While val inner) = do

531− check m val Boolean

528+ check val Boolean

532− (allCodePathsReturn, _) <- checkBlock m mass ret inner

529+ (allCodePathsReturn, _) <- checkBlock mass ret inner

533 return (allCodePathsReturn, mass)

530 return (allCodePathsReturn, mass)

534−checkStatement m mass ret (If ifst) = do

531+checkStatement mass ret (If ifst) = do

535− allCodePathsReturn <- checkIfStatement m mass ret ifst

532+ allCodePathsReturn <- checkIfStatement mass ret ifst

536 return (allCodePathsReturn, mass)

533 return (allCodePathsReturn, mass)

537−checkStatement m mass ret (For ident start end inner) = do

534+checkStatement mass ret (For ident start end inner) = do

538− assignVariable ident (m `M.union` mass)

535+ assignVariable ident

539− check (m `M.union` mass) start Number

536+ check start Number

540− check (m `M.union` mass) end Number

537+ check end Number

541− let mass1 = M.insert ident Number mass

542− (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner

538+ (allCodePathsReturn, _) <- bindLocalVariables [(ident, Number)] $ checkBlock mass ret inner

543 return (allCodePathsReturn, mass)

539 return (allCodePathsReturn, mass)

544−checkStatement m mass ret (ForEach ident vals inner) = do

540+checkStatement mass ret (ForEach ident vals inner) = do

545− assignVariable ident (m `M.union` mass)

541+ assignVariable ident

546 val <- fresh

542 val <- fresh

547− check (m `M.union` mass) vals (Array val)

543+ check vals (Array val)

548− let mass1 = M.insert ident val mass

549− (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner

544+ (allCodePathsReturn, _) <- bindLocalVariables [(ident, val)] $ checkBlock mass ret inner

550 guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn

545 guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn

551 return (False, mass)

546 return (False, mass)

552−checkStatement m mass ret (Return val) = do

547+checkStatement mass ret (Return val) = do

553− check (m `M.union` mass) val ret

548+ check val ret

554 return (True, mass)

549 return (True, mass)

555

550

556−checkIfStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> IfStatement -> Subst Check Bool

551+checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> Subst Bool

557−checkIfStatement m mass ret (IfStatement val thens Nothing) = do

552+checkIfStatement mass ret (IfStatement val thens Nothing) = do

558− check m val Boolean

553+ check val Boolean

559− _ <- checkBlock m mass ret thens

554+ _ <- checkBlock mass ret thens

560 return False

555 return False

561−checkIfStatement m mass ret (IfStatement val thens (Just elses)) = do

556+checkIfStatement mass ret (IfStatement val thens (Just elses)) = do

562− check m val Boolean

557+ check val Boolean

563− (allCodePathsReturn1, _) <- checkBlock m mass ret thens

558+ (allCodePathsReturn1, _) <- checkBlock mass ret thens

564− allCodePathsReturn2 <- checkElseStatement m mass ret elses

559+ allCodePathsReturn2 <- checkElseStatement mass ret elses

565 return $ allCodePathsReturn1 && allCodePathsReturn2

560 return $ allCodePathsReturn1 && allCodePathsReturn2

566

561

567−checkElseStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> ElseStatement -> Subst Check Bool

562+checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> Subst Bool

568−checkElseStatement m mass ret (Else elses) = fst <$> checkBlock m mass ret elses

563+checkElseStatement mass ret (Else elses) = fst <$> checkBlock mass ret elses

569−checkElseStatement m mass ret (ElseIf ifst) = checkIfStatement m mass ret ifst

564+checkElseStatement mass ret (ElseIf ifst) = checkIfStatement mass ret ifst

570

565

571−checkBlock :: M.Map Ident Type -> M.Map Ident Type -> Type -> [Statement] -> Subst Check (Bool, M.Map Ident Type)

566+checkBlock :: M.Map Ident Type -> Type -> [Statement] -> Subst (Bool, M.Map Ident Type)

572−checkBlock _ mass _ [] = return (False, mass)

567+checkBlock mass _ [] = return (False, mass)

573−checkBlock m mass ret (s:ss) = do

568+checkBlock mass ret (s:ss) = do

574− (b1, mass1) <- checkStatement (m `M.union` mass) mass ret s

569+ (b1, mass1) <- checkStatement mass ret s

575− case (b1, ss) of

570+ bindLocalVariables (M.toList mass1) $ case (b1, ss) of

576 (True, []) -> return (True, mass1)

571 (True, []) -> return (True, mass1)

577 (True, _) -> throwError "Unreachable code"

572 (True, _) -> throwError "Unreachable code"

578− (False, ss) -> do

579− (b2, mass2) <- checkBlock m mass1 ret ss

573+ (False, ss) -> checkBlock mass1 ret ss

580− return (b2, mass2)

581

574

582−skolemize :: String -> Type -> Subst Check Type

575+skolemize :: String -> Type -> Subst Type

583skolemize ident ty = do

576skolemize ident ty = do

584 tsk <- Skolem <$> fresh'

577 tsk <- Skolem <$> fresh'

585 rsk <- RSkolem <$> fresh'

578 rsk <- RSkolem <$> fresh'

586 return $ replaceRowVars ident rsk $ replaceTypeVars ident tsk ty

579 return $ replaceRowVars ident rsk $ replaceTypeVars ident tsk ty

587

580

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

581+check :: Value -> Type -> Subst ()

589−check m val ty = rethrow errorMessage $ check' m val ty

582+check val ty = rethrow errorMessage $ check' val ty

590 where

583 where

591 errorMessage msg =

584 errorMessage msg =

592 "Error checking type of term " ++

585 "Error checking type of term " ++

@@ -596,92 +589,81 @@ check m val ty = rethrow errorMessage $ check' m val ty

596 ":\n" ++

589 ":\n" ++

597 msg

590 msg

598

591

599−check' :: M.Map Ident Type -> Value -> Type -> Subst Check ()

592+check' :: Value -> Type -> Subst ()

600−check' m val (ForAll idents ty) = do

593+check' val (ForAll idents ty) = do

601 sk <- skolemize idents ty

594 sk <- skolemize idents ty

602− check m val sk

595+ check val sk

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

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

604− ty <- infer m val

597+ ty <- infer val

605 -- Don't unify an unknown with an inferred polytype

598 -- Don't unify an unknown with an inferred polytype

606 ty' <- replaceAllVarsWithUnknowns ty

599 ty' <- replaceAllVarsWithUnknowns ty

607 ty' ~~ u

600 ty' ~~ u

608−check' m (NumericLiteral _) Number = return ()

601+check' (NumericLiteral _) Number = return ()

609−check' m (StringLiteral _) String = return ()

602+check' (StringLiteral _) String = return ()

610−check' m (BooleanLiteral _) Boolean = return ()

603+check' (BooleanLiteral _) Boolean = return ()

611−check' m (Unary op val) ty = checkUnary m op val ty

604+check' (Unary op val) ty = checkUnary op val ty

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

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

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

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

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

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

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

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

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

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

617− let bindings = M.fromList (zip args argTys)

610+ bindLocalVariables (zip args argTys) $ check ret retTy

618− check (bindings `M.union` m) ret retTy

619−check' m app@(App _ _) ret = do

611+check' app@(App _ _) ret = do

620 let (f, argss) = unfoldApplication app

612 let (f, argss) = unfoldApplication app

621− ft <- infer m f

613+ ft <- infer f

622− checkFunctionApplications m ft argss ret

614+ checkFunctionApplications ft argss ret

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

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

624− case mp of

625− ModulePath [] ->

626− case M.lookup name m of

627− Just ty1 -> do

628− repl <- lift $ replaceAllTypeSynonyms ty1

629− repl `subsumes` ty

630− Nothing -> lookupGlobal

631− _ -> lookupGlobal

632− where

633− lookupGlobal = do

634− env <- lift getEnv

616+ env <- getEnv

635− modulePath <- checkModulePath `fmap` lift get

617+ modulePath <- checkModulePath <$> get

636− case M.lookup (qualify modulePath var) (names env) of

618+ case M.lookup (qualify modulePath var) (names env) of

637− Nothing -> throwError $ show var ++ " is undefined"

619+ Nothing -> throwError $ show var ++ " is undefined"

638− Just (ty1, _) -> do

620+ Just (ty1, _) -> do

639− repl <- lift $ replaceAllTypeSynonyms ty1

621+ repl <- replaceAllTypeSynonyms ty1

640− repl `subsumes` ty

622+ repl `subsumes` ty

641−check' m (TypedValue val ty1) ty2 = do

623+check' (TypedValue val ty1) ty2 = do

642− kind <- lift $ kindOf ty1

624+ kind <- liftCheck $ kindOf ty1

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

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

644 ty1 `subsumes` ty2

626 ty1 `subsumes` ty2

645− check m val ty1

627+ check val ty1

646−check' m (Case val binders) ret = do

628+check' (Case val binders) ret = do

647− t1 <- infer m val

629+ t1 <- infer val

648− checkBinders m t1 ret binders

630+ checkBinders t1 ret binders

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

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

650− check m cond Boolean

632+ check cond Boolean

651− check m th ty

633+ check th ty

652− check m el ty

634+ check el ty

653−check' m (ObjectLiteral ps) (Object row) = do

635+check' (ObjectLiteral ps) (Object row) = do

654− lift $ ensureNoDuplicateProperties ps

636+ ensureNoDuplicateProperties ps

655− checkProperties m ps row False

637+ checkProperties ps row False

656−check' m (ObjectUpdate obj ps) (Object row) = do

638+check' (ObjectUpdate obj ps) (Object row) = do

657− lift $ ensureNoDuplicateProperties ps

639+ ensureNoDuplicateProperties ps

658 us <- zip (map fst ps) <$> replicateM (length ps) fresh

640 us <- zip (map fst ps) <$> replicateM (length ps) fresh

659 let (propsToCheck, rest) = rowToList row

641 let (propsToCheck, rest) = rowToList row

660 propsToRemove = map fst ps

642 propsToRemove = map fst ps

661 remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck

643 remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck

662− check m obj (Object (rowFromList (us ++ remainingProps, rest)))

644+ check obj (Object (rowFromList (us ++ remainingProps, rest)))

663− checkProperties m ps row True

645+ checkProperties ps row True

664−check' m (Accessor prop val) ty = do

646+check' (Accessor prop val) ty = do

665 rest <- fresh

647 rest <- fresh

666− check m val (Object (RCons prop ty rest))

648+ check val (Object (RCons prop ty rest))

667−check' m (Block ss) ret = do

649+check' (Block ss) ret = do

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

650+ (allCodePathsReturn, _) <- checkBlock M.empty ret ss

669 guardWith "Block is missing a return statement" allCodePathsReturn

651 guardWith "Block is missing a return statement" allCodePathsReturn

670−check' m (Constructor c) ty = do

652+check' (Constructor c) ty = do

671− env <- lift getEnv

653+ env <- getEnv

672− modulePath <- checkModulePath `fmap` lift get

654+ modulePath <- checkModulePath <$> get

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

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

674 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

656 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

675 Just ty1 -> do

657 Just ty1 -> do

676− repl <- lift $ replaceAllTypeSynonyms ty1

658+ repl <- replaceAllTypeSynonyms ty1

677 repl `subsumes` ty

659 repl `subsumes` ty

678−check' m val (SaturatedTypeSynonym name args) = do

660+check' val (SaturatedTypeSynonym name args) = do

679 ty <- expandTypeSynonym name args

661 ty <- expandTypeSynonym name args

680− check m val ty

662+ check val ty

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

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

682

664

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

665+checkProperties :: [(String, Value)] -> Row -> Bool -> Subst ()

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

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

685 go [] [] REmpty = return ()

667 go [] [] REmpty = return ()

686 go [] [] u@(RUnknown _) = u ~~ REmpty

668 go [] [] u@(RUnknown _) = u ~~ REmpty

687 go [] [] (RSkolem _) | lax = return ()

669 go [] [] (RSkolem _) | lax = return ()

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

689 | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p

671 | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p

690 go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row

672 go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row

691 go ((p,v):ps) [] u@(RUnknown _) = do

673 go ((p,v):ps) [] u@(RUnknown _) = do

692− ty <- infer m v

674+ ty <- infer v

693 rest <- fresh

675 rest <- fresh

694 u ~~ RCons p ty rest

676 u ~~ RCons p ty rest

695 go ps [] rest

677 go ps [] rest

696 go ((p,v):ps) ts r =

678 go ((p,v):ps) ts r =

697 case lookup p ts of

679 case lookup p ts of

698 Nothing -> do

680 Nothing -> do

699− ty <- infer m v

681+ ty <- infer v

700 rest <- fresh

682 rest <- fresh

701 r ~~ RCons p ty rest

683 r ~~ RCons p ty rest

702 go ps ts rest

684 go ps ts rest

703 Just ty -> do

685 Just ty -> do

704− check m v ty

686+ check v ty

705 go ps (delete (p, ty) ts) r

687 go ps (delete (p, ty) ts) r

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

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

707

689

@@ -711,16 +693,16 @@ unfoldApplication = go []

711 go argss (App f args) = go (args:argss) f

693 go argss (App f args) = go (args:argss) f

712 go argss f = (f, argss)

694 go argss f = (f, argss)

713

695

714−checkFunctionApplications :: M.Map Ident Type -> Type -> [[Value]] -> Type -> Subst Check ()

696+checkFunctionApplications :: Type -> [[Value]] -> Type -> Subst ()

715−checkFunctionApplications _ _ [] _ = error "Nullary function application"

697+checkFunctionApplications _ [] _ = error "Nullary function application"

716−checkFunctionApplications m fnTy [args] ret = checkFunctionApplication m fnTy args ret

698+checkFunctionApplications fnTy [args] ret = checkFunctionApplication fnTy args ret

717−checkFunctionApplications m fnTy (args:argss) ret = do

699+checkFunctionApplications fnTy (args:argss) ret = do

718− argTys <- mapM (infer m) args

700+ argTys <- mapM (infer) args

719− f <- inferFunctionApplication m fnTy argTys

701+ f <- inferFunctionApplication fnTy argTys

720− checkFunctionApplications m f argss ret

702+ checkFunctionApplications f argss ret

721

703

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

704+checkFunctionApplication :: Type -> [Value] -> Type -> Subst ()

723−checkFunctionApplication m fnTy args ret = rethrow errorMessage $ checkFunctionApplication' m fnTy args ret

705+checkFunctionApplication fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fnTy args ret

724 where

706 where

725 errorMessage msg = "Error applying function of type "

707 errorMessage msg = "Error applying function of type "

726 ++ prettyPrintType fnTy

708 ++ prettyPrintType fnTy

@@ -728,46 +710,46 @@ checkFunctionApplication m fnTy args ret = rethrow errorMessage $ checkFunctionA

728 ++ ", expecting value of type "

710 ++ ", expecting value of type "

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

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

730

712

731−inferFunctionApplication :: M.Map Ident Type -> Type -> [Type] -> Subst Check Type

713+inferFunctionApplication :: Type -> [Type] -> Subst Type

732−inferFunctionApplication m (Function argTys retTy) args = do

714+inferFunctionApplication (Function argTys retTy) args = do

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

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

734 zipWithM subsumes args argTys

716 zipWithM subsumes args argTys

735 return retTy

717 return retTy

736−inferFunctionApplication m (ForAll ident ty) args = do

718+inferFunctionApplication (ForAll ident ty) args = do

737 replaced <- replaceVarWithUnknown ident ty

719 replaced <- replaceVarWithUnknown ident ty

738− inferFunctionApplication m replaced args

720+ inferFunctionApplication replaced args

739−inferFunctionApplication m u@(TUnknown _) args = do

721+inferFunctionApplication u@(TUnknown _) args = do

740 ret <- fresh

722 ret <- fresh

741 args' <- mapM replaceAllVarsWithUnknowns args

723 args' <- mapM replaceAllVarsWithUnknowns args

742 u ~~ Function args' ret

724 u ~~ Function args' ret

743 return ret

725 return ret

744−inferFunctionApplication m (SaturatedTypeSynonym name tyArgs) args = do

726+inferFunctionApplication (SaturatedTypeSynonym name tyArgs) args = do

745 ty <- expandTypeSynonym name tyArgs

727 ty <- expandTypeSynonym name tyArgs

746− inferFunctionApplication m ty args

728+ inferFunctionApplication ty args

747−inferFunctionApplication _ fnTy args = throwError $ "Cannot apply function of type "

729+inferFunctionApplication fnTy args = throwError $ "Cannot apply function of type "

748 ++ prettyPrintType fnTy

730 ++ prettyPrintType fnTy

749 ++ " to argument(s) of type(s) " ++ intercalate ", " (map prettyPrintType args)

731 ++ " to argument(s) of type(s) " ++ intercalate ", " (map prettyPrintType args)

750

732

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

733+checkFunctionApplication' :: Type -> [Value] -> Type -> Subst ()

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

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

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

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

754− zipWithM (check m) args argTys

736+ zipWithM (check) args argTys

755 retTy `subsumes` ret

737 retTy `subsumes` ret

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

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

757 replaced <- replaceVarWithUnknown ident ty

739 replaced <- replaceVarWithUnknown ident ty

758− checkFunctionApplication m replaced args ret

740+ checkFunctionApplication replaced args ret

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

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

760− tyArgs <- mapM (\arg -> infer m arg >>= replaceAllVarsWithUnknowns) args

742+ tyArgs <- mapM (\arg -> infer arg >>= replaceAllVarsWithUnknowns) args

761 u ~~ Function tyArgs ret

743 u ~~ Function tyArgs ret

762−checkFunctionApplication' m (SaturatedTypeSynonym name tyArgs) args ret = do

744+checkFunctionApplication' (SaturatedTypeSynonym name tyArgs) args ret = do

763 ty <- expandTypeSynonym name tyArgs

745 ty <- expandTypeSynonym name tyArgs

764− checkFunctionApplication' m ty args ret

746+ checkFunctionApplication' ty args ret

765−checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of type "

747+checkFunctionApplication' fnTy args ret = throwError $ "Applying a function of type "

766 ++ prettyPrintType fnTy

748 ++ prettyPrintType fnTy

767 ++ " to argument(s) " ++ intercalate ", " (map prettyPrintValue args)

749 ++ " to argument(s) " ++ intercalate ", " (map prettyPrintValue args)

768 ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."

750 ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."

769

751

770−subsumes :: Type -> Type -> Subst Check ()

752+subsumes :: Type -> Type -> Subst ()

771subsumes (ForAll ident ty1) ty2 = do

753subsumes (ForAll ident ty1) ty2 = do

772 replaced <- replaceVarWithUnknown ident ty1

754 replaced <- replaceVarWithUnknown ident ty1

773 replaced `subsumes` ty2

755 replaced `subsumes` ty2

tests/Main.hs+3−2

@@ -58,13 +58,14 @@ assertDoesNotCompile inputFile = do

58main :: IO ()

59main = do

60 cd <- getCurrentDirectory

61+ putStrLn $ cd

61 let examples = cd ++ pathSeparator : "examples"

62 let examples = cd ++ pathSeparator : "examples"

62 let passing = examples ++ pathSeparator : "passing"

63 let passing = examples ++ pathSeparator : "passing"

63 passingTestCases <- getDirectoryContents passing

64 passingTestCases <- getDirectoryContents passing

64− forM_ passingTestCases $ \inputFile -> when (".ps" `isSuffixOf` inputFile) $

65+ forM_ passingTestCases $ \inputFile -> when (".purs" `isSuffixOf` inputFile) $

65 assertCompiles (passing ++ pathSeparator : inputFile)

66 assertCompiles (passing ++ pathSeparator : inputFile)

66 let failing = examples ++ pathSeparator : "failing"

67 let failing = examples ++ pathSeparator : "failing"

67 failingTestCases <- getDirectoryContents failing

68 failingTestCases <- getDirectoryContents failing

68− forM_ failingTestCases $ \inputFile -> when (".ps" `isSuffixOf` inputFile) $

69+ forM_ failingTestCases $ \inputFile -> when (".purs" `isSuffixOf` inputFile) $

69 assertDoesNotCompile (failing ++ pathSeparator : inputFile)

70 assertDoesNotCompile (failing ++ pathSeparator : inputFile)

70 exitSuccess

71 exitSuccess