0574eeb · rowtype-yoga/purescript-native

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

Merge pull request #714 from purescript/287

Type Wildcards

commit0574eeb77ed3341d207570a6b2c9765c11b84bc5 authorPhil Freeman <paf31@cantab.net> dateMon 17 Nov 2014, 08:41 (12 years ago) parentc61ad82 2d01405

11 files changed+91−19

compare with golang

unifiedsplit

examples/failing/TypeWildcards1.purs+4 examples/failing/TypeWildcards2.purs+4 examples/failing/TypeWildcards3.purs+7 examples/passing/TypeWildcards.purs+13 src/Language/PureScript/Parser/Declarations.hs+8−8 src/Language/PureScript/Parser/Types.hs+14 src/Language/PureScript/Pretty/Types.hs+1 src/Language/PureScript/TypeChecker/Kinds.hs+1 src/Language/PureScript/TypeChecker/Types.hs+13−11 src/Language/PureScript/TypeChecker/Unify.hs+12 src/Language/PureScript/Types.hs+14

examples/failing/TypeWildcards1.pursnew file+4

@@ -0,0 +1,4 @@

1+module TypeWildcards where

3+type Test = _

examples/failing/TypeWildcards2.pursnew file+4

@@ -0,0 +1,4 @@

1+module TypeWildcards where

3+data Test = Test _

examples/failing/TypeWildcards3.pursnew file+7

@@ -0,0 +1,7 @@

1+module TypeWildcards where

3+data Foo a = Foo

5+instance showFoo :: Show (Foo _) where

6+ show Foo = "Foo"

examples/passing/TypeWildcards.pursnew file+13

@@ -0,0 +1,13 @@

1+module Main where

3+testTopLevel :: _ -> _

4+testTopLevel n = n + 1

6+test :: forall a. (Eq a) => (a -> a) -> a -> a

7+test f a = go (f a) a

8+ where

9+ go :: _ -> _ -> _

10+ go a1 a2 | a1 == a2 = a1

11+ go a1 _ = go (f a1) a1

12+

13+main = Debug.Trace.trace "Done"

src/Language/PureScript/Parser/Declarations.hs+8−8

@@ -64,7 +64,7 @@ parseDataDeclaration = do

6464 tyArgs <- many (indented *> kindedIdent)

6565 ctors <- P.option [] $ do

6666 _ <- lexeme $ indented *> P.char '='

67− sepBy1 ((,) <$> properName <*> P.many (indented *> parseTypeAtom)) pipe

67+ sepBy1 ((,) <$> properName <*> P.many (indented *> noWildcards parseTypeAtom)) pipe

6868 return $ DataDeclaration dtype name tyArgs ctors

6969

7070parseTypeDeclaration :: P.Parsec String ParseState Declaration

@@ -76,7 +76,7 @@ parseTypeSynonymDeclaration :: P.Parsec String ParseState Declaration

7676parseTypeSynonymDeclaration =

7777 TypeSynonymDeclaration <$> (P.try (reserved "type") *> indented *> properName)

7878 <*> many (indented *> kindedIdent)

79− <*> (lexeme (indented *> P.char '=') *> parsePolyType)

79+ <*> (lexeme (indented *> P.char '=') *> noWildcards parsePolyType)

8080

8181parseValueDeclaration :: P.Parsec String ParseState Declaration

8282parseValueDeclaration = do

@@ -106,16 +106,16 @@ parseExternDeclaration = P.try (reserved "foreign") *> indented *> reserved "imp

106106 <|> (do reserved "instance"

107107 name <- parseIdent <* lexeme (indented *> P.string "::")

108108 deps <- P.option [] $ do

109− deps <- parens (commaSep1 ((,) <$> parseQualified properName <*> P.many parseTypeAtom))

109+ deps <- parens (commaSep1 ((,) <$> parseQualified properName <*> P.many (noWildcards parseTypeAtom)))

110110 indented

111111 reservedOp "=>"

112112 return deps

113113 className <- indented *> parseQualified properName

114− tys <- P.many (indented *> parseTypeAtom)

114+ tys <- P.many (indented *> noWildcards parseTypeAtom)

115115 return $ ExternInstanceDeclaration name deps className tys)

116116 <|> (do ident <- parseIdent

117117 js <- P.optionMaybe (JSRaw <$> stringLiteral)

118− ty <- lexeme (indented *> P.string "::") *> parsePolyType

118+ ty <- lexeme (indented *> P.string "::") *> noWildcards parsePolyType

119119 return $ ExternDeclaration (if isJust js then InlineJavascript else ForeignImport) ident js ty))

120120

121121parseAssociativity :: P.Parsec String ParseState Associativity

@@ -176,7 +176,7 @@ parseTypeClassDeclaration = do

176176 reserved "class"

177177 implies <- P.option [] $ do

178178 indented

179− implies <- parens (commaSep1 ((,) <$> parseQualified properName <*> P.many parseTypeAtom))

179+ implies <- parens (commaSep1 ((,) <$> parseQualified properName <*> P.many (noWildcards parseTypeAtom)))

180180 reservedOp "<="

181181 return implies

182182 className <- indented *> properName

@@ -191,12 +191,12 @@ parseTypeInstanceDeclaration = do

191191 reserved "instance"

192192 name <- parseIdent <* lexeme (indented *> P.string "::")

193193 deps <- P.optionMaybe $ do

194− deps <- parens (commaSep1 ((,) <$> parseQualified properName <*> P.many parseTypeAtom))

194+ deps <- parens (commaSep1 ((,) <$> parseQualified properName <*> P.many (noWildcards parseTypeAtom)))

195195 indented

196196 reservedOp "=>"

197197 return deps

198198 className <- indented *> parseQualified properName

199− ty <- P.many (indented *> parseTypeAtom)

199+ ty <- P.many (indented *> (noWildcards parseTypeAtom))

200200 members <- P.option [] . P.try $ do

201201 indented *> reserved "where"

202202 mark (P.many (same *> positioned parseValueDeclaration))

src/Language/PureScript/Parser/Types.hs+14

@@ -16,6 +16,7 @@

1616module Language.PureScript.Parser.Types (

1717 parseType,

1818 parsePolyType,

19+ noWildcards,

1920 parseTypeAtom

2021) where

2122

@@ -43,6 +44,9 @@ parseFunction = parens $ P.try (lexeme (P.string "->")) >> return tyFunction

4344parseObject :: P.Parsec String ParseState Type

4445parseObject = braces $ TypeApp tyObject <$> parseRow

4546

47+parseTypeWildcard :: P.Parsec String ParseState Type

48+parseTypeWildcard = lexeme (P.char '_') >> return TypeWildcard

49+

4650parseTypeVariable :: P.Parsec String ParseState Type

4751parseTypeVariable = do

4852 ident <- identifier

@@ -65,6 +69,7 @@ parseTypeAtom = indented *> P.choice (map P.try

6569 , parseArrayOf

6670 , parseFunction

6771 , parseObject

72+ , parseTypeWildcard

6873 , parseTypeVariable

6974 , parseTypeConstructor

7075 , parseForAll

@@ -108,6 +113,15 @@ parseType = do

108113parsePolyType :: P.Parsec String ParseState Type

109114parsePolyType = parseAnyType

110115

116+-- |

117+-- Parse an atomic type with no wildcards

118+--

119+noWildcards :: P.Parsec String ParseState Type -> P.Parsec String ParseState Type

120+noWildcards p = do

121+ ty <- p

122+ when (containsWildcards ty) $ P.unexpected "type wildcard"

123+ return ty

124+

111125parseNameAndType :: P.Parsec String ParseState t -> P.Parsec String ParseState (String, t)

112126parseNameAndType p = (,) <$> (indented *> (identifierName <|> stringLiteral) <* indented <* lexeme (P.string "::")) <*> p

113127

src/Language/PureScript/Pretty/Types.hs+1

@@ -34,6 +34,7 @@ import Language.PureScript.Environment

3434typeLiterals :: Pattern () Type String

3535typeLiterals = mkPattern match

3636 where

37+ match TypeWildcard = Just "_"

3738 match (TypeVar var) = Just var

3839 match (PrettyPrintObject row) = Just $ "{ " ++ prettyPrintRow row ++ " }"

3940 match (PrettyPrintArray ty) = Just $ "[" ++ prettyPrintType ty ++ "]"

src/Language/PureScript/TypeChecker/Kinds.hs+1

@@ -149,6 +149,7 @@ infer :: Type -> UnifyT Kind Check Kind

149149infer ty = rethrow (mkErrorStack "Error inferring type of value" (Just (TypeError ty)) <>) $ infer' ty

150150

151151infer' :: Type -> UnifyT Kind Check Kind

152+infer' TypeWildcard = fresh

152153infer' (TypeVar v) = do

153154 Just moduleName <- checkCurrentModule <$> get

154155 UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

src/Language/PureScript/TypeChecker/Types.hs+13−11

@@ -129,15 +129,17 @@ typeDictionaryForBindingGroup moduleName vals = do

129129

130130checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData -> UnifyT Type Check (Ident, (Expr, Type))

131131checkTypedBindingGroupElement moduleName (ident, (val', ty, checkType)) dict = do

132+ -- Replace type wildcards

133+ ty' <- replaceTypeWildcards ty

132134 -- Kind check

133135 kind <- liftCheck $ kindOf moduleName ty

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

135137 -- Check the type with the new names in scope

136− ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty

138+ ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'

137139 val'' <- if checkType

138− then bindNames dict $ TypedValue True <$> check val' ty' <*> pure ty'

139− else return (TypedValue False val' ty')

140− return (ident, (val'', ty'))

140+ then bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''

141+ else return (TypedValue False val' ty'')

142+ return (ident, (val'', ty''))

141143

142144typeForBindingGroupElement :: (Ident, Expr) -> TypeData -> UntypedData -> UnifyT Type Check (Ident, (Expr, Type))

143145typeForBindingGroupElement (ident, val) dict untypedDict = do

@@ -259,7 +261,7 @@ infer' (App f arg) = do

259261infer' (Var var) = do

260262 Just moduleName <- checkCurrentModule <$> get

261263 checkVisibility moduleName var

262− ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var

264+ ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards <=< lookupVariable moduleName $ var

263265 case ty of

264266 ConstrainedType constraints ty' -> do

265267 dicts <- getTypeClassDictionaries

@@ -291,7 +293,7 @@ infer' (SuperClassDictionary className tys) = do

291293infer' (TypedValue checkType val ty) = do

292294 Just moduleName <- checkCurrentModule <$> get

293295 checkTypeKind moduleName ty

294− ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty

296+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

295297 val' <- if checkType then check val ty' else return val

296298 return $ TypedValue True val' ty'

297299infer' (PositionedValue pos val) = rethrowWithPosition pos $ infer' val

@@ -303,7 +305,7 @@ inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue

303305 Just moduleName <- checkCurrentModule <$> get

304306 checkTypeKind moduleName ty

305307 let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)

306− ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty

308+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

307309 TypedValue _ val' ty'' <- if checkType then bindNames dict (check val ty') else return tv

308310 bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j

309311inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do

@@ -483,7 +485,7 @@ check' v@(Var var) ty = do

483485 Just moduleName <- checkCurrentModule <$> get

484486 checkVisibility moduleName var

485487 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var

486− ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty

488+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

487489 v' <- subsumes (Just v) repl ty'

488490 case v' of

489491 Nothing -> throwError . strMsg $ "Unable to check type subsumption"

@@ -504,8 +506,8 @@ check' (SuperClassDictionary className tys) _ = do

504506check' (TypedValue checkType val ty1) ty2 = do

505507 Just moduleName <- checkCurrentModule <$> get

506508 checkTypeKind moduleName ty1

507− ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1

508− ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty2

509+ ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1

510+ ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2

509511 val' <- subsumes (Just val) ty1' ty2'

510512 case val' of

511513 Nothing -> throwError . strMsg $ "Unable to check type subsumption"

@@ -555,7 +557,7 @@ check' (Let ds val) ty = do

555557 (ds', val') <- inferLetBinding [] ds val (`check` ty)

556558 return $ TypedValue True (Let ds' val') ty

557559check' val ty | containsTypeSynonyms ty = do

558− ty' <- introduceSkolemScope <=< expandAllTypeSynonyms $ ty

560+ ty' <- introduceSkolemScope <=< expandAllTypeSynonyms <=< replaceTypeWildcards $ ty

559561 check val ty'

560562check' val kt@(KindedType ty kind) = do

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

src/Language/PureScript/TypeChecker/Unify.hs+12

@@ -21,6 +21,7 @@ module Language.PureScript.TypeChecker.Unify (

2121 unifyRows,

2222 unifiesWith,

2323 replaceVarWithUnknown,

24+ replaceTypeWildcards,

2425 varIfUnknown

2526) where

2627

@@ -157,6 +158,17 @@ replaceVarWithUnknown :: String -> Type -> UnifyT Type Check Type

157158replaceVarWithUnknown ident ty = do

158159 tu <- fresh

159160 return $ replaceTypeVars ident tu ty

161+

162+-- |

163+-- Replace type wildcards with unknowns

164+--

165+replaceTypeWildcards :: Type -> UnifyT t Check Type

166+replaceTypeWildcards = everywhereOnTypesM replace

167+ where

168+ replace TypeWildcard = do

169+ u <- fresh'

170+ return $ TUnknown u

171+ replace other = return other

160172

161173-- |

162174-- Replace outermost unsolved unification variables with named type variables

src/Language/PureScript/Types.hs+14

@@ -47,6 +47,10 @@ data Type

4747 --

4848 | TypeVar String

4949 -- |

50+ -- A type wildcard, as would appear in a partial type synonym

51+ --

52+ | TypeWildcard

53+ -- |

5054 -- A type constructor

5155 --

5256 | TypeConstructor (Qualified ProperName)

@@ -215,6 +219,16 @@ moveQuantifiersToFront = go [] []

215219 [] -> constrained

216220 qs' -> foldl (\ty' (q, sco) -> ForAll q ty' sco) constrained qs'

217221

222+-- |

223+-- Check if a type contains wildcards

224+--

225+containsWildcards :: Type -> Bool

226+containsWildcards = everythingOnTypes (||) go

227+ where

228+ go :: Type -> Bool

229+ go TypeWildcard = True

230+ go _ = False

231+

218232--

219233-- Traversals

220234--