8c9d494 · rowtype-yoga/purescript-native

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

on golang help sign in

Fix up broken tests, fix the escape check and skolem escape check.

8c9d494Phil Freeman13 years ago

examples/passing/Do.purs+1−1

compare with golang

unifiedsplit

@@ -19,7 +19,7 @@ test3 = maybe do

20test4 = maybe do

21 Just 1

22− Nothing

22+ Nothing :: Maybe Number

23 return 2

25test5 mx my = maybe do

purescript.cabal+1−1

@@ -72,7 +72,7 @@ executable psc

72 buildable: True

73 hs-source-dirs: src

74 other-modules:

75− ghc-options: -Wall -O2 -fno-warn-unused-do-bind

75+ ghc-options: -Wall -O2

77test-suite tests

78 build-depends: base >=4 && <5, cmdtheline -any, containers -any,

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

@@ -97,7 +97,7 @@ typeCheckAll moduleName (DataBindingGroupDeclaration tys : rest) = do

97 forM_ tys $ \(name, _, _) ->

98 typeIsNotDefined moduleName name

99 ks <- kindsOfAll moduleName (map (\(name, args, dctors) -> (name, args, mapMaybe snd dctors)) tys)

100− forM (zip tys ks) $ \((name, args, dctors), ctorKind) ->

100+ forM_ (zip tys ks) $ \((name, args, dctors), ctorKind) ->

101 addDataType moduleName name args dctors ctorKind

102 typeCheckAll moduleName rest

103typeCheckAll moduleName (TypeSynonymDeclaration name args ty : rest) = do

@@ -119,7 +119,7 @@ typeCheckAll moduleName (BindingGroupDeclaration vals : rest) = do

119 forM_ (map fst vals) $ \name ->

120 valueIsNotDefined moduleName name

121 tys <- typesOf moduleName vals

122− forM (zip (map fst vals) tys) $ \(name, ty) ->

122+ forM_ (zip (map fst vals) tys) $ \(name, ty) ->

123 addValue moduleName name ty

124 typeCheckAll moduleName rest

125typeCheckAll moduleName (ExternDataDeclaration name kind : rest) = do

src/Language/PureScript/TypeChecker/Monad.hs+3

@@ -156,6 +156,9 @@ deriving instance MonadError String Subst

156liftCheck :: Check a -> Subst a

157liftCheck = Subst . lift . lift

158

159+getSubstState :: Subst SubstState

160+getSubstState = Subst . lift $ get

161+

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

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

160runSubst context subst = do

163runSubst context subst = do

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

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

src/Language/PureScript/TypeChecker/Types.hs+69−79

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

22import Data.List

23import Data.Maybe (isNothing, isJust, fromMaybe)

24import qualified Data.Data as D

25−import Data.Generics

26− (mkT, something, everywhere, mkQ)

25+import Data.Generics (everything, mkT, something, everywhere, mkQ)

28import Language.PureScript.Values

27import Language.PureScript.Values

29import Language.PureScript.Types

28import Language.PureScript.Types

@@ -129,7 +128,7 @@ unifyRows r1 r2 =

129 unifyRows' sd r [] (TUnknown u) = replace u (rowFromList (sd, r))

128 unifyRows' sd r [] (TUnknown u) = replace u (rowFromList (sd, r))

130 unifyRows' ((name, ty):row) r others u@(TUnknown un) = do

129 unifyRows' ((name, ty):row) r others u@(TUnknown un) = do

131 occursCheck un ty

130 occursCheck un ty

132− forM row $ \(_, t) -> occursCheck un t

131+ forM_ row $ \(_, t) -> occursCheck un t

133 u' <- fresh

132 u' <- fresh

134 u ~~ RCons name ty u'

133 u ~~ RCons name ty u'

135 unifyRows' row r others u'

134 unifyRows' row r others u'

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

143

142

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

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

145typesOf moduleName vals = do

144typesOf moduleName vals = do

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

145+ (tys, _) <- runSubst (SubstContext moduleName) $ do

147 let es = map isTyped vals

146 let es = map isTyped vals

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

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

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

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

@@ -152,46 +151,50 @@ typesOf moduleName vals = do

152 let untypedDict = zip (map fst untyped) untypedNames

151 let untypedDict = zip (map fst untyped) untypedNames

153 dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable))) $ typedDict ++ untypedDict)

152 dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable))) $ typedDict ++ untypedDict)

154 tys <- forM es $ \e -> do

153 tys <- forM es $ \e -> do

155− ty <- case e of

154+ (val, ty) <- case e of

156 (_, (val, Just ty)) -> do

155 (_, (val, Just ty)) -> do

157 kind <- liftCheck $ kindOf moduleName ty

156 kind <- liftCheck $ kindOf moduleName ty

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

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

159 ty' <- replaceAllTypeSynonyms ty

158 ty' <- replaceAllTypeSynonyms ty

160− bindNames dict $ check val ty'

159+ val' <- bindNames dict $ check val ty'

161− return ty'

160+ return (val', ty')

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

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

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

162+ TypedValue val' ty <- bindNames dict $ infer val

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

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

165− return ty

164+ return (val', ty)

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

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

167 [eff, a] <- replicateM 2 fresh

166 [eff, a] <- replicateM 2 fresh

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

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

168+ escapeCheck val ty

169 return ty

170 return tys

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

172− forM tys $ skolemEscapeCheck

171+ forM_ tys $ skolemEscapeCheck

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

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

174

173

175isTyped :: (Ident, Value) -> (Ident, (Value, Maybe Type))

174isTyped :: (Ident, Value) -> (Ident, (Value, Maybe Type))

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

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

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

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

178

177

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

178+escapeCheck :: Value -> Type -> Subst ()

180−escapeCheck checks ty sub =

179+escapeCheck value ty = do

181− let

180+ subst <- substSubst <$> getSubstState

182− visibleUnknowns = nub $ unknowns ty

181+ let visibleUnknowns = nub $ unknowns $ apply subst ty

183− in

182+ let allUnknowns = findAllTypes value

184− forM_ checks $ \c -> case c of

183+ forM_ allUnknowns $ \t -> do

185− AnyUnifiable t -> do

186− let unsolvedUnknowns = nub . unknowns $ apply sub t

184+ let unsolvedUnknowns = nub . unknowns $ apply subst t

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

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

188−-}

186+

187+findAllTypes :: Value -> [Type]

188+findAllTypes = everything (++) (mkQ [] go)

189+ where

190+ go (TypedValue _ ty) = [ty]

191+ go _ = []

189

192

190skolemEscapeCheck :: Type -> Check ()

193skolemEscapeCheck :: Type -> Check ()

191skolemEscapeCheck ty =

194skolemEscapeCheck ty =

192 case something (mkQ Nothing findSkolems) ty of

195 case something (mkQ Nothing findSkolems) ty of

193 Nothing -> return ()

196 Nothing -> return ()

194− Just _ -> throwError "Skolem variables cannot escape. Consider adding a type signature."

197+ Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature." ++ show ty

195 where

198 where

196 findSkolems (Skolem _) = return ()

199 findSkolems (Skolem _) = return ()

197 findSkolems _ = mzero

200 findSkolems _ = mzero

@@ -283,9 +286,9 @@ infer' (ObjectUpdate o ps) = do

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

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

284infer' (Indexer index val) = do

287infer' (Indexer index val) = do

285 el <- fresh

288 el <- fresh

286− check index Number

289+ index' <- check index Number

287− check val (Array el)

290+ val' <- check val (Array el)

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

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

289infer' (Accessor prop val) = do

292infer' (Accessor prop val) = do

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

293 typed@(TypedValue _ objTy) <- infer val

291 propTy <- inferProperty objTy prop

294 propTy <- inferProperty objTy prop

@@ -330,11 +333,11 @@ infer' (Case vals binders) = do

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

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

331 return $ TypedValue (Case ts binders') ret

334 return $ TypedValue (Case ts binders') ret

332infer' (IfThenElse cond th el) = do

335infer' (IfThenElse cond th el) = do

333− check cond Boolean

336+ cond' <- check cond Boolean

334− TypedValue v2 t2 <- infer th

337+ v2@(TypedValue _ t2) <- infer th

335− TypedValue v3 t3 <- infer el

338+ v3@(TypedValue _ t3) <- infer el

336 t2 ~~ t3

339 t2 ~~ t3

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

340+ return $ TypedValue (IfThenElse cond' v2 v3) t2

338infer' (TypedValue val ty) = do

341infer' (TypedValue val ty) = do

339 moduleName <- substCurrentModule <$> ask

342 moduleName <- substCurrentModule <$> ask

340 kind <- liftCheck $ kindOf moduleName ty

343 kind <- liftCheck $ kindOf moduleName ty

@@ -368,7 +371,8 @@ checkUnary op val res =

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

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

369 (valTy, resTy) -> do

372 (valTy, resTy) -> do

370 res ~~ resTy

373 res ~~ resTy

371− check val valTy

374+ val' <- check val valTy

375+ return $ Unary op val'

372

376

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

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

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

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

@@ -391,17 +395,17 @@ inferBinary _ _ _ = error "Invalid arguments to inferBinary"

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

395checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst Value

392checkBinary op left right res | isEqualityTest op = do

396checkBinary op left right res | isEqualityTest op = do

393 res ~~ Boolean

397 res ~~ Boolean

394− TypedValue v1 t1 <- infer left

398+ left'@(TypedValue _ t1) <- infer left

395− TypedValue v2 t2 <- infer right

399+ right'@(TypedValue _ t2) <- infer right

396 t1 ~~ t2

400 t1 ~~ t2

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

401+ return $ Binary op left' right'

398checkBinary op left right res =

402checkBinary op left right res =

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

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

400 (valTy, resTy) -> do

404 (valTy, resTy) -> do

401 res ~~ resTy

405 res ~~ resTy

402− v1 <- check left valTy

406+ left' <- check left valTy

403− v2 <- check right valTy

407+ right' <- check right valTy

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

408+ return $ Binary op left' right'

405

409

406isEqualityTest :: BinaryOperator -> Bool

410isEqualityTest :: BinaryOperator -> Bool

407isEqualityTest EqualTo = True

411isEqualityTest EqualTo = True

@@ -591,48 +595,53 @@ check' val u@(TUnknown _) = do

591 ty' <- replaceAllVarsWithUnknowns ty

595 ty' <- replaceAllVarsWithUnknowns ty

592 ty' ~~ u

596 ty' ~~ u

593 return val'

597 return val'

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

598+check' v@(NumericLiteral _) Number = return v

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

599+check' v@(StringLiteral _) String = return v

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

600+check' v@(BooleanLiteral _) Boolean = return v

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

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

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

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

599−check' (ArrayLiteral vals) (Array ty) = TypedValue <$> (ArrayLiteral <$> forM vals (\val -> check val ty)) <*> pure (Array ty)

603+check' (ArrayLiteral vals) (Array ty) = ArrayLiteral <$> forM vals (\val -> check val ty)

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

604+check' (Indexer index vals) ty = do

605+ index' <- check index Number

606+ vals' <- check vals (Array ty)

607+ return $ Indexer index' vals'

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

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

602 moduleName <- substCurrentModule <$> ask

609 moduleName <- substCurrentModule <$> ask

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

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

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

611+ ret' <- bindLocalVariables moduleName (zip args argTys) $ check ret retTy

612+ return $ Abs args ret'

605check' (App f args) ret = do

613check' (App f args) ret = do

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

614 f'@(TypedValue _ ft) <- infer f

607 args' <- checkFunctionApplication ft args ret

615 args' <- checkFunctionApplication ft args ret

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

616+ return $ App f' args'

609check' (Var var) ty = do

617check' (Var var) ty = do

610 moduleName <- substCurrentModule <$> ask

618 moduleName <- substCurrentModule <$> ask

611 ty1 <- lookupVariable moduleName var

619 ty1 <- lookupVariable moduleName var

612 repl <- replaceAllTypeSynonyms ty1

620 repl <- replaceAllTypeSynonyms ty1

613 repl `subsumes` ty

621 repl `subsumes` ty

614− return $ TypedValue (Var var) ty

622+ return $ Var var

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

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

616 moduleName <- substCurrentModule <$> ask

624 moduleName <- substCurrentModule <$> ask

617 kind <- liftCheck $ kindOf moduleName ty1

625 kind <- liftCheck $ kindOf moduleName ty1

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

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

619 ty1 `subsumes` ty2

627 ty1 `subsumes` ty2

620− check val ty1

628+ val' <- check val ty1

621− return v

629+ return $ TypedValue val' ty1

622check' (Case vals binders) ret = do

630check' (Case vals binders) ret = do

623 vals' <- mapM infer vals

631 vals' <- mapM infer vals

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

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

625 binders' <- checkBinders ts ret binders

633 binders' <- checkBinders ts ret binders

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

634+ return $ Case vals' binders'

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

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

628− check cond Boolean

636+ cond' <- check cond Boolean

629− check th ty

637+ th' <- check th ty

630− check el ty

638+ el' <- check el ty

639+ return $ IfThenElse cond' th' el'

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

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

632 ensureNoDuplicateProperties ps

641 ensureNoDuplicateProperties ps

633 ps' <- checkProperties ps row False

642 ps' <- checkProperties ps row False

634− return $ TypedValue (ObjectLiteral ps') t

643+ return $ ObjectLiteral ps'

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

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

636 ensureNoDuplicateProperties ps

645 ensureNoDuplicateProperties ps

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

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

638 let (propsToCheck, rest) = rowToList row

647 let (propsToCheck, rest) = rowToList row

@@ -640,14 +649,15 @@ check' (ObjectUpdate obj ps) t@(Object row) = do

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

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

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

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

642 ps' <- checkProperties ps row True

651 ps' <- checkProperties ps row True

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

652+ return $ ObjectUpdate obj' ps'

644check' (Accessor prop val) ty = do

653check' (Accessor prop val) ty = do

645 rest <- fresh

654 rest <- fresh

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

655+ val' <- check val (Object (RCons prop ty rest))

656+ return $ Accessor prop val'

647check' (Block ss) ret = do

657check' (Block ss) ret = do

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

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

649 guardWith "Block is missing a return statement" allCodePathsReturn

659 guardWith "Block is missing a return statement" allCodePathsReturn

650− return $ TypedValue (Block ss') ret

660+ return $ Block ss'

651check' (Constructor c) ty = do

661check' (Constructor c) ty = do

652 env <- getEnv

662 env <- getEnv

653 moduleName <- substCurrentModule <$> ask

663 moduleName <- substCurrentModule <$> ask

@@ -656,7 +666,7 @@ check' (Constructor c) ty = do

656 Just (ty1, _) -> do

666 Just (ty1, _) -> do

657 repl <- replaceAllTypeSynonyms ty1

667 repl <- replaceAllTypeSynonyms ty1

658 repl `subsumes` ty

668 repl `subsumes` ty

659− return $ TypedValue (Constructor c) ty

669+ return $ Constructor c

660check' val (SaturatedTypeSynonym name args) = do

670check' val (SaturatedTypeSynonym name args) = do

661 ty <- expandTypeSynonym name args

671 ty <- expandTypeSynonym name args

662 check val ty

672 check val ty

@@ -700,26 +710,6 @@ checkFunctionApplication fnTy args ret = rethrow errorMessage $ checkFunctionApp

700 ++ ", expecting value of type "

710 ++ ", expecting value of type "

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

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

702

712

703−inferFunctionApplication :: Type -> [Type] -> Subst Type

704−inferFunctionApplication (Function argTys retTy) args = do

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

706− zipWithM subsumes args argTys

707− return retTy

708−inferFunctionApplication (ForAll ident ty) args = do

709− replaced <- replaceVarWithUnknown ident ty

710− inferFunctionApplication replaced args

711−inferFunctionApplication u@(TUnknown _) args = do

712− ret <- fresh

713− args' <- mapM replaceAllVarsWithUnknowns args

714− u ~~ Function args' ret

715− return ret

716−inferFunctionApplication (SaturatedTypeSynonym name tyArgs) args = do

717− ty <- expandTypeSynonym name tyArgs

718− inferFunctionApplication ty args

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

720− ++ prettyPrintType fnTy

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

722−

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

713checkFunctionApplication' :: Type -> [Value] -> Type -> Subst [Value]

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

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

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

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

@@ -747,7 +737,7 @@ subsumes (ForAll ident ty1) ty2 = do

747 replaced <- replaceVarWithUnknown ident ty1

737 replaced <- replaceVarWithUnknown ident ty1

748 replaced `subsumes` ty2

738 replaced `subsumes` ty2

749subsumes (Function args1 ret1) (Function args2 ret2) = do

739subsumes (Function args1 ret1) (Function args2 ret2) = do

750− zipWithM subsumes args2 args1

740+ zipWithM_ subsumes args2 args1

751 ret1 `subsumes` ret2

741 ret1 `subsumes` ret2

752subsumes ty1 ty2 = ty1 ~~ ty2

742subsumes ty1 ty2 = ty1 ~~ ty2

753

743