0fde5e0 · rowtype-yoga/purescript-native

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

on golang help sign in

Fully type the provided value in infer and check. Need to fix the escape check.

0fde5e0Phil Freeman13 years ago

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

compare with golang

unifiedsplit

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

58 unknowns _ = []

60kindOf :: ModuleName -> Type -> Check Kind

61−kindOf moduleName ty = fmap (\(k, _, _) -> k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty

61+kindOf moduleName ty = fmap (\(k, _) -> k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty

63kindsOf :: ModuleName -> ProperName -> [String] -> [Type] -> Check Kind

64−kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . runSubst (SubstContext moduleName) $ do

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

65 tyCon <- fresh

66 kargs <- replicateM (length args) fresh

67 let dict = (name, tyCon) : zip (map ProperName args) kargs

@@ -69,7 +69,7 @@ kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . run

69 solveTypes ts kargs tyCon

71kindsOfAll :: ModuleName -> [(ProperName, [String], [Type])] -> Check [Kind]

72−kindsOfAll moduleName tys = fmap (map starIfUnknown . (\(ks, _, _) -> ks)) . runSubst (SubstContext moduleName) $ do

72+kindsOfAll moduleName tys = fmap (map starIfUnknown . (\(ks, _) -> ks)) . runSubst (SubstContext moduleName) $ do

73 tyCons <- replicateM (length tys) fresh

74 let dict = zipWith (\(name, _, _) tyCon -> (name, tyCon)) tys tyCons

75 bindLocalTypeVariables moduleName dict $

src/Language/PureScript/TypeChecker/Monad.hs+4−11

@@ -106,9 +106,6 @@ canonicalizeType mn env (Qualified Nothing nm) = case (mn, nm) `M.lookup` types

106 Just (_, DataAlias mn' pn') -> (mn', pn')

107 _ -> (mn, nm)

108

109−data AnyUnifiable where

110− AnyUnifiable :: forall t. (Unifiable t) => t -> AnyUnifiable

111−

112data CheckState = CheckState { checkEnv :: Environment

109data CheckState = CheckState { checkEnv :: Environment

113 , checkNextVar :: Int

110 , checkNextVar :: Int

114 }

111 }

@@ -143,8 +140,7 @@ instance Monoid Substitution where

143 mempty = Substitution unknown

140 mempty = Substitution unknown

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

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

145

142

146−data SubstState = SubstState { substSubst :: Substitution

143+data SubstState = SubstState { substSubst :: Substitution }

147− , substFutureEscapeChecks :: [AnyUnifiable] }

148

144

149newtype SubstContext = SubstContext { substCurrentModule :: ModuleName } deriving (Show)

145newtype SubstContext = SubstContext { substCurrentModule :: ModuleName } deriving (Show)

150

146

@@ -160,10 +156,10 @@ deriving instance MonadError String Subst

160liftCheck :: Check a -> Subst a

156liftCheck :: Check a -> Subst a

161liftCheck = Subst . lift . lift

157liftCheck = Subst . lift . lift

162

158

163−runSubst :: (Unifiable a) => SubstContext -> Subst a -> Check (a, Substitution, [AnyUnifiable])

159+runSubst :: (Unifiable a) => SubstContext -> Subst a -> Check (a, Substitution)

164runSubst context subst = do

160runSubst context subst = do

165− (a, s) <- flip runStateT (SubstState mempty []) . flip runReaderT context . unSubst $ subst

161+ (a, s) <- flip runStateT (SubstState mempty) . flip runReaderT context . unSubst $ subst

166− return (apply (substSubst s) a, substSubst s, substFutureEscapeChecks s)

162+ return (apply (substSubst s) a, substSubst s)

167

163

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

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

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

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

@@ -215,6 +211,3 @@ fresh' = do

215

211

216fresh :: (Unifiable t) => Subst t

212fresh :: (Unifiable t) => Subst t

217fresh = unknown . Unknown <$> fresh'

213fresh = unknown . Unknown <$> fresh'

218−

219−escapeCheckLater :: (Unifiable t) => t -> Subst ()

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

src/Language/PureScript/TypeChecker/Types.hs+173−161

@@ -143,7 +143,7 @@ typeConstructorsAreEqual env moduleName = (==) `on` canonicalizeType moduleName

143

144typesOf :: ModuleName -> [(Ident, Value)] -> Check [Type]

145typesOf moduleName vals = do

146− (tys, sub, checks) <- runSubst (SubstContext moduleName) $ do

146+ (tys, sub) <- runSubst (SubstContext moduleName) $ do

147 let es = map isTyped vals

148 typed = filter (isJust . snd . snd) es

149 untyped = filter (isNothing . snd . snd) es

@@ -160,7 +160,7 @@ typesOf moduleName vals = do

160 bindNames dict $ check val ty'

161 return ty'

162 (ident, (val, Nothing)) -> do

163− ty <- bindNames dict $ infer val

163+ TypedValue _ ty <- bindNames dict $ infer val

164 ty ~~ fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)

165 return ty

166 when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do

@@ -168,7 +168,7 @@ typesOf moduleName vals = do

168 ty ~~ TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a

169 return ty

170 return tys

171− forM tys $ flip (escapeCheck checks) sub

171+ --forM tys $ flip (escapeCheck checks) sub

172 forM tys $ skolemEscapeCheck

173 return $ map (varIfUnknown . desaturateAllTypeSynonyms . setifyAll) tys

174

@@ -176,7 +176,7 @@ isTyped :: (Ident, Value) -> (Ident, (Value, Maybe Type))

176isTyped (name, TypedValue value ty) = (name, (value, Just ty))

177isTyped (name, value) = (name, (value, Nothing))

178

179−escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()

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

180escapeCheck checks ty sub =

181 let

182 visibleUnknowns = nub $ unknowns ty

@@ -185,6 +185,7 @@ escapeCheck checks ty sub =

185 AnyUnifiable t -> do

186 let unsolvedUnknowns = nub . unknowns $ apply sub t

187 guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns

188+-}

188

189

189skolemEscapeCheck :: Type -> Check ()

190skolemEscapeCheck :: Type -> Check ()

190skolemEscapeCheck ty =

191skolemEscapeCheck ty =

@@ -247,100 +248,99 @@ expandTypeSynonym name args = do

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

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

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

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

249

250

250−infer :: Value -> Subst Type

251+infer :: Value -> Subst Value

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

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

252− ty <- infer' val

253− escapeCheckLater ty

254− return ty

255

253

256−infer' :: Value -> Subst Type

254+infer' :: Value -> Subst Value

257−infer' (NumericLiteral _) = return Number

255+infer' v@(NumericLiteral _) = return $ TypedValue v Number

258−infer' (StringLiteral _) = return String

256+infer' v@(StringLiteral _) = return $ TypedValue v String

259−infer' (BooleanLiteral _) = return Boolean

257+infer' v@(BooleanLiteral _) = return $ TypedValue v Boolean

260infer' (ArrayLiteral vals) = do

258infer' (ArrayLiteral vals) = do

261− ts <- mapM (infer) vals

259+ ts <- mapM infer vals

262 els <- fresh

260 els <- fresh

263− forM_ ts $ \t -> els ~~ Array t

261+ forM_ ts $ \(TypedValue _ t) -> els ~~ Array t

264− return els

262+ return $ TypedValue (ArrayLiteral ts) els

265infer' (Unary op val) = do

263infer' (Unary op val) = do

266− t <- infer val

264+ v <- infer val

267− inferUnary op t

265+ inferUnary op v

268infer' (Binary op left right) = do

266infer' (Binary op left right) = do

269− t1 <- infer left

267+ v1 <- infer left

270− t2 <- infer right

268+ v2 <- infer right

271− inferBinary op t1 t2

269+ inferBinary op v1 v2

272infer' (ObjectLiteral ps) = do

270infer' (ObjectLiteral ps) = do

273 ensureNoDuplicateProperties ps

271 ensureNoDuplicateProperties ps

274 ts <- mapM (infer . snd) ps

272 ts <- mapM (infer . snd) ps

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

273+ let fields = zipWith (\name (TypedValue _ t) -> (name, t)) (map fst ps) ts

276− return $ Object $ rowFromList (fields, REmpty)

274+ ty = Object $ rowFromList (fields, REmpty)

275+ return $ TypedValue (ObjectLiteral (zip (map fst ps) ts)) ty

277infer' (ObjectUpdate o ps) = do

276infer' (ObjectUpdate o ps) = do

278 ensureNoDuplicateProperties ps

277 ensureNoDuplicateProperties ps

279 row <- fresh

278 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

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

282− check o $ Object $ rowFromList (oldTys, row)

282+ o' <- check o $ Object $ rowFromList (oldTys, row)

283− return $ Object $ rowFromList (newTys, row)

283+ return $ TypedValue (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)

284infer' (Indexer index val) = do

285 el <- fresh

286 check index Number

287 check val (Array el)

288− return el

288+ return $ TypedValue (Indexer (TypedValue index Number) (TypedValue val (Array el))) el

289infer' (Accessor prop val) = do

290− obj <- infer val

290+ typed@(TypedValue _ objTy) <- infer val

291− propTy <- inferProperty obj prop

291+ propTy <- inferProperty objTy prop

292 case propTy of

293 Nothing -> do

294 field <- fresh

295 rest <- fresh

296− obj `subsumes` Object (RCons prop field rest)

296+ objTy `subsumes` Object (RCons prop field rest)

297− return field

297+ return $ TypedValue (Accessor prop typed) field

298− Just ty -> return ty

298+ Just ty -> return $ TypedValue (Accessor prop typed) ty

299infer' (Abs args ret) = do

300 ts <- replicateM (length args) fresh

301 moduleName <- substCurrentModule <$> ask

302 bindLocalVariables moduleName (zip args ts) $ do

303− body <- infer' ret

303+ (TypedValue body bodyTy) <- infer' ret

304− return $ Function ts body

304+ return $ TypedValue (Abs args body) $ Function ts bodyTy

305−infer' app@(App _ _) = do

305+infer' (App f args) = do

306− let (f, argss) = unfoldApplication app

307− ft <- infer f

306+ (TypedValue f' ft) <- infer f

308 ret <- fresh

307 ret <- fresh

309− checkFunctionApplications ft argss ret

308+ args' <- checkFunctionApplication ft args ret

310− return ret

309+ return $ TypedValue (App f' args') ret

311infer' (Var var) = do

310infer' (Var var) = do

312 moduleName <- substCurrentModule <$> ask

311 moduleName <- substCurrentModule <$> ask

313 ty <- lookupVariable moduleName var

312 ty <- lookupVariable moduleName var

314− replaceAllTypeSynonyms ty

313+ ty' <- replaceAllTypeSynonyms ty

314+ return $ TypedValue (Var var) ty'

315infer' (Block ss) = do

316 ret <- fresh

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

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

318 guardWith "Block is missing a return statement" allCodePathsReturn

319− return ret

319+ return $ TypedValue (Block ss') ret

320−infer' (Constructor c) = do

320+infer' v@(Constructor c) = do

321 env <- getEnv

322 moduleName <- substCurrentModule `fmap` ask

323 case M.lookup (qualify moduleName c) (dataConstructors env) of

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

325− Just (ty, _) -> replaceAllTypeSynonyms ty

325+ Just (ty, _) -> do ty' <- replaceAllTypeSynonyms ty

326+ return $ TypedValue v ty'

326infer' (Case vals binders) = do

327infer' (Case vals binders) = do

327 ts <- mapM infer vals

328 ts <- mapM infer vals

328 ret <- fresh

329 ret <- fresh

329− checkBinders ts ret binders

330+ binders' <- checkBinders (map (\(TypedValue _ t) -> t) ts) ret binders

330− return ret

331+ return $ TypedValue (Case ts binders') ret

331infer' (IfThenElse cond th el) = do

332infer' (IfThenElse cond th el) = do

332 check cond Boolean

333 check cond Boolean

333− t2 <- infer th

334+ TypedValue v2 t2 <- infer th

334− t3 <- infer el

335+ TypedValue v3 t3 <- infer el

335 t2 ~~ t3

336 t2 ~~ t3

336− return t2

337+ return $ TypedValue (IfThenElse cond v2 v3) t2

337infer' (TypedValue val ty) = do

338infer' (TypedValue val ty) = do

338 moduleName <- substCurrentModule <$> ask

339 moduleName <- substCurrentModule <$> ask

339 kind <- liftCheck $ kindOf moduleName ty

340 kind <- liftCheck $ kindOf moduleName ty

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

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

341 ty' <- replaceAllTypeSynonyms ty

342 ty' <- replaceAllTypeSynonyms ty

342 check val ty'

343 check val ty'

343− return ty'

344infer' _ = error "Invalid argument to infer"

345

346inferProperty :: Type -> String -> Subst (Maybe Type)

@@ -355,14 +355,15 @@ inferProperty (ForAll ident ty) prop = do

355 inferProperty replaced prop

356inferProperty _ _ = return Nothing

357

358−inferUnary :: UnaryOperator -> Type -> Subst Type

358+inferUnary :: UnaryOperator -> Value -> Subst Value

359−inferUnary op val =

359+inferUnary op (TypedValue val valTy) =

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

361− (valTy, resTy) -> do

361+ (valTy', resTy) -> do

362− val ~~ valTy

362+ valTy' ~~ valTy

363− return resTy

363+ return $ TypedValue (Unary op val) resTy

364+inferUnary _ _ = error "Invalid arguments to inferUnary"

364

365

365−checkUnary :: UnaryOperator -> Value -> Type -> Subst ()

366+checkUnary :: UnaryOperator -> Value -> Type -> Subst Value

366checkUnary op val res =

367checkUnary op val res =

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

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

368 (valTy, resTy) -> do

369 (valTy, resTy) -> do

@@ -375,29 +376,32 @@ unaryOps = [ (Negate, (Number, Number))

375 , (BitwiseNot, (Number, Number))

376 , (BitwiseNot, (Number, Number))

376 ]

377 ]

377

378

378−inferBinary :: BinaryOperator -> Type -> Type -> Subst Type

379+inferBinary :: BinaryOperator -> Value -> Value -> Subst Value

379−inferBinary op left right | isEqualityTest op = do

380+inferBinary op left@(TypedValue _ leftTy) right@(TypedValue _ rightTy) | isEqualityTest op = do

380− left ~~ right

381+ leftTy ~~ rightTy

381− return Boolean

382+ return $ TypedValue (Binary op left right) Boolean

382−inferBinary op left right =

383+inferBinary op left@(TypedValue _ leftTy) right@(TypedValue _ rightTy) =

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

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

384 (valTy, resTy) -> do

385 (valTy, resTy) -> do

385− left ~~ valTy

386+ leftTy ~~ valTy

386− right ~~ valTy

387+ rightTy ~~ valTy

387− return resTy

388+ return $ TypedValue (Binary op left right) resTy

389+inferBinary _ _ _ = error "Invalid arguments to inferBinary"

388

390

389−checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst ()

391+checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst Value

390checkBinary op left right res | isEqualityTest op = do

392checkBinary op left right res | isEqualityTest op = do

391 res ~~ Boolean

393 res ~~ Boolean

392− t1 <- infer left

394+ TypedValue v1 t1 <- infer left

393− t2 <- infer right

395+ TypedValue v2 t2 <- infer right

394 t1 ~~ t2

396 t1 ~~ t2

397+ return $ TypedValue (Binary op v1 v2) $ res

395checkBinary op left right res =

398checkBinary op left right res =

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

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

397 (valTy, resTy) -> do

400 (valTy, resTy) -> do

398 res ~~ resTy

401 res ~~ resTy

399− check left valTy

402+ v1 <- check left valTy

400− check right valTy

403+ v2 <- check right valTy

404+ return $ TypedValue (Binary op v1 v2) $ res

401

405

402isEqualityTest :: BinaryOperator -> Bool

406isEqualityTest :: BinaryOperator -> Bool

403isEqualityTest EqualTo = True

407isEqualityTest EqualTo = True

@@ -480,17 +484,20 @@ inferBinder val (NamedBinder name binder) = do

480 m <- inferBinder val binder

484 m <- inferBinder val binder

481 return $ M.insert name val m

485 return $ M.insert name val m

482

486

483−checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> Subst ()

487+checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> Subst [([Binder], Maybe Guard, Value)]

484−checkBinders _ _ [] = return ()

488+checkBinders _ _ [] = return []

485checkBinders nvals ret ((binders, grd, val):bs) = do

489checkBinders nvals ret ((binders, grd, val):bs) = do

486 moduleName <- substCurrentModule <$> ask

490 moduleName <- substCurrentModule <$> ask

487 m1 <- M.unions <$> zipWithM inferBinder nvals binders

491 m1 <- M.unions <$> zipWithM inferBinder nvals binders

488− bindLocalVariables moduleName (M.toList m1) $ do

492+ r <- bindLocalVariables moduleName (M.toList m1) $ do

489− check val ret

493+ val' <- check val ret

490 case grd of

494 case grd of

491− Nothing -> return ()

495+ Nothing -> return (binders, Nothing, val')

496+ Just g -> do

492− Just g -> check g Boolean

497+ g' <- check g Boolean

498+ return (binders, Just g', val')

493− checkBinders nvals ret bs

499+ rs <- checkBinders nvals ret bs

500+ return $ r : rs

494

501

495assignVariable :: Ident -> Subst ()

502assignVariable :: Ident -> Subst ()

496assignVariable name = do

503assignVariable name = do

@@ -500,66 +507,70 @@ assignVariable name = do

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

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

501 _ -> return ()

508 _ -> return ()

502

509

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)

504checkStatement mass _ (VariableIntroduction name val) = do

511checkStatement mass _ (VariableIntroduction name val) = do

505 assignVariable name

512 assignVariable name

506− t <- infer val

513+ val'@(TypedValue _ t) <- infer val

507− return (False, M.insert name t mass)

514+ return (False, M.insert name t mass, VariableIntroduction name val')

508checkStatement mass _ (Assignment ident val) = do

515checkStatement mass _ (Assignment ident val) = do

509− t <- infer val

516+ val'@(TypedValue _ t) <- infer val

510 case M.lookup ident mass of

517 case M.lookup ident mass of

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

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

512 Just ty -> do t ~~ ty

519 Just ty -> do t ~~ ty

513− return (False, mass)

520+ return (False, mass, Assignment ident val')

514checkStatement mass ret (While val inner) = do

521checkStatement mass ret (While val inner) = do

515− check val Boolean

522+ val' <- check val Boolean

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

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

517− return (allCodePathsReturn, mass)

524+ return (allCodePathsReturn, mass, While val' inner')

518checkStatement mass ret (If ifst) = do

525checkStatement mass ret (If ifst) = do

519− allCodePathsReturn <- checkIfStatement mass ret ifst

526+ (allCodePathsReturn, ifst') <- checkIfStatement mass ret ifst

520− return (allCodePathsReturn, mass)

527+ return (allCodePathsReturn, mass, If ifst')

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

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

522 moduleName <- substCurrentModule <$> ask

529 moduleName <- substCurrentModule <$> ask

523 assignVariable ident

530 assignVariable ident

524− check start Number

531+ start' <- check start Number

525− check end Number

532+ end' <- check end Number

526− (allCodePathsReturn, _) <- bindLocalVariables moduleName [(ident, Number)] $ checkBlock mass ret inner

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

527− return (allCodePathsReturn, mass)

534+ return (allCodePathsReturn, mass, For ident start' end' inner')

528checkStatement mass ret (Return val) = do

535checkStatement mass ret (Return val) = do

529− check val ret

536+ val' <- check val ret

530− return (True, mass)

537+ return (True, mass, Return val')

531

538

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

539+checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> Subst (Bool, IfStatement)

533checkIfStatement mass ret (IfStatement val thens Nothing) = do

540checkIfStatement mass ret (IfStatement val thens Nothing) = do

534− check val Boolean

541+ val' <- check val Boolean

535− _ <- checkBlock mass ret thens

542+ (_, _, thens') <- checkBlock mass ret thens

536− return False

543+ return (False, IfStatement val' thens' Nothing)

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

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

538− check val Boolean

545+ val' <- check val Boolean

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

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

540− allCodePathsReturn2 <- checkElseStatement mass ret elses

547+ (allCodePathsReturn2, elses') <- checkElseStatement mass ret elses

541− return $ allCodePathsReturn1 && allCodePathsReturn2

548+ return (allCodePathsReturn1 && allCodePathsReturn2, IfStatement val' thens' (Just elses'))

542−

549+

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

550+checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> Subst (Bool, ElseStatement)

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

551+checkElseStatement mass ret (Else elses) = do

552+ (allCodePathsReturn, _, elses') <- checkBlock mass ret elses

553+ return (allCodePathsReturn, Else elses')

545−checkElseStatement mass ret (ElseIf ifst) = checkIfStatement mass ret ifst

554+checkElseStatement mass ret (ElseIf ifst) = (id *** ElseIf) <$> checkIfStatement mass ret ifst

546−

555+

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

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

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

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

549checkBlock mass ret (s:ss) = do

558checkBlock mass ret (s:ss) = do

550 moduleName <- substCurrentModule <$> ask

559 moduleName <- substCurrentModule <$> ask

551− (b1, mass1) <- checkStatement mass ret s

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

552 bindLocalVariables moduleName (M.toList mass1) $ case (b1, ss) of

561 bindLocalVariables moduleName (M.toList mass1) $ case (b1, ss) of

553− (True, []) -> return (True, mass1)

562+ (True, []) -> return (True, mass1, [s'])

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

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

564+ (False, ss') -> do

555− (False, ss') -> checkBlock mass1 ret ss'

565+ (b, m, ss'') <- checkBlock mass1 ret ss'

566+ return (b, m, s':ss'')

556

567

557skolemize :: String -> Type -> Subst Type

568skolemize :: String -> Type -> Subst Type

558skolemize ident ty = do

569skolemize ident ty = do

559 tsk <- Skolem <$> fresh'

570 tsk <- Skolem <$> fresh'

560 return $ replaceTypeVars ident tsk ty

571 return $ replaceTypeVars ident tsk ty

561

572

562−check :: Value -> Type -> Subst ()

573+check :: Value -> Type -> Subst Value

563check val ty = rethrow errorMessage $ check' val ty

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

564 where

575 where

565 errorMessage msg =

576 errorMessage msg =

@@ -570,65 +581,73 @@ check val ty = rethrow errorMessage $ check' val ty

570 ":\n" ++

581 ":\n" ++

571 msg

582 msg

572

583

573−check' :: Value -> Type -> Subst ()

584+check' :: Value -> Type -> Subst Value

574check' val (ForAll idents ty) = do

585check' val (ForAll idents ty) = do

575 sk <- skolemize idents ty

586 sk <- skolemize idents ty

576 check val sk

587 check val sk

577check' val u@(TUnknown _) = do

588check' val u@(TUnknown _) = do

578− ty <- infer val

589+ val'@(TypedValue _ ty) <- infer val

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

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

580 ty' <- replaceAllVarsWithUnknowns ty

591 ty' <- replaceAllVarsWithUnknowns ty

581 ty' ~~ u

592 ty' ~~ u

593+ return val'

582−check' (NumericLiteral _) Number = return ()

594+check' v@(NumericLiteral _) Number = return $ TypedValue v Number

583−check' (StringLiteral _) String = return ()

595+check' v@(StringLiteral _) String = return $ TypedValue v String

584−check' (BooleanLiteral _) Boolean = return ()

596+check' v@(BooleanLiteral _) Boolean = return $ TypedValue v Boolean

585check' (Unary op val) ty = checkUnary op val ty

597check' (Unary op val) ty = checkUnary op val ty

586check' (Binary op left right) ty = checkBinary op left right ty

598check' (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)

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

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

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

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

590 moduleName <- substCurrentModule <$> ask

602 moduleName <- substCurrentModule <$> ask

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

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

592 bindLocalVariables moduleName (zip args argTys) $ check ret retTy

604 bindLocalVariables moduleName (zip args argTys) $ check ret retTy

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

605+check' (App f args) ret = do

594− let (f, argss) = unfoldApplication app

595− ft <- infer f

606+ f'@(TypedValue _ ft) <- infer f

596− checkFunctionApplications ft argss ret

607+ args' <- checkFunctionApplication ft args ret

608+ return $ TypedValue (App f' args') ret

597check' (Var var) ty = do

609check' (Var var) ty = do

598 moduleName <- substCurrentModule <$> ask

610 moduleName <- substCurrentModule <$> ask

599 ty1 <- lookupVariable moduleName var

611 ty1 <- lookupVariable moduleName var

600 repl <- replaceAllTypeSynonyms ty1

612 repl <- replaceAllTypeSynonyms ty1

601 repl `subsumes` ty

613 repl `subsumes` ty

614+ return $ TypedValue (Var var) ty

602−check' (TypedValue val ty1) ty2 = do

615+check' v@(TypedValue val ty1) ty2 = do

603 moduleName <- substCurrentModule <$> ask

616 moduleName <- substCurrentModule <$> ask

604 kind <- liftCheck $ kindOf moduleName ty1

617 kind <- liftCheck $ kindOf moduleName ty1

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

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

606 ty1 `subsumes` ty2

619 ty1 `subsumes` ty2

607 check val ty1

620 check val ty1

621+ return v

608check' (Case vals binders) ret = do

622check' (Case vals binders) ret = do

609− ts <- mapM infer vals

623+ vals' <- mapM infer vals

624+ let ts = map (\(TypedValue _ t) -> t) vals'

610− checkBinders ts ret binders

625+ binders' <- checkBinders ts ret binders

626+ return $ TypedValue (Case vals' binders') ret

611check' (IfThenElse cond th el) ty = do

627check' (IfThenElse cond th el) ty = do

612 check cond Boolean

628 check cond Boolean

613 check th ty

629 check th ty

614 check el ty

630 check el ty

615−check' (ObjectLiteral ps) (Object row) = do

631+check' (ObjectLiteral ps) t@(Object row) = do

616 ensureNoDuplicateProperties ps

632 ensureNoDuplicateProperties ps

617− checkProperties ps row False

633+ ps' <- checkProperties ps row False

634+ return $ TypedValue (ObjectLiteral ps') t

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

635+check' (ObjectUpdate obj ps) t@(Object row) = do

619 ensureNoDuplicateProperties ps

636 ensureNoDuplicateProperties ps

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

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

621 let (propsToCheck, rest) = rowToList row

638 let (propsToCheck, rest) = rowToList row

622 propsToRemove = map fst ps

639 propsToRemove = map fst ps

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

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

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

641+ obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))

625− checkProperties ps row True

642+ ps' <- checkProperties ps row True

643+ return $ TypedValue (ObjectUpdate obj' ps') t

626check' (Accessor prop val) ty = do

644check' (Accessor prop val) ty = do

627 rest <- fresh

645 rest <- fresh

628 check val (Object (RCons prop ty rest))

646 check val (Object (RCons prop ty rest))

629check' (Block ss) ret = do

647check' (Block ss) ret = do

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

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

631 guardWith "Block is missing a return statement" allCodePathsReturn

649 guardWith "Block is missing a return statement" allCodePathsReturn

650+ return $ TypedValue (Block ss') ret

632check' (Constructor c) ty = do

651check' (Constructor c) ty = do

633 env <- getEnv

652 env <- getEnv

634 moduleName <- substCurrentModule <$> ask

653 moduleName <- substCurrentModule <$> ask

@@ -637,51 +656,42 @@ check' (Constructor c) ty = do

637 Just (ty1, _) -> do

656 Just (ty1, _) -> do

638 repl <- replaceAllTypeSynonyms ty1

657 repl <- replaceAllTypeSynonyms ty1

639 repl `subsumes` ty

658 repl `subsumes` ty

659+ return $ TypedValue (Constructor c) ty

640check' val (SaturatedTypeSynonym name args) = do

660check' val (SaturatedTypeSynonym name args) = do

641 ty <- expandTypeSynonym name args

661 ty <- expandTypeSynonym name args

642 check val ty

662 check val ty

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

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

644

664

645−checkProperties :: [(String, Value)] -> Type -> Bool -> Subst ()

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

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

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

647− go [] [] REmpty = return ()

667+ go [] [] REmpty = return []

648− go [] [] u@(TUnknown _) = u ~~ REmpty

668+ go [] [] u@(TUnknown _) = do u ~~ REmpty

669+ return []

649− go [] [] (Skolem _) | lax = return ()

670+ go [] [] (Skolem _) | lax = return []

650− go [] ((p, _): _) _ | lax = return ()

671+ go [] ((p, _): _) _ | lax = return []

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

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

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

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

653 go ((p,v):ps') [] u@(TUnknown _) = do

674 go ((p,v):ps') [] u@(TUnknown _) = do

654− ty <- infer v

675+ v'@(TypedValue _ ty) <- infer v

655 rest <- fresh

676 rest <- fresh

656 u ~~ RCons p ty rest

677 u ~~ RCons p ty rest

657− go ps' [] rest

678+ ps'' <- go ps' [] rest

679+ return $ (p, v') : ps''

658 go ((p,v):ps') ts r =

680 go ((p,v):ps') ts r =

659 case lookup p ts of

681 case lookup p ts of

660 Nothing -> do

682 Nothing -> do

661− ty <- infer v

683+ v'@(TypedValue _ ty) <- infer v

662 rest <- fresh

684 rest <- fresh

663 r ~~ RCons p ty rest

685 r ~~ RCons p ty rest

664− go ps' ts rest

686+ ps'' <- go ps' ts rest

687+ return $ (p, v') : ps''

665 Just ty -> do

688 Just ty -> do

666− check v ty

689+ v' <- check v ty

667− go ps' (delete (p, ty) ts) r

690+ ps'' <- go ps' (delete (p, ty) ts) r

691+ return $ (p, v') : ps''

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

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

669

693

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

694+checkFunctionApplication :: Type -> [Value] -> Type -> Subst [Value]

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

685checkFunctionApplication fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fnTy args ret

695checkFunctionApplication fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fnTy args ret

686 where

696 where

687 errorMessage msg = "Error applying function of type "

697 errorMessage msg = "Error applying function of type "

@@ -699,7 +709,6 @@ inferFunctionApplication (ForAll ident ty) args = do

699 replaced <- replaceVarWithUnknown ident ty

709 replaced <- replaceVarWithUnknown ident ty

700 inferFunctionApplication replaced args

710 inferFunctionApplication replaced args

701inferFunctionApplication u@(TUnknown _) args = do

711inferFunctionApplication u@(TUnknown _) args = do

702−

703 ret <- fresh

712 ret <- fresh

704 args' <- mapM replaceAllVarsWithUnknowns args

713 args' <- mapM replaceAllVarsWithUnknowns args

705 u ~~ Function args' ret

714 u ~~ Function args' ret

@@ -711,17 +720,20 @@ inferFunctionApplication fnTy args = throwError $ "Cannot apply function of type

711 ++ prettyPrintType fnTy

720 ++ prettyPrintType fnTy

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

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

713

722

714−checkFunctionApplication' :: Type -> [Value] -> Type -> Subst ()

723+checkFunctionApplication' :: Type -> [Value] -> Type -> Subst [Value]

715checkFunctionApplication' (Function argTys retTy) args ret = do

724checkFunctionApplication' (Function argTys retTy) args ret = do

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

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

717− zipWithM (check) args argTys

726+ args' <- zipWithM check args argTys

718 retTy `subsumes` ret

727 retTy `subsumes` ret

728+ return args'

719checkFunctionApplication' (ForAll ident ty) args ret = do

729checkFunctionApplication' (ForAll ident ty) args ret = do

720 replaced <- replaceVarWithUnknown ident ty

730 replaced <- replaceVarWithUnknown ident ty

721 checkFunctionApplication replaced args ret

731 checkFunctionApplication replaced args ret

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

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

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

733+ args' <- mapM (\arg -> infer arg >>= \(TypedValue v t) -> TypedValue v <$> replaceAllVarsWithUnknowns t) args

734+ let tys = map (\(TypedValue _ t) -> t) args'

724− u ~~ Function tyArgs ret

735+ u ~~ Function tys ret

736+ return args'

725checkFunctionApplication' (SaturatedTypeSynonym name tyArgs) args ret = do

737checkFunctionApplication' (SaturatedTypeSynonym name tyArgs) args ret = do

726 ty <- expandTypeSynonym name tyArgs

738 ty <- expandTypeSynonym name tyArgs

727 checkFunctionApplication' ty args ret

739 checkFunctionApplication' ty args ret