90a755f · rowtype-yoga/purescript-native

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

on golang help sign in

Disallow constraint generalization for recursive functions.

90a755fPhil Freeman11 years ago

examples/failing/Generalization1.pursnew file+11

compare with golang

unifiedsplit

@@ -0,0 +1,11 @@

1+-- @shouldFailWith CannotGeneralizeRecursiveFunction

2+module Main where

4+import Prelude

6+foo 0 x _ = x

7+foo n x y = x <> bar (n - 1) x y

9+bar 0 x _ = x

10+bar n x y = y <> foo (n - 1) x y

11+

examples/failing/Generalization2.pursnew file+8

@@ -0,0 +1,8 @@

1+-- @shouldFailWith CannotGeneralizeRecursiveFunction

2+module Main where

4+import Prelude

6+test n m | n <= 1 = m

7+ | otherwise = test (n - 1) (m <> m)

examples/passing/Generalization1.pursnew file+10

@@ -0,0 +1,10 @@

1+module Main where

3+import Prelude

4+import Control.Monad.Eff.Console (print)

6+main = do

7+ print (sum 1.0 2.0)

8+ print (sum 1 2)

10+sum x y = x + y

src/Language/PureScript/Errors.hs+11−1

@@ -149,6 +149,7 @@ data SimpleErrorMessage

149 | IncorrectAnonymousArgument

150 | InvalidOperatorInBinder Ident Ident

151 | DeprecatedRequirePath

152+ | CannotGeneralizeRecursiveFunction Ident Type

152 deriving (Show)

153 deriving (Show)

153

154

154-- | Error message hints, providing more detailed information about failure.

155-- | Error message hints, providing more detailed information about failure.

@@ -330,6 +331,7 @@ errorCode em = case unwrapErrorMessage em of

330 IncorrectAnonymousArgument -> "IncorrectAnonymousArgument"

331 IncorrectAnonymousArgument -> "IncorrectAnonymousArgument"

331 InvalidOperatorInBinder{} -> "InvalidOperatorInBinder"

332 InvalidOperatorInBinder{} -> "InvalidOperatorInBinder"

332 DeprecatedRequirePath{} -> "DeprecatedRequirePath"

333 DeprecatedRequirePath{} -> "DeprecatedRequirePath"

334+ CannotGeneralizeRecursiveFunction{} -> "CannotGeneralizeRecursiveFunction"

333

335

334-- |

336-- |

335-- A stack trace for an error

337-- A stack trace for an error

@@ -420,6 +422,7 @@ onTypesInErrorMessageM f (ErrorMessage hints simple) = ErrorMessage <$> traverse

420 gSimple (OrphanInstance nm cl ts) = OrphanInstance nm cl <$> traverse f ts

422 gSimple (OrphanInstance nm cl ts) = OrphanInstance nm cl <$> traverse f ts

421 gSimple (WildcardInferredType ty) = WildcardInferredType <$> f ty

423 gSimple (WildcardInferredType ty) = WildcardInferredType <$> f ty

422 gSimple (MissingTypeDeclaration nm ty) = MissingTypeDeclaration nm <$> f ty

424 gSimple (MissingTypeDeclaration nm ty) = MissingTypeDeclaration nm <$> f ty

425+ gSimple (CannotGeneralizeRecursiveFunction nm ty) = CannotGeneralizeRecursiveFunction nm <$> f ty

423

426

424 gSimple other = pure other

427 gSimple other = pure other

425

428

@@ -981,6 +984,13 @@ prettyPrintSingleError full level showWiki e = flip evalState defaultUnknownMap

981 renderSimpleErrorMessage DeprecatedRequirePath =

984 renderSimpleErrorMessage DeprecatedRequirePath =

982 line "The require-path option is deprecated and will be removed in PureScript 0.9."

985 line "The require-path option is deprecated and will be removed in PureScript 0.9."

983

986

987+ renderSimpleErrorMessage (CannotGeneralizeRecursiveFunction ident ty) =

988+ paras [ line $ "Unable to generalize the type of the recursive function " ++ showIdent ident ++ "."

989+ , line $ "The inferred type of " ++ showIdent ident ++ " was:"

990+ , indent $ typeAsBox ty

991+ , line "Try adding a type signature."

992+ ]

993+

984 renderHint :: ErrorMessageHint -> Box.Box -> Box.Box

994 renderHint :: ErrorMessageHint -> Box.Box -> Box.Box

985 renderHint (ErrorUnifyingTypes t1 t2) detail =

995 renderHint (ErrorUnifyingTypes t1 t2) detail =

986 paras [ detail

996 paras [ detail

@@ -1202,7 +1212,7 @@ prettyPrintMultipleWarningsBox = prettyPrintMultipleErrorsWith Warning "Warning

1202

1212

1203-- | Pretty print errors as a Box

1213-- | Pretty print errors as a Box

1204prettyPrintMultipleErrorsBox :: Bool -> MultipleErrors -> [Box.Box]

1214prettyPrintMultipleErrorsBox :: Bool -> MultipleErrors -> [Box.Box]

1205−prettyPrintMultipleErrorsBox = prettyPrintMultipleErrorsWith Error "Error found:" "Error"

1215+prettyPrintMultipleErrorsBox = prettyPrintMultipleErrorsWith Error "Error found:" "Error"

1206

1216

1207prettyPrintMultipleErrorsWith :: Level -> String -> String -> Bool -> MultipleErrors -> [Box.Box]

1217prettyPrintMultipleErrorsWith :: Level -> String -> String -> Bool -> MultipleErrors -> [Box.Box]

1208prettyPrintMultipleErrorsWith level intro _ full (MultipleErrors [e]) =

1218prettyPrintMultipleErrorsWith level intro _ full (MultipleErrors [e]) =

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

@@ -234,7 +234,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkFixities ds

234 go (ValueDeclaration name nameKind [] (Right val)) =

235 warnAndRethrow (addHint (ErrorInValueDeclaration name)) $ do

236 valueIsNotDefined moduleName name

237− [(_, (val', ty))] <- typesOf moduleName [(name, val)]

237+ [(_, (val', ty))] <- typesOf NonRecursiveBindingGroup moduleName [(name, val)]

238 addValue moduleName name ty nameKind

239 return $ ValueDeclaration name nameKind [] $ Right val'

240 go ValueDeclaration{} = internalError "Binders were not desugared"

@@ -242,7 +242,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkFixities ds

242 warnAndRethrow (addHint (ErrorInBindingGroup (map (\(ident, _, _) -> ident) vals))) $ do

243 for_ (map (\(ident, _, _) -> ident) vals) $ \name ->

244 valueIsNotDefined moduleName name

245− tys <- typesOf moduleName $ map (\(ident, _, ty) -> (ident, ty)) vals

245+ tys <- typesOf RecursiveBindingGroup moduleName $ map (\(ident, _, ty) -> (ident, ty)) vals

246 vals' <- forM [ (name, val, nameKind, ty)

247 | (name, nameKind, _) <- vals

248 , (name', (val, ty)) <- tys

src/Language/PureScript/TypeChecker/Types.hs+22−6

@@ -7,9 +7,10 @@

7-- |

8-- This module implements the type checker

9--

10−module Language.PureScript.TypeChecker.Types (

10+module Language.PureScript.TypeChecker.Types

11+ ( BindingGroupType(..)

11− typesOf

12+ , typesOf

12−) where

13+ ) where

14{-

15{-

15 The following functions represent the corresponding type checking judgements:

16 The following functions represent the corresponding type checking judgements:

@@ -59,14 +60,20 @@ import Language.PureScript.TypeChecker.Unify

59import Language.PureScript.TypeClassDictionaries

60import Language.PureScript.TypeClassDictionaries

60import Language.PureScript.Types

61import Language.PureScript.Types

63+data BindingGroupType

64+ = RecursiveBindingGroup

65+ | NonRecursiveBindingGroup

66+ deriving (Show, Eq, Ord)

67+

62-- | Infer the types of multiple mutually-recursive values, and return elaborated values including

68-- | Infer the types of multiple mutually-recursive values, and return elaborated values including

63-- type class dictionaries and type annotations.

69-- type class dictionaries and type annotations.

64typesOf ::

70typesOf ::

65 (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

71 (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

72+ BindingGroupType ->

66 ModuleName ->

73 ModuleName ->

67 [(Ident, Expr)] ->

74 [(Ident, Expr)] ->

68 m [(Ident, (Expr, Type))]

75 m [(Ident, (Expr, Type))]

69−typesOf moduleName vals = do

76+typesOf bindingGroupType moduleName vals = do

70 tys <- fmap tidyUp . liftUnifyWarnings replace $ do

77 tys <- fmap tidyUp . liftUnifyWarnings replace $ do

71 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName vals

78 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName vals

72 ds1 <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict

79 ds1 <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict

@@ -79,14 +86,23 @@ typesOf moduleName vals = do

79 let unsolvedTypeVars = nub $ unknownsInType ty

86 let unsolvedTypeVars = nub $ unknownsInType ty

80 -- Generalize and constrain the type

87 -- Generalize and constrain the type

81 let generalized = generalize unsolved ty

88 let generalized = generalize unsolved ty

82− -- Make sure any unsolved type constraints only use type variables which appear

89+

83− -- unknown in the inferred type.

84 when shouldGeneralize $ do

90 when shouldGeneralize $ do

91+ -- Show the inferred type in a warning

85 tell . errorMessage $ MissingTypeDeclaration ident generalized

92 tell . errorMessage $ MissingTypeDeclaration ident generalized

93+ -- For non-recursive binding groups, can generalize over constraints.

94+ -- For recursive binding groups, we throw an error here for now.

95+ when (bindingGroupType == RecursiveBindingGroup && not (null unsolved))

96+ . throwError

97+ . errorMessage

98+ $ CannotGeneralizeRecursiveFunction ident generalized

99+ -- Make sure any unsolved type constraints only use type variables which appear

100+ -- unknown in the inferred type.

86 forM_ unsolved $ \(_, (className, classTys)) -> do

101 forM_ unsolved $ \(_, (className, classTys)) -> do

87 let constraintTypeVars = nub $ foldMap unknownsInType classTys

102 let constraintTypeVars = nub $ foldMap unknownsInType classTys

88 when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $

103 when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $

89 throwError . errorMessage $ NoInstanceFound className classTys

104 throwError . errorMessage $ NoInstanceFound className classTys

105+

90 -- Check skolem variables did not escape their scope

106 -- Check skolem variables did not escape their scope

91 skolemEscapeCheck val'

107 skolemEscapeCheck val'

92 -- Check rows do not contain duplicate labels

108 -- Check rows do not contain duplicate labels