git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Fix issue with typed holes in inference mode (#2386)

* Fix issue with typed holes in inference mode * Fix issues arising from unification variable overlaps * remove import * Fixes after code review

commitda83efb94a6a50d4d29c73fa89a3e8fa0c4c9b76 authorPhil Freeman <paf31@cantab.net> dateThu 20 Oct 2016, 09:32 (10 years ago) parent26590bb
5 files changed+114−74
compare with golang
unifiedsplit
src/Language/PureScript/Make.hs+1−1 src/Language/PureScript/TypeChecker/Entailment.hs+34−22 src/Language/PureScript/TypeChecker/Monad.hs+3−3 src/Language/PureScript/TypeChecker/TypeSearch.hs+35−14 src/Language/PureScript/TypeChecker/Types.hs+41−34
src/Language/PureScript/Make.hs+1−1
@@ -149,7 +149,7 @@ rebuildModule MakeActions{..} externs m@(Module _ _ moduleName _ _) = do
149149 lint withPrim
150150 ((Module ss coms _ elaborated exps, env'), nextVar) <- runSupplyT 0 $ do
151151 [desugared] <- desugar externs [withPrim]
152− runCheck' env $ typeCheckModule desugared
152+ runCheck' (emptyCheckState env) $ typeCheckModule desugared
153153 regrouped <- createBindingGroups moduleName . collapseBindingGroups $ elaborated
154154 let mod' = Module ss coms moduleName regrouped exps
155155 corefn = CF.moduleToCoreFn env' mod'
src/Language/PureScript/TypeChecker/Entailment.hs+34−22
@@ -5,8 +5,10 @@
55--
66module Language.PureScript.TypeChecker.Entailment
77 ( InstanceContext
8+ , SolverOptions(..)
89 , replaceTypeClassDictionaries
910 , newDictionaries
11+ , entails
1012 ) where
1113
1214import Prelude.Compat
@@ -56,7 +58,7 @@ replaceTypeClassDictionaries
5658 . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
5759 => Bool
5860 -> Expr
59− -> m (Expr, [(Ident, Constraint)])
61+ -> m (Expr, [(Ident, InstanceContext, Constraint)])
6062replaceTypeClassDictionaries shouldGeneralize expr = flip evalStateT M.empty $ do
6163 -- Loop, deferring any unsolved constraints, until there are no more
6264 -- constraints which can be solved, then make a generalization pass.
@@ -70,18 +72,18 @@ replaceTypeClassDictionaries shouldGeneralize expr = flip evalStateT M.empty $ d
7072 -- This pass solves constraints where possible, deferring constraints if not.
7173 deferPass :: Expr -> StateT InstanceContext m (Expr, Any)
7274 deferPass = fmap (second fst) . runWriterT . f where
73− f :: Expr -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
75+ f :: Expr -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) Expr
7476 (_, f, _) = everywhereOnValuesTopDownM return (go True) return
7577
7678 -- This pass generalizes any remaining constraints
77− generalizePass :: Expr -> StateT InstanceContext m (Expr, [(Ident, Constraint)])
79+ generalizePass :: Expr -> StateT InstanceContext m (Expr, [(Ident, InstanceContext, Constraint)])
7880 generalizePass = fmap (second snd) . runWriterT . f where
79− f :: Expr -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
81+ f :: Expr -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) Expr
8082 (_, f, _) = everywhereOnValuesTopDownM return (go False) return
8183
82− go :: Bool -> Expr -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
83− go deferErrors dict@(TypeClassDictionary _ _ hints) =
84− rethrow (addHints hints) $ entails shouldGeneralize deferErrors dict
84+ go :: Bool -> Expr -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) Expr
85+ go deferErrors (TypeClassDictionary constraint context hints) =
86+ rethrow (addHints hints) $ entails (SolverOptions shouldGeneralize deferErrors) constraint context hints
8587 go _ other = return other
8688
8789-- | Three options for how we can handle a constraint, depending on the mode we're in.
@@ -93,18 +95,29 @@ data EntailsResult a
9395 | Deferred
9496 -- ^ We couldn't solve this constraint right now, so it has been deferred
9597
96−-- |
97−-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
98+-- | Options for the constraint solver
99+data SolverOptions = SolverOptions
100+ { solverShouldGeneralize :: Bool
101+ -- ^ Should the solver be allowed to generalize over unsolved constraints?
102+ , solverDeferErrors :: Bool
103+ -- ^ Should the solver be allowed to defer errors by skipping constraints?
104+ }
105+
106+-- | Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
98107-- return a type class dictionary reference.
99−--
100108entails
101109 :: forall m
102110 . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
103− => Bool
104− -> Bool
105− -> Expr
106− -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
107−entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hints) =
111+ => SolverOptions
112+ -- ^ Solver options
113+ -> Constraint
114+ -- ^ The constraint to solve
115+ -> InstanceContext
116+ -- ^ The contexts in which to solve the constraint
117+ -> [ErrorMessageHint]
118+ -- ^ Error message hints to apply to any instance errors
119+ -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) Expr
120+entails SolverOptions{..} constraint context hints =
108121 solve constraint
109122 where
110123 forClassName :: InstanceContext -> Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]
@@ -123,10 +136,10 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin
123136 valUndefined :: Expr
124137 valUndefined = Var (Qualified (Just (ModuleName [ProperName C.prim])) (Ident C.undefined))
125138
126− solve :: Constraint -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
139+ solve :: Constraint -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) Expr
127140 solve con = go 0 con
128141 where
129− go :: Int -> Constraint -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
142+ go :: Int -> Constraint -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) Expr
130143 go work (Constraint className' tys' _) | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
131144 go work con'@(Constraint className' tys' conInfo) = WriterT . StateT . (withErrorMessageHint (ErrorSolvingConstraint con') .) . runStateT . runWriterT $ do
132145 -- We might have unified types by solving other constraints, so we need to
@@ -179,7 +192,7 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin
179192 let newContext = mkContext newDicts
180193 modify (combineContexts newContext)
181194 -- Mark this constraint for generalization
182− tell (mempty, [(ident, unsolved)])
195+ tell (mempty, [(ident, context, unsolved)])
183196 return (Var qident)
184197 Deferred ->
185198 -- Constraint was deferred, just return the dictionary unchanged,
@@ -219,10 +232,10 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin
219232
220233 unique :: [Type] -> [(a, TypeClassDictionaryInScope)] -> m (EntailsResult a)
221234 unique tyArgs []
222− | deferErrors = return Deferred
235+ | solverDeferErrors = return Deferred
223236 -- We need a special case for nullary type classes, since we want
224237 -- to generalize over Partial constraints.
225− | shouldGeneralize && (null tyArgs || any canBeGeneralized tyArgs) = return (Unsolved (Constraint className' tyArgs conInfo))
238+ | solverShouldGeneralize && (null tyArgs || any canBeGeneralized tyArgs) = return (Unsolved (Constraint className' tyArgs conInfo))
226239 | otherwise = throwError . errorMessage $ NoInstanceFound (Constraint className' tyArgs conInfo)
227240 unique _ [(a, dict)] = return $ Solved a dict
228241 unique tyArgs tcds
@@ -250,7 +263,7 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin
250263 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
251264 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
252265 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
253− solveSubgoals :: Matching Type -> Maybe [Constraint] -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) (Maybe [Expr])
266+ solveSubgoals :: Matching Type -> Maybe [Constraint] -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) (Maybe [Expr])
254267 solveSubgoals _ Nothing = return Nothing
255268 solveSubgoals subst (Just subgoals) =
256269 Just <$> traverse (go (work + 1) . mapConstraintArgs (map (replaceAllTypeVars (M.toList subst)))) subgoals
@@ -267,7 +280,6 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin
267280 App (Accessor (C.__superclass_ ++ showQualified runProperName superclassName ++ "_" ++ show index)
268281 dict)
269282 valUndefined
270−entails _ _ _ = internalError "entails: expected TypeClassDictionary"
271283
272284-- Check if an instance matches our list of types, allowing for types
273285-- to be solved via functional dependencies. If the types match, we return a
src/Language/PureScript/TypeChecker/Monad.hs+3−3
@@ -257,11 +257,11 @@ modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })
257257
258258-- | Run a computation in the typechecking monad, starting with an empty @Environment@
259259runCheck :: (Functor m) => StateT CheckState m a -> m (a, Environment)
260−runCheck = runCheck' initEnvironment
260+runCheck = runCheck' (emptyCheckState initEnvironment)
261261
262262-- | Run a computation in the typechecking monad, failing with an error, or succeeding with a return value and the final @Environment@.
263−runCheck' :: (Functor m) => Environment -> StateT CheckState m a -> m (a, Environment)
264−runCheck' env check = second checkEnv <$> runStateT check (emptyCheckState env)
263+runCheck' :: (Functor m) => CheckState -> StateT CheckState m a -> m (a, Environment)
264+runCheck' st check = second checkEnv <$> runStateT check st
265265
266266-- | Make an assertion, failing with an error message
267267guardWith :: (MonadError e m) => e -> Bool -> m ()
src/Language/PureScript/TypeChecker/TypeSearch.hs+35−14
@@ -19,6 +19,7 @@ import Language.PureScript.TypeChecker.Unify as P
1919import Control.Monad.Supply as P
2020import Language.PureScript.AST as P
2121import Language.PureScript.Environment as P
22+import Language.PureScript.Errors as P
2223import Language.PureScript.Names as P
2324import Language.PureScript.TypeChecker.Skolems as Skolem
2425import Language.PureScript.TypeChecker.Synonyms as P
@@ -26,29 +27,32 @@ import Language.PureScript.Types as P
2627
2728checkInEnvironment
2829 :: Environment
29− -> Integer
30− -> StateT TC.CheckState (SupplyT (WriterT b (Except e))) a
30+ -> TC.CheckState
31+ -> StateT TC.CheckState (SupplyT (WriterT b (Except P.MultipleErrors))) a
3132 -> Maybe (a, Environment)
32−checkInEnvironment env nextVar =
33+checkInEnvironment env st =
3334 either (const Nothing) Just
3435 . runExcept
3536 . evalWriterT
36− . P.evalSupplyT nextVar
37− . TC.runCheck' env
37+ . P.evalSupplyT 0
38+ . TC.runCheck' (st { TC.checkEnv = env })
3839
3940evalWriterT :: Monad m => WriterT b m r -> m r
4041evalWriterT m = liftM fst (runWriterT m)
4142
4243checkSubsume
43− :: P.Environment
44+ :: Maybe [(P.Ident, Entailment.InstanceContext, P.Constraint)]
45+ -- ^ Additional constraints we need to satisfy
46+ -> P.Environment
4447 -- ^ The Environment which contains the relevant definitions and typeclasses
45− -> Integer
48+ -> TC.CheckState
49+ -- ^ The typechecker state
4650 -> P.Type
4751 -- ^ The user supplied type
4852 -> P.Type
4953 -- ^ 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
54+ -> Maybe ((P.Expr, [(P.Ident, Entailment.InstanceContext, P.Constraint)]), P.Environment)
55+checkSubsume unsolved env st userT envT = checkInEnvironment env st $ do
5256 let initializeSkolems =
5357 Skolem.introduceSkolemScope
5458 <=< P.replaceAllTypeSynonyms
@@ -62,12 +66,29 @@ checkSubsume env nextVar userT envT = checkInEnvironment env nextVar $ do
6266 elab <- subsumes envT' userT'
6367 subst <- gets TC.checkSubstitution
6468 let expP = P.overTypes (P.substituteType subst) (elab dummyExpression)
65− Entailment.replaceTypeClassDictionaries False expP
69+
70+ -- Now check that any unsolved constraints have not become impossible
71+ (traverse_ . traverse_) (\(_, context, constraint) -> do
72+ let constraint' = P.mapConstraintArgs (map (P.substituteType subst)) constraint
73+ flip evalStateT Map.empty . evalWriterT $
74+ Entailment.entails
75+ (Entailment.SolverOptions
76+ { solverShouldGeneralize = True
77+ , solverDeferErrors = False
78+ }) constraint' context []) unsolved
79+
80+ -- Finally, check any constraints which were found during elaboration
81+ Entailment.replaceTypeClassDictionaries (isJust unsolved) expP
6682
6783typeSearch
68− :: P.Environment
69− -> Integer
84+ :: Maybe [(P.Ident, Entailment.InstanceContext, P.Constraint)]
85+ -- ^ Additional constraints we need to satisfy
86+ -> P.Environment
87+ -- ^ The Environment which contains the relevant definitions and typeclasses
88+ -> TC.CheckState
89+ -- ^ The typechecker state
7090 -> P.Type
91+ -- ^ The type we are looking for
7192 -> 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)
93+typeSearch unsolved env st type' =
94+ Map.mapMaybe (\(x, _, _) -> checkSubsume unsolved env st type' x $> x) (P.names env)
src/Language/PureScript/TypeChecker/Types.hs+41−34
@@ -1,3 +1,4 @@
1+{-# LANGUAGE LambdaCase #-}
12{-# LANGUAGE OverloadedStrings #-}
23{-# LANGUAGE NamedFieldPuns #-}
34
@@ -27,15 +28,16 @@ module Language.PureScript.TypeChecker.Types
2728
2829import Prelude.Compat
2930
30−import Control.Arrow (second)
31+import Control.Arrow (first, second, (***))
3132import Control.Monad
3233import Control.Monad.Error.Class (MonadError(..))
3334import Control.Monad.State.Class (MonadState(..), gets)
34−import Control.Monad.Supply.Class (MonadSupply, peek)
35+import Control.Monad.Supply.Class (MonadSupply)
3536import Control.Monad.Writer.Class (MonadWriter(..))
3637
3738import Data.Bifunctor (bimap)
3839import Data.Either (lefts, rights)
40+import Data.Functor (($>))
3941import Data.List (transpose, nub, (\\), partition, delete)
4042import Data.Maybe (fromMaybe)
4143import qualified Data.Map as M
@@ -74,17 +76,13 @@ typesOf
7476 -> [(Ident, Expr)]
7577 -> m [(Ident, (Expr, Type))]
7678typesOf 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
81− (tys, w) <- withoutWarnings . capturingSubstitution tidyUp $ do
79+ tys <- capturingSubstitution tidyUp $ do
8280 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup (Just moduleName) vals
83− ds1 <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
84− ds2 <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict
85− return (map (\x -> (False, x)) ds1 ++ map (\x -> (True, x)) ds2)
81+ ds1 <- parU typed $ \e -> withoutWarnings $ checkTypedBindingGroupElement moduleName e dict
82+ ds2 <- forM untyped $ \e -> withoutWarnings $ typeForBindingGroupElement e dict untypedDict
83+ return (map (False, ) ds1 ++ map (True, ) ds2)
8684
87− inferred <- forM tys $ \(shouldGeneralize, (ident, (val, ty))) -> do
85+ inferred <- forM tys $ \(shouldGeneralize, ((ident, (val, ty)), _)) -> do
8886 -- Replace type class dictionary placeholders with actual dictionaries
8987 (val', unsolved) <- replaceTypeClassDictionaries shouldGeneralize val
9088 -- Generalize and constrain the type
@@ -104,7 +102,7 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
104102 $ CannotGeneralizeRecursiveFunction ident generalized
105103 -- Make sure any unsolved type constraints only use type variables which appear
106104 -- unknown in the inferred type.
107− forM_ unsolved $ \(_, con) -> do
105+ forM_ unsolved $ \(_, _, con) -> do
108106 -- We need information about functional dependencies, since we allow
109107 -- ambiguous types to be inferred if they can be solved by some functional
110108 -- dependency.
@@ -113,46 +111,55 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
113111 let solved = foldMap (S.fromList . fdDetermined) typeClassDependencies
114112 let constraintTypeVars = nub . foldMap (unknownsInType . fst) . filter ((`notElem` solved) . snd) $ zip (constraintArgs con) [0..]
115113 when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $ do
116− nextVar <- peek
117− throwError . onErrorMessages (replaceTypes (not shouldGeneralize) currentSubst nextVar) . errorMessage $ NoInstanceFound con
114+ throwError . onErrorMessages (replaceTypes currentSubst) . errorMessage $ NoInstanceFound con
118115
119116 -- Check skolem variables did not escape their scope
120117 skolemEscapeCheck val'
121118 -- Check rows do not contain duplicate labels
122119 checkDuplicateLabels val'
123− return (ident, (foldr (Abs . Left . fst) val' unsolved, generalized))
120+ return ((ident, (foldr (Abs . Left . (\(x, _, _) -> x)) val' unsolved, generalized)), unsolved)
124121
125122 -- Show warnings here, since types in wildcards might have been solved during
126123 -- instance resolution (by functional dependencies).
127− finalSubst <- gets checkSubstitution
124+ finalState <- get
125+ forM_ tys $ \(shouldGeneralize, ((_, (_, _)), w)) -> do
126+ let replaceTypes' = replaceTypes (checkSubstitution finalState)
127+ runTypeSearch' = runTypeSearch (guard shouldGeneralize $> foldMap snd inferred) finalState
128+ (escalateWarningWhen isHoleError . tell . onErrorMessages (runTypeSearch' . replaceTypes')) w
128129
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
135−
136− return inferred
130+ return (map fst inferred)
137131 where
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
132+ replaceTypes
133+ :: Substitution
134+ -> ErrorMessage
135+ -> ErrorMessage
136+ replaceTypes subst = onTypesInErrorMessage (substituteType subst)
137+
138+ -- | Run type search to complete any typed hole error messages
139+ runTypeSearch
140+ :: Maybe [(Ident, InstanceContext, Constraint)]
141+ -- ^ Any unsolved constraints which we need to continue to satisfy
142+ -> CheckState
143+ -- ^ The final type checker state
144+ -> ErrorMessage
145+ -> ErrorMessage
146+ runTypeSearch cons st = \case
147+ ErrorMessage hints (HoleInferredType x ty y (TSBefore env)) ->
148+ let subst = checkSubstitution st
149+ searchResult = (fmap . fmap) (substituteType subst)
150+ (M.toList (typeSearch cons env st (substituteType subst ty)))
151+ in ErrorMessage hints (HoleInferredType x ty y (TSAfter searchResult))
152+ other -> other
146153
147154 -- | Generalize type vars using forall and add inferred constraints
148155 generalize unsolved = varIfUnknown . constrain unsolved
149156
150157 -- | Add any unsolved constraints
151158 constrain [] = id
152− constrain cs = ConstrainedType (map snd cs)
159+ constrain cs = ConstrainedType (map (\(_, _, x) -> x) cs)
153160
154161 -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
155− tidyUp ts sub = map (\(b, (i, (val, ty))) -> (b, (i, (overTypes (substituteType sub) val, substituteType sub ty)))) ts
162+ tidyUp ts sub = map (second (first (second (overTypes (substituteType sub) *** substituteType sub)))) ts
156163
157164 isHoleError :: ErrorMessage -> Bool
158165 isHoleError (ErrorMessage _ HoleInferredType{}) = True