427c2a2 · rowtype-yoga/purescript-native

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

on golang help sign in

Type directed search (#2352)

427c2a2Christoph Hegemann10 years ago

purescript.cabal+1

compare with golang

unifiedsplit

@@ -238,6 +238,7 @@ library

238 Language.PureScript.TypeChecker.Subsumption

239 Language.PureScript.TypeChecker.Synonyms

240 Language.PureScript.TypeChecker.Types

241+ Language.PureScript.TypeChecker.TypeSearch

241 Language.PureScript.TypeChecker.Unify

242 Language.PureScript.TypeChecker.Unify

242 Language.PureScript.TypeClassDictionaries

243 Language.PureScript.TypeClassDictionaries

243 Language.PureScript.Types

244 Language.PureScript.Types

src/Control/Monad/Supply.hs+2−1

@@ -7,6 +7,7 @@ module Control.Monad.Supply where

8import Prelude.Compat

10+import Control.Applicative

10import Control.Monad.Error.Class (MonadError(..))

11import Control.Monad.Error.Class (MonadError(..))

11import Control.Monad.Reader

12import Control.Monad.Reader

12import Control.Monad.State

13import Control.Monad.State

@@ -15,7 +16,7 @@ import Control.Monad.Writer

15import Data.Functor.Identity

16import Data.Functor.Identity

17newtype SupplyT m a = SupplyT { unSupplyT :: StateT Integer m a }

18newtype SupplyT m a = SupplyT { unSupplyT :: StateT Integer m a }

18− deriving (Functor, Applicative, Monad, MonadTrans, MonadError e, MonadWriter w, MonadReader r)

19+ deriving (Functor, Applicative, Monad, MonadTrans, MonadError e, MonadWriter w, MonadReader r, Alternative, MonadPlus)

20runSupplyT :: Integer -> SupplyT m a -> m (a, Integer)

21runSupplyT :: Integer -> SupplyT m a -> m (a, Integer)

21runSupplyT n = flip runStateT n . unSupplyT

22runSupplyT n = flip runStateT n . unSupplyT

src/Control/Monad/Supply/Class.hs+11−5

@@ -1,6 +1,9 @@

1-- |

2-- A class for monads supporting a supply of fresh names

3--

5+{-# LANGUAGE DefaultSignatures #-}

4module Control.Monad.Supply.Class where

7module Control.Monad.Supply.Class where

6import Prelude.Compat

9import Prelude.Compat

@@ -11,18 +14,21 @@ import Control.Monad.Writer

12class Monad m => MonadSupply m where

15class Monad m => MonadSupply m where

13 fresh :: m Integer

16 fresh :: m Integer

17+ peek :: m Integer

18+ default fresh :: MonadTrans t => t m Integer

19+ fresh = lift fresh

20+ default peek :: MonadTrans t => t m Integer

21+ peek = lift peek

15instance Monad m => MonadSupply (SupplyT m) where

23instance Monad m => MonadSupply (SupplyT m) where

16 fresh = SupplyT $ do

24 fresh = SupplyT $ do

17 n <- get

25 n <- get

18 put (n + 1)

26 put (n + 1)

19 return n

27 return n

28+ peek = SupplyT get

21−instance MonadSupply m => MonadSupply (StateT s m) where

30+instance MonadSupply m => MonadSupply (StateT s m)

22− fresh = lift fresh

23−

24−instance (Monoid w, MonadSupply m) => MonadSupply (WriterT w m) where

31+instance (Monoid w, MonadSupply m) => MonadSupply (WriterT w m)

25− fresh = lift fresh

27freshName :: MonadSupply m => m String

33freshName :: MonadSupply m => m String

28freshName = fmap (('$' :) . show) fresh

34freshName = fmap (('$' :) . show) fresh

src/Language/PureScript/AST/Declarations.hs+10−1

@@ -29,6 +29,15 @@ import qualified Text.Parsec as P

29-- | A map of locally-bound names in scope.

30type Context = [(Ident, Type)]

32+-- | Holds the data necessary to do type directed search for typed holes

33+data TypeSearch

34+ = TSBefore Environment

35+ -- ^ An Environment captured for later consumption by type directed search

36+ | TSAfter [(Qualified Ident, Type)]

37+ -- ^ Results of applying type directed search to the previously captured

38+ -- Environment

39+ deriving Show

40+

32-- | A type of error messages

41-- | A type of error messages

33data SimpleErrorMessage

42data SimpleErrorMessage

34 = ErrorParsingFFIModule FilePath (Maybe Bundle.ErrorMessage)

43 = ErrorParsingFFIModule FilePath (Maybe Bundle.ErrorMessage)

@@ -99,7 +108,7 @@ data SimpleErrorMessage

99 | ShadowedTypeVar String

108 | ShadowedTypeVar String

100 | UnusedTypeVar String

109 | UnusedTypeVar String

101 | WildcardInferredType Type Context

110 | WildcardInferredType Type Context

102− | HoleInferredType String Type Context

111+ | HoleInferredType String Type Context TypeSearch

103 | MissingTypeDeclaration Ident Type

112 | MissingTypeDeclaration Ident Type

104 | OverlappingPattern [[Binder]] Bool

113 | OverlappingPattern [[Binder]] Bool

105 | IncompleteExhaustivityCheck

114 | IncompleteExhaustivityCheck

src/Language/PureScript/AST/Traversals.hs+12

@@ -586,3 +586,15 @@ accumTypes f = everythingOnValues mappend forDecls forValues (const mempty) (con

586 forValues (DeferredDictionary _ tys) = mconcat (map f tys)

587 forValues (TypedValue _ _ ty) = f ty

588 forValues _ = mempty

589+

590+-- |

591+-- Map a function over type annotations appearing inside a value

592+--

593+overTypes :: (Type -> Type) -> Expr -> Expr

594+overTypes f = let (_, f', _) = everywhereOnValues id g id in f'

595+ where

596+ g :: Expr -> Expr

597+ g (TypedValue checkTy val t) = TypedValue checkTy val (f t)

598+ g (TypeClassDictionary c sco hints) = TypeClassDictionary (mapConstraintArgs (map f) c) sco hints

599+ g other = other

600+

src/Language/PureScript/Errors.hs+30−5

@@ -40,6 +40,7 @@ import qualified System.Console.ANSI as ANSI

40import qualified Text.Parsec as P

41import qualified Text.Parsec.Error as PE

42import qualified Text.PrettyPrint.Boxes as Box

43+import qualified Language.PureScript.Publish.BoxesHelpers as BoxHelpers

43import Text.Parsec.Error (Message(..))

44import Text.Parsec.Error (Message(..))

45newtype ErrorSuggestion = ErrorSuggestion String

46newtype ErrorSuggestion = ErrorSuggestion String

@@ -266,7 +267,7 @@ onTypesInErrorMessageM f (ErrorMessage hints simple) = ErrorMessage <$> traverse

266 gSimple (ExpectedType ty k) = ExpectedType <$> f ty <*> pure k

267 gSimple (ExpectedType ty k) = ExpectedType <$> f ty <*> pure k

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

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

268 gSimple (WildcardInferredType ty ctx) = WildcardInferredType <$> f ty <*> traverse (sndM f) ctx

269 gSimple (WildcardInferredType ty ctx) = WildcardInferredType <$> f ty <*> traverse (sndM f) ctx

269− gSimple (HoleInferredType name ty ctx) = HoleInferredType name <$> f ty <*> traverse (sndM f) ctx

270+ gSimple (HoleInferredType name ty ctx env) = HoleInferredType name <$> f ty <*> traverse (sndM f) ctx <*> gTypeSearch env

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

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

271 gSimple (CannotGeneralizeRecursiveFunction nm ty) = CannotGeneralizeRecursiveFunction nm <$> f ty

272 gSimple (CannotGeneralizeRecursiveFunction nm ty) = CannotGeneralizeRecursiveFunction nm <$> f ty

272 gSimple other = pure other

273 gSimple other = pure other

@@ -280,6 +281,9 @@ onTypesInErrorMessageM f (ErrorMessage hints simple) = ErrorMessage <$> traverse

280 gHint (ErrorSolvingConstraint con) = ErrorSolvingConstraint <$> overConstraintArgs (traverse f) con

281 gHint (ErrorSolvingConstraint con) = ErrorSolvingConstraint <$> overConstraintArgs (traverse f) con

281 gHint other = pure other

282 gHint other = pure other

282

283

284+ gTypeSearch (TSBefore env) = pure (TSBefore env)

285+ gTypeSearch (TSAfter result) = TSAfter <$> traverse (traverse f) result

286+

283wikiUri :: ErrorMessage -> String

287wikiUri :: ErrorMessage -> String

284wikiUri e = "https://github.com/purescript/purescript/wiki/Error-Code-" ++ errorCode e

288wikiUri e = "https://github.com/purescript/purescript/wiki/Error-Code-" ++ errorCode e

285

289

@@ -733,10 +737,31 @@ prettyPrintSingleError (PPEOptions codeColor full level showWiki) e = flip evalS

733 paras $ [ line "Wildcard type definition has the inferred type "

737 paras $ [ line "Wildcard type definition has the inferred type "

734 , markCodeBox $ indent $ typeAsBox ty

738 , markCodeBox $ indent $ typeAsBox ty

735 ] ++ renderContext ctx

739 ] ++ renderContext ctx

736− renderSimpleErrorMessage (HoleInferredType name ty ctx) =

740+ renderSimpleErrorMessage (HoleInferredType name ty ctx ts) =

741+ let

742+ maxTSResults = 15

743+ tsResult = case ts of

744+ (TSAfter idents) | not (null idents) ->

745+ let

746+ formatTS (names, types) =

747+ let

748+ idBoxes = Box.text . showQualified runIdent <$> names

749+ tyBoxes = (\t -> BoxHelpers.indented

750+ (Box.text ":: " Box.<> typeAsBox t)) <$> types

751+ longestId = maximum (map Box.cols idBoxes)

752+ in

753+ Box.vcat Box.top $

754+ zipWith (Box.<>)

755+ (Box.alignHoriz Box.left longestId <$> idBoxes)

756+ tyBoxes

757+ in [ line "You could substitute the hole with one of these values:"

758+ , markCodeBox (indent (formatTS (unzip (take maxTSResults idents))))

759+ ]

760+ _ -> []

761+ in

737− paras $ [ line $ "Hole '" ++ markCode name ++ "' has the inferred type "

762+ paras $ [ line $ "Hole '" ++ markCode name ++ "' has the inferred type "

738− , markCodeBox $ indent $ typeAsBox ty

763+ , markCodeBox (indent (typeAsBox ty))

739− ] ++ renderContext ctx

764+ ] ++ tsResult ++ renderContext ctx

740 renderSimpleErrorMessage (MissingTypeDeclaration ident ty) =

765 renderSimpleErrorMessage (MissingTypeDeclaration ident ty) =

741 paras [ line $ "No type declaration was provided for the top-level declaration of " ++ markCode (showIdent ident) ++ "."

766 paras [ line $ "No type declaration was provided for the top-level declaration of " ++ markCode (showIdent ident) ++ "."

742 , line "It is good practice to provide type declarations as a form of documentation."

767 , line "It is good practice to provide type declarations as a form of documentation."

src/Language/PureScript/TypeChecker/TypeSearch.hsnew file+73

@@ -0,0 +1,73 @@

1+{-# LANGUAGE NoImplicitPrelude #-}

2+{-# LANGUAGE OverloadedStrings #-}

3+{-# LANGUAGE RecordWildCards #-}

5+module Language.PureScript.TypeChecker.TypeSearch

6+ ( typeSearch

7+ ) where

9+import Protolude

10+

11+import Control.Monad.Writer

12+import qualified Data.Map as Map

13+import qualified Language.PureScript.TypeChecker.Entailment as Entailment

14+

15+import qualified Language.PureScript.TypeChecker.Monad as TC

16+import Language.PureScript.TypeChecker.Subsumption

17+import Language.PureScript.TypeChecker.Unify as P

18+

19+import Control.Monad.Supply as P

20+import Language.PureScript.AST as P

21+import Language.PureScript.Environment as P

22+import Language.PureScript.Names as P

23+import Language.PureScript.TypeChecker.Skolems as Skolem

24+import Language.PureScript.TypeChecker.Synonyms as P

25+import Language.PureScript.Types as P

26+

27+checkInEnvironment

28+ :: Environment

29+ -> Integer

30+ -> StateT TC.CheckState (SupplyT (WriterT b (Except e))) a

31+ -> Maybe (a, Environment)

32+checkInEnvironment env nextVar =

33+ either (const Nothing) Just

34+ . runExcept

35+ . evalWriterT

36+ . P.evalSupplyT nextVar

37+ . TC.runCheck' env

38+

39+evalWriterT :: Monad m => WriterT b m r -> m r

40+evalWriterT m = liftM fst (runWriterT m)

41+

42+checkSubsume

43+ :: P.Environment

44+ -- ^ The Environment which contains the relevant definitions and typeclasses

45+ -> Integer

46+ -> P.Type

47+ -- ^ The user supplied type

48+ -> P.Type

49+ -- ^ The type supplied by the environment

50+ -> Maybe ((P.Expr, [(P.Ident, P.Constraint)]), P.Environment)

51+checkSubsume env nextVar userT envT = checkInEnvironment env nextVar $ do

52+ let initializeSkolems =

53+ Skolem.introduceSkolemScope

54+ <=< P.replaceAllTypeSynonyms

55+ <=< P.replaceTypeWildcards

56+

57+ userT' <- initializeSkolems userT

58+ envT' <- initializeSkolems envT

59+

60+ let dummyExpression = P.Var (P.Qualified Nothing (P.Ident "x"))

61+

62+ elab <- subsumes envT' userT'

63+ subst <- gets TC.checkSubstitution

64+ let expP = P.overTypes (P.substituteType subst) (elab dummyExpression)

65+ Entailment.replaceTypeClassDictionaries False expP

66+

67+typeSearch

68+ :: P.Environment

69+ -> Integer

70+ -> P.Type

71+ -> Map (P.Qualified P.Ident) P.Type

72+typeSearch env nextVar type' =

73+ Map.mapMaybe (\(x, _, _) -> checkSubsume env nextVar type' x $> x) (P.names env)

src/Language/PureScript/TypeChecker/Types.hs+27−17

@@ -31,7 +31,7 @@ import Control.Arrow (second)

31import Control.Monad

32import Control.Monad.Error.Class (MonadError(..))

33import Control.Monad.State.Class (MonadState(..), gets)

34−import Control.Monad.Supply.Class (MonadSupply)

34+import Control.Monad.Supply.Class (MonadSupply, peek)

35import Control.Monad.Writer.Class (MonadWriter(..))

37import Data.Bifunctor (bimap)

@@ -55,9 +55,11 @@ import Language.PureScript.TypeChecker.Rows

55import Language.PureScript.TypeChecker.Skolems

56import Language.PureScript.TypeChecker.Subsumption

57import Language.PureScript.TypeChecker.Synonyms

58+import Language.PureScript.TypeChecker.TypeSearch

58import Language.PureScript.TypeChecker.Unify

59import Language.PureScript.TypeChecker.Unify

59import Language.PureScript.Types

60import Language.PureScript.Types

62+

61data BindingGroupType

63data BindingGroupType

62 = RecursiveBindingGroup

64 = RecursiveBindingGroup

63 | NonRecursiveBindingGroup

65 | NonRecursiveBindingGroup

@@ -72,6 +74,10 @@ typesOf

72 -> [(Ident, Expr)]

74 -> [(Ident, Expr)]

73 -> m [(Ident, (Expr, Type))]

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

74typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do

76typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do

77+ -- TODO: If we push withoutWarnings into the do block we can differentiate

78+ -- between ds1 and ds2 warnings and capture shouldGeneralize and the unsolved

79+ -- dictionaries

80+ -- Careful: We need to make sure the capturingSubstitution still does the right thing

75 (tys, w) <- withoutWarnings . capturingSubstitution tidyUp $ do

81 (tys, w) <- withoutWarnings . capturingSubstitution tidyUp $ do

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

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

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

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

@@ -106,8 +112,9 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do

106 TypeClassData{ typeClassDependencies } <- gets (findClass . typeClasses . checkEnv)

112 TypeClassData{ typeClassDependencies } <- gets (findClass . typeClasses . checkEnv)

107 let solved = foldMap (S.fromList . fdDetermined) typeClassDependencies

113 let solved = foldMap (S.fromList . fdDetermined) typeClassDependencies

108 let constraintTypeVars = nub . foldMap (unknownsInType . fst) . filter ((`notElem` solved) . snd) $ zip (constraintArgs con) [0..]

114 let constraintTypeVars = nub . foldMap (unknownsInType . fst) . filter ((`notElem` solved) . snd) $ zip (constraintArgs con) [0..]

109− when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $

115+ when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $ do

116+ nextVar <- peek

110− throwError . onErrorMessages (replaceTypes currentSubst) . errorMessage $ NoInstanceFound con

117+ throwError . onErrorMessages (replaceTypes (not shouldGeneralize) currentSubst nextVar) . errorMessage $ NoInstanceFound con

111

118

112 -- Check skolem variables did not escape their scope

119 -- Check skolem variables did not escape their scope

113 skolemEscapeCheck val'

120 skolemEscapeCheck val'

@@ -118,11 +125,24 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do

118 -- Show warnings here, since types in wildcards might have been solved during

125 -- Show warnings here, since types in wildcards might have been solved during

119 -- instance resolution (by functional dependencies).

126 -- instance resolution (by functional dependencies).

120 finalSubst <- gets checkSubstitution

127 finalSubst <- gets checkSubstitution

128+

129+ -- TODO: We should only do type search for Typed Holes which we inferred

130+ -- without generalizing type class constraints

131+ -- eg. foldMap ?x [1, 2, 3] finds `negate` right now, which is wrong

132+

133+ nextVar <- peek

121− escalateWarningWhen isHoleError . tell . onErrorMessages (replaceTypes finalSubst) $ w

134+ escalateWarningWhen isHoleError . tell . onErrorMessages (replaceTypes True finalSubst nextVar) $ w

122

135

123 return inferred

136 return inferred

124 where

137 where

138+ replaceTypes shouldRunTypeSearch subst nextVar =

139+ (if shouldRunTypeSearch then runTypeSearch else id)

125− replaceTypes subst = onTypesInErrorMessage (substituteType subst)

140+ . onTypesInErrorMessage (substituteType subst)

141+ where

142+ runTypeSearch (ErrorMessage hints (HoleInferredType x ty y (TSBefore env))) =

143+ ErrorMessage hints (HoleInferredType x ty y $ TSAfter $

144+ fmap (substituteType subst) <$> M.toList (typeSearch env nextVar (substituteType subst ty)))

145+ runTypeSearch x = x

126

146

127 -- | Generalize type vars using forall and add inferred constraints

147 -- | Generalize type vars using forall and add inferred constraints

128 generalize unsolved = varIfUnknown . constrain unsolved

148 generalize unsolved = varIfUnknown . constrain unsolved

@@ -207,17 +227,6 @@ isTyped (name, PositionedValue pos c value) =

207 (isTyped (name, value))

227 (isTyped (name, value))

208isTyped (name, value) = Left (name, value)

228isTyped (name, value) = Left (name, value)

209

229

210−-- |

211−-- Map a function over type annotations appearing inside a value

212−--

213−overTypes :: (Type -> Type) -> Expr -> Expr

214−overTypes f = let (_, f', _) = everywhereOnValues id g id in f'

215− where

216− g :: Expr -> Expr

217− g (TypedValue checkTy val t) = TypedValue checkTy val (f t)

218− g (TypeClassDictionary c sco hints) = TypeClassDictionary (mapConstraintArgs (map f) c) sco hints

219− g other = other

220−

221-- | Check the kind of a type, failing if it is not of kind *.

230-- | Check the kind of a type, failing if it is not of kind *.

222checkTypeKind ::

231checkTypeKind ::

223 (MonadError MultipleErrors m) =>

232 (MonadError MultipleErrors m) =>

@@ -345,7 +354,8 @@ infer' (TypedValue checkType val ty) = do

345infer' (Hole name) = do

354infer' (Hole name) = do

346 ty <- freshType

355 ty <- freshType

347 ctx <- getLocalContext

356 ctx <- getLocalContext

357+ env <- getEnv

348− tell . errorMessage $ HoleInferredType name ty ctx

358+ tell . errorMessage $ HoleInferredType name ty ctx (TSBefore env)

349 return $ TypedValue True (Hole name) ty

359 return $ TypedValue True (Hole name) ty

350infer' (PositionedValue pos c val) = warnAndRethrowWithPositionTC pos $ do

360infer' (PositionedValue pos c val) = warnAndRethrowWithPositionTC pos $ do

351 TypedValue t v ty <- infer' val

361 TypedValue t v ty <- infer' val