git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Type directed search (#2352)

* initial version of type search on holes * also display type info * apply the substitution to local definitions aswell * clean up typed hole code * don't crash on Rank-N-Types, fix warnings * fix merge conflicts * adds haddock comments for TypeSearch * improve rendering of typesearch * Infernal -> TypeChecker.TypeSearch removes eventual psc-ide code * comment on dummyExpression also don't generalize constraints when typesearching * stylish haskell * do not run type search when generalizing * run `filtering` with the captured substitution rules out correct solutions right now * Revert "run `filtering` with the captured substitution" This reverts commit 2221fe0b707b3a4a539a8cbbe3bcc5abed4256b5. * merges * cleaned up * capture current SupplyT and pass it to typesearch this is so that we don't overlap the type variables * clear up which type is coming from the Environment * only show type search suggestions if we have any limits the maximum number of suggestions to 15

commit427c2a27fc17f455fff1607cac92e061498c7105 authorChristoph Hegemann <kRITZCREEK@users.noreply.github.com> dateWed 12 Oct 2016, 05:38 (10 years ago) parent61019d0
8 files changed+166−29
compare with golang
unifiedsplit
purescript.cabal+1 src/Control/Monad/Supply.hs+2−1 src/Control/Monad/Supply/Class.hs+11−5 src/Language/PureScript/AST/Declarations.hs+10−1 src/Language/PureScript/AST/Traversals.hs+12 src/Language/PureScript/Errors.hs+30−5 src/Language/PureScript/TypeChecker/TypeSearch.hs+73 src/Language/PureScript/TypeChecker/Types.hs+27−17
purescript.cabal+1
@@ -238,6 +238,7 @@ library
238238 Language.PureScript.TypeChecker.Subsumption
239239 Language.PureScript.TypeChecker.Synonyms
240240 Language.PureScript.TypeChecker.Types
241+ Language.PureScript.TypeChecker.TypeSearch
241242 Language.PureScript.TypeChecker.Unify
242243 Language.PureScript.TypeClassDictionaries
243244 Language.PureScript.Types
src/Control/Monad/Supply.hs+2−1
@@ -7,6 +7,7 @@ module Control.Monad.Supply where
77
88import Prelude.Compat
99
10+import Control.Applicative
1011import Control.Monad.Error.Class (MonadError(..))
1112import Control.Monad.Reader
1213import Control.Monad.State
@@ -15,7 +16,7 @@ import Control.Monad.Writer
1516import Data.Functor.Identity
1617
1718newtype 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)
1920
2021runSupplyT :: Integer -> SupplyT m a -> m (a, Integer)
2122runSupplyT n = flip runStateT n . unSupplyT
src/Control/Monad/Supply/Class.hs+11−5
@@ -1,6 +1,9 @@
11-- |
22-- A class for monads supporting a supply of fresh names
33--
4+
5+{-# LANGUAGE DefaultSignatures #-}
6+
47module Control.Monad.Supply.Class where
58
69import Prelude.Compat
@@ -11,18 +14,21 @@ import Control.Monad.Writer
1114
1215class Monad m => MonadSupply m where
1316 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
1422
1523instance Monad m => MonadSupply (SupplyT m) where
1624 fresh = SupplyT $ do
1725 n <- get
1826 put (n + 1)
1927 return n
28+ peek = SupplyT get
2029
21−instance MonadSupply m => MonadSupply (StateT s m) where
22− fresh = lift fresh
23−
24−instance (Monoid w, MonadSupply m) => MonadSupply (WriterT w m) where
25− fresh = lift fresh
30+instance MonadSupply m => MonadSupply (StateT s m)
31+instance (Monoid w, MonadSupply m) => MonadSupply (WriterT w m)
2632
2733freshName :: MonadSupply m => m String
2834freshName = fmap (('$' :) . show) fresh
src/Language/PureScript/AST/Declarations.hs+10−1
@@ -29,6 +29,15 @@ import qualified Text.Parsec as P
2929-- | A map of locally-bound names in scope.
3030type Context = [(Ident, Type)]
3131
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+
3241-- | A type of error messages
3342data SimpleErrorMessage
3443 = ErrorParsingFFIModule FilePath (Maybe Bundle.ErrorMessage)
@@ -99,7 +108,7 @@ data SimpleErrorMessage
99108 | ShadowedTypeVar String
100109 | UnusedTypeVar String
101110 | WildcardInferredType Type Context
102− | HoleInferredType String Type Context
111+ | HoleInferredType String Type Context TypeSearch
103112 | MissingTypeDeclaration Ident Type
104113 | OverlappingPattern [[Binder]] Bool
105114 | IncompleteExhaustivityCheck
src/Language/PureScript/AST/Traversals.hs+12
@@ -586,3 +586,15 @@ accumTypes f = everythingOnValues mappend forDecls forValues (const mempty) (con
586586 forValues (DeferredDictionary _ tys) = mconcat (map f tys)
587587 forValues (TypedValue _ _ ty) = f ty
588588 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
4040import qualified Text.Parsec as P
4141import qualified Text.Parsec.Error as PE
4242import qualified Text.PrettyPrint.Boxes as Box
43+import qualified Language.PureScript.Publish.BoxesHelpers as BoxHelpers
4344import Text.Parsec.Error (Message(..))
4445
4546newtype ErrorSuggestion = ErrorSuggestion String
@@ -266,7 +267,7 @@ onTypesInErrorMessageM f (ErrorMessage hints simple) = ErrorMessage <$> traverse
266267 gSimple (ExpectedType ty k) = ExpectedType <$> f ty <*> pure k
267268 gSimple (OrphanInstance nm cl ts) = OrphanInstance nm cl <$> traverse f ts
268269 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
270271 gSimple (MissingTypeDeclaration nm ty) = MissingTypeDeclaration nm <$> f ty
271272 gSimple (CannotGeneralizeRecursiveFunction nm ty) = CannotGeneralizeRecursiveFunction nm <$> f ty
272273 gSimple other = pure other
@@ -280,6 +281,9 @@ onTypesInErrorMessageM f (ErrorMessage hints simple) = ErrorMessage <$> traverse
280281 gHint (ErrorSolvingConstraint con) = ErrorSolvingConstraint <$> overConstraintArgs (traverse f) con
281282 gHint other = pure other
282283
284+ gTypeSearch (TSBefore env) = pure (TSBefore env)
285+ gTypeSearch (TSAfter result) = TSAfter <$> traverse (traverse f) result
286+
283287wikiUri :: ErrorMessage -> String
284288wikiUri e = "https://github.com/purescript/purescript/wiki/Error-Code-" ++ errorCode e
285289
@@ -733,10 +737,31 @@ prettyPrintSingleError (PPEOptions codeColor full level showWiki) e = flip evalS
733737 paras $ [ line "Wildcard type definition has the inferred type "
734738 , markCodeBox $ indent $ typeAsBox ty
735739 ] ++ renderContext ctx
736− renderSimpleErrorMessage (HoleInferredType name ty ctx) =
737− paras $ [ line $ "Hole '" ++ markCode name ++ "' has the inferred type "
738− , markCodeBox $ indent $ typeAsBox ty
739− ] ++ renderContext 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
762+ paras $ [ line $ "Hole '" ++ markCode name ++ "' has the inferred type "
763+ , markCodeBox (indent (typeAsBox ty))
764+ ] ++ tsResult ++ renderContext ctx
740765 renderSimpleErrorMessage (MissingTypeDeclaration ident ty) =
741766 paras [ line $ "No type declaration was provided for the top-level declaration of " ++ markCode (showIdent ident) ++ "."
742767 , 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 #-}
4+
5+module Language.PureScript.TypeChecker.TypeSearch
6+ ( typeSearch
7+ ) where
8+
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)
3131import Control.Monad
3232import Control.Monad.Error.Class (MonadError(..))
3333import Control.Monad.State.Class (MonadState(..), gets)
34−import Control.Monad.Supply.Class (MonadSupply)
34+import Control.Monad.Supply.Class (MonadSupply, peek)
3535import Control.Monad.Writer.Class (MonadWriter(..))
3636
3737import Data.Bifunctor (bimap)
@@ -55,9 +55,11 @@ import Language.PureScript.TypeChecker.Rows
5555import Language.PureScript.TypeChecker.Skolems
5656import Language.PureScript.TypeChecker.Subsumption
5757import Language.PureScript.TypeChecker.Synonyms
58+import Language.PureScript.TypeChecker.TypeSearch
5859import Language.PureScript.TypeChecker.Unify
5960import Language.PureScript.Types
6061
62+
6163data BindingGroupType
6264 = RecursiveBindingGroup
6365 | NonRecursiveBindingGroup
@@ -72,6 +74,10 @@ typesOf
7274 -> [(Ident, Expr)]
7375 -> m [(Ident, (Expr, Type))]
7476typesOf 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
7581 (tys, w) <- withoutWarnings . capturingSubstitution tidyUp $ do
7682 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup (Just moduleName) vals
7783 ds1 <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
@@ -106,8 +112,9 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
106112 TypeClassData{ typeClassDependencies } <- gets (findClass . typeClasses . checkEnv)
107113 let solved = foldMap (S.fromList . fdDetermined) typeClassDependencies
108114 let constraintTypeVars = nub . foldMap (unknownsInType . fst) . filter ((`notElem` solved) . snd) $ zip (constraintArgs con) [0..]
109− when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $
110− throwError . onErrorMessages (replaceTypes currentSubst) . errorMessage $ NoInstanceFound con
115+ when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $ do
116+ nextVar <- peek
117+ throwError . onErrorMessages (replaceTypes (not shouldGeneralize) currentSubst nextVar) . errorMessage $ NoInstanceFound con
111118
112119 -- Check skolem variables did not escape their scope
113120 skolemEscapeCheck val'
@@ -118,11 +125,24 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
118125 -- Show warnings here, since types in wildcards might have been solved during
119126 -- instance resolution (by functional dependencies).
120127 finalSubst <- gets checkSubstitution
121− escalateWarningWhen isHoleError . tell . onErrorMessages (replaceTypes finalSubst) $ w
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
134+ escalateWarningWhen isHoleError . tell . onErrorMessages (replaceTypes True finalSubst nextVar) $ w
122135
123136 return inferred
124137 where
125− replaceTypes subst = onTypesInErrorMessage (substituteType subst)
138+ replaceTypes shouldRunTypeSearch subst nextVar =
139+ (if shouldRunTypeSearch then runTypeSearch else id)
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
126146
127147 -- | Generalize type vars using forall and add inferred constraints
128148 generalize unsolved = varIfUnknown . constrain unsolved
@@ -207,17 +227,6 @@ isTyped (name, PositionedValue pos c value) =
207227 (isTyped (name, value))
208228isTyped (name, value) = Left (name, value)
209229
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−
221230-- | Check the kind of a type, failing if it is not of kind *.
222231checkTypeKind ::
223232 (MonadError MultipleErrors m) =>
@@ -345,7 +354,8 @@ infer' (TypedValue checkType val ty) = do
345354infer' (Hole name) = do
346355 ty <- freshType
347356 ctx <- getLocalContext
348− tell . errorMessage $ HoleInferredType name ty ctx
357+ env <- getEnv
358+ tell . errorMessage $ HoleInferredType name ty ctx (TSBefore env)
349359 return $ TypedValue True (Hole name) ty
350360infer' (PositionedValue pos c val) = warnAndRethrowWithPositionTC pos $ do
351361 TypedValue t v ty <- infer' val