90a755f · rowtype-yoga/purescript-native

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

Disallow constraint generalization for recursive functions.

Fix #1978, disallow constraint generalization for recursive functions.

commit90a755f6db79bdc2dff4df641b3c38e74e66cb52 authorPhil Freeman <paf31@cantab.net> dateTue 5 Apr 2016, 19:49 (11 years ago) parentcf11462

6 files changed+64−9

compare with golang

unifiedsplit

examples/failing/Generalization1.purs+11 examples/failing/Generalization2.purs+8 examples/passing/Generalization1.purs+10 src/Language/PureScript/Errors.hs+11−1 src/Language/PureScript/TypeChecker.hs+2−2 src/Language/PureScript/TypeChecker/Types.hs+22−6

examples/failing/Generalization1.pursnew file+11

@@ -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

149149 | IncorrectAnonymousArgument

150150 | InvalidOperatorInBinder Ident Ident

151151 | DeprecatedRequirePath

152+ | CannotGeneralizeRecursiveFunction Ident Type

152153 deriving (Show)

153154

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

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

330331 IncorrectAnonymousArgument -> "IncorrectAnonymousArgument"

331332 InvalidOperatorInBinder{} -> "InvalidOperatorInBinder"

332333 DeprecatedRequirePath{} -> "DeprecatedRequirePath"

334+ CannotGeneralizeRecursiveFunction{} -> "CannotGeneralizeRecursiveFunction"

333335

334336-- |

335337-- A stack trace for an error

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

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

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

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

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

423426

424427 gSimple other = pure other

425428

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

981984 renderSimpleErrorMessage DeprecatedRequirePath =

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

983986

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+

984994 renderHint :: ErrorMessageHint -> Box.Box -> Box.Box

985995 renderHint (ErrorUnifyingTypes t1 t2) detail =

986996 paras [ detail

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

12021212

12031213-- | Pretty print errors as a Box

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

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

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

12061216

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

12081218prettyPrintMultipleErrorsWith 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

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

235235 warnAndRethrow (addHint (ErrorInValueDeclaration name)) $ do

236236 valueIsNotDefined moduleName name

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

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

238238 addValue moduleName name ty nameKind

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

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

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

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

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

244244 valueIsNotDefined moduleName name

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

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

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

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

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

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

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

77-- |

88-- This module implements the type checker

99--

10−module Language.PureScript.TypeChecker.Types (

11− typesOf

12−) where

10+module Language.PureScript.TypeChecker.Types

11+ ( BindingGroupType(..)

12+ , typesOf

13+ ) where

1314

1415{-

1516 The following functions represent the corresponding type checking judgements:

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

5960import Language.PureScript.TypeClassDictionaries

6061import Language.PureScript.Types

6162

63+data BindingGroupType

64+ = RecursiveBindingGroup

65+ | NonRecursiveBindingGroup

66+ deriving (Show, Eq, Ord)

67+

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

6369-- type class dictionaries and type annotations.

6470typesOf ::

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

72+ BindingGroupType ->

6673 ModuleName ->

6774 [(Ident, Expr)] ->

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

69−typesOf moduleName vals = do

76+typesOf bindingGroupType moduleName vals = do

7077 tys <- fmap tidyUp . liftUnifyWarnings replace $ do

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

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

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

7986 let unsolvedTypeVars = nub $ unknownsInType ty

8087 -- Generalize and constrain the type

8188 let generalized = generalize unsolved ty

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

83− -- unknown in the inferred type.

89+

8490 when shouldGeneralize $ do

91+ -- Show the inferred type in a warning

8592 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.

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

87102 let constraintTypeVars = nub $ foldMap unknownsInType classTys

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

89104 throwError . errorMessage $ NoInstanceFound className classTys

105+

90106 -- Check skolem variables did not escape their scope

91107 skolemEscapeCheck val'

92108 -- Check rows do not contain duplicate labels