da83efb · rowtype-yoga/purescript-native

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

on golang help sign in

Fix issue with typed holes in inference mode (#2386)

da83efbPhil Freeman10 years ago

src/Language/PureScript/Make.hs+1−1

compare with golang

unifiedsplit

@@ -149,7 +149,7 @@ rebuildModule MakeActions{..} externs m@(Module _ _ moduleName _ _) = do

149 lint withPrim

150 ((Module ss coms _ elaborated exps, env'), nextVar) <- runSupplyT 0 $ do

151 [desugared] <- desugar externs [withPrim]

152− runCheck' env $ typeCheckModule desugared

152+ runCheck' (emptyCheckState env) $ typeCheckModule desugared

153 regrouped <- createBindingGroups moduleName . collapseBindingGroups $ elaborated

154 let mod' = Module ss coms moduleName regrouped exps

155 corefn = CF.moduleToCoreFn env' mod'

src/Language/PureScript/TypeChecker/Entailment.hs+34−22

@@ -5,8 +5,10 @@

5--

6module Language.PureScript.TypeChecker.Entailment

7 ( InstanceContext

8+ , SolverOptions(..)

8 , replaceTypeClassDictionaries

9 , replaceTypeClassDictionaries

9 , newDictionaries

10 , newDictionaries

11+ , entails

10 ) where

12 ) where

12import Prelude.Compat

14import Prelude.Compat

@@ -56,7 +58,7 @@ replaceTypeClassDictionaries

56 . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)

58 . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)

57 => Bool

59 => Bool

58 -> Expr

60 -> Expr

59− -> m (Expr, [(Ident, Constraint)])

61+ -> m (Expr, [(Ident, InstanceContext, Constraint)])

60replaceTypeClassDictionaries shouldGeneralize expr = flip evalStateT M.empty $ do

62replaceTypeClassDictionaries shouldGeneralize expr = flip evalStateT M.empty $ do

61 -- Loop, deferring any unsolved constraints, until there are no more

63 -- Loop, deferring any unsolved constraints, until there are no more

62 -- constraints which can be solved, then make a generalization pass.

64 -- constraints which can be solved, then make a generalization pass.

@@ -70,18 +72,18 @@ replaceTypeClassDictionaries shouldGeneralize expr = flip evalStateT M.empty $ d

70 -- This pass solves constraints where possible, deferring constraints if not.

72 -- This pass solves constraints where possible, deferring constraints if not.

71 deferPass :: Expr -> StateT InstanceContext m (Expr, Any)

73 deferPass :: Expr -> StateT InstanceContext m (Expr, Any)

72 deferPass = fmap (second fst) . runWriterT . f where

74 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

74 (_, f, _) = everywhereOnValuesTopDownM return (go True) return

76 (_, f, _) = everywhereOnValuesTopDownM return (go True) return

76 -- This pass generalizes any remaining constraints

78 -- 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)])

78 generalizePass = fmap (second snd) . runWriterT . f where

80 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

80 (_, f, _) = everywhereOnValuesTopDownM return (go False) return

82 (_, f, _) = everywhereOnValuesTopDownM return (go False) return

82− go :: Bool -> Expr -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr

84+ go :: Bool -> Expr -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) Expr

83− go deferErrors dict@(TypeClassDictionary _ _ hints) =

85+ go deferErrors (TypeClassDictionary constraint context hints) =

84− rethrow (addHints hints) $ entails shouldGeneralize deferErrors dict

86+ rethrow (addHints hints) $ entails (SolverOptions shouldGeneralize deferErrors) constraint context hints

85 go _ other = return other

87 go _ other = return other

87-- | Three options for how we can handle a constraint, depending on the mode we're in.

89-- | Three options for how we can handle a constraint, depending on the mode we're in.

@@ -93,18 +95,29 @@ data EntailsResult a

93 | Deferred

95 | Deferred

94 -- ^ We couldn't solve this constraint right now, so it has been deferred

96 -- ^ We couldn't solve this constraint right now, so it has been deferred

96−-- |

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+

97−-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,

106+-- | Check that the current set of type class dictionaries entail the specified type class goal, and, if so,

98-- return a type class dictionary reference.

107-- return a type class dictionary reference.

99−--

100entails

108entails

101 :: forall m

109 :: forall m

102 . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)

110 . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)

103− => Bool

111+ => SolverOptions

104− -> Bool

112+ -- ^ Solver options

105− -> Expr

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

106− -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr

119+ -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) Expr

107−entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hints) =

120+entails SolverOptions{..} constraint context hints =

108 solve constraint

121 solve constraint

109 where

122 where

110 forClassName :: InstanceContext -> Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]

123 forClassName :: InstanceContext -> Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]

@@ -123,10 +136,10 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin

123 valUndefined :: Expr

136 valUndefined :: Expr

124 valUndefined = Var (Qualified (Just (ModuleName [ProperName C.prim])) (Ident C.undefined))

137 valUndefined = Var (Qualified (Just (ModuleName [ProperName C.prim])) (Ident C.undefined))

125

138

126− solve :: Constraint -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr

139+ solve :: Constraint -> WriterT (Any, [(Ident, InstanceContext, Constraint)]) (StateT InstanceContext m) Expr

127 solve con = go 0 con

140 solve con = go 0 con

128 where

141 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

130 go work (Constraint className' tys' _) | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'

143 go work (Constraint className' tys' _) | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'

131 go work con'@(Constraint className' tys' conInfo) = WriterT . StateT . (withErrorMessageHint (ErrorSolvingConstraint con') .) . runStateT . runWriterT $ do

144 go work con'@(Constraint className' tys' conInfo) = WriterT . StateT . (withErrorMessageHint (ErrorSolvingConstraint con') .) . runStateT . runWriterT $ do

132 -- We might have unified types by solving other constraints, so we need to

145 -- We might have unified types by solving other constraints, so we need to

@@ -179,7 +192,7 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin

179 let newContext = mkContext newDicts

192 let newContext = mkContext newDicts

180 modify (combineContexts newContext)

193 modify (combineContexts newContext)

181 -- Mark this constraint for generalization

194 -- Mark this constraint for generalization

182− tell (mempty, [(ident, unsolved)])

195+ tell (mempty, [(ident, context, unsolved)])

183 return (Var qident)

196 return (Var qident)

184 Deferred ->

197 Deferred ->

185 -- Constraint was deferred, just return the dictionary unchanged,

198 -- Constraint was deferred, just return the dictionary unchanged,

@@ -219,10 +232,10 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin

219

232

220 unique :: [Type] -> [(a, TypeClassDictionaryInScope)] -> m (EntailsResult a)

233 unique :: [Type] -> [(a, TypeClassDictionaryInScope)] -> m (EntailsResult a)

221 unique tyArgs []

234 unique tyArgs []

222− | deferErrors = return Deferred

235+ | solverDeferErrors = return Deferred

223 -- We need a special case for nullary type classes, since we want

236 -- We need a special case for nullary type classes, since we want

224 -- to generalize over Partial constraints.

237 -- 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))

226 | otherwise = throwError . errorMessage $ NoInstanceFound (Constraint className' tyArgs conInfo)

239 | otherwise = throwError . errorMessage $ NoInstanceFound (Constraint className' tyArgs conInfo)

227 unique _ [(a, dict)] = return $ Solved a dict

240 unique _ [(a, dict)] = return $ Solved a dict

228 unique tyArgs tcds

241 unique tyArgs tcds

@@ -250,7 +263,7 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin

250 -- Create dictionaries for subgoals which still need to be solved by calling go recursively

263 -- Create dictionaries for subgoals which still need to be solved by calling go recursively

251 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type

264 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type

252 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.

265 -- 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])

254 solveSubgoals _ Nothing = return Nothing

267 solveSubgoals _ Nothing = return Nothing

255 solveSubgoals subst (Just subgoals) =

268 solveSubgoals subst (Just subgoals) =

256 Just <$> traverse (go (work + 1) . mapConstraintArgs (map (replaceAllTypeVars (M.toList subst)))) subgoals

269 Just <$> traverse (go (work + 1) . mapConstraintArgs (map (replaceAllTypeVars (M.toList subst)))) subgoals

@@ -267,7 +280,6 @@ entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hin

267 App (Accessor (C.__superclass_ ++ showQualified runProperName superclassName ++ "_" ++ show index)

280 App (Accessor (C.__superclass_ ++ showQualified runProperName superclassName ++ "_" ++ show index)

268 dict)

281 dict)

269 valUndefined

282 valUndefined

270−entails _ _ _ = internalError "entails: expected TypeClassDictionary"

271

283

272-- Check if an instance matches our list of types, allowing for types

284-- Check if an instance matches our list of types, allowing for types

273-- to be solved via functional dependencies. If the types match, we return a

285-- 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) })

257

258-- | Run a computation in the typechecking monad, starting with an empty @Environment@

259runCheck :: (Functor m) => StateT CheckState m a -> m (a, Environment)

260−runCheck = runCheck' initEnvironment

260+runCheck = runCheck' (emptyCheckState initEnvironment)

261

262-- | 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)

263+runCheck' :: (Functor m) => CheckState -> StateT CheckState m a -> m (a, Environment)

264−runCheck' env check = second checkEnv <$> runStateT check (emptyCheckState env)

264+runCheck' st check = second checkEnv <$> runStateT check st

265

266-- | Make an assertion, failing with an error message

267guardWith :: (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

19import Control.Monad.Supply as P

20import Language.PureScript.AST as P

21import Language.PureScript.Environment as P

22+import Language.PureScript.Errors as P

22import Language.PureScript.Names as P

23import Language.PureScript.Names as P

23import Language.PureScript.TypeChecker.Skolems as Skolem

24import Language.PureScript.TypeChecker.Skolems as Skolem

24import Language.PureScript.TypeChecker.Synonyms as P

25import Language.PureScript.TypeChecker.Synonyms as P

@@ -26,29 +27,32 @@ import Language.PureScript.Types as P

27checkInEnvironment

28checkInEnvironment

28 :: Environment

29 :: Environment

29− -> Integer

30+ -> TC.CheckState

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

31+ -> StateT TC.CheckState (SupplyT (WriterT b (Except P.MultipleErrors))) a

31 -> Maybe (a, Environment)

32 -> Maybe (a, Environment)

32−checkInEnvironment env nextVar =

33+checkInEnvironment env st =

33 either (const Nothing) Just

34 either (const Nothing) Just

34 . runExcept

35 . runExcept

35 . evalWriterT

36 . evalWriterT

36− . P.evalSupplyT nextVar

37+ . P.evalSupplyT 0

37− . TC.runCheck' env

38+ . TC.runCheck' (st { TC.checkEnv = env })

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

40evalWriterT :: Monad m => WriterT b m r -> m r

40evalWriterT m = liftM fst (runWriterT m)

41evalWriterT m = liftM fst (runWriterT m)

42checkSubsume

43checkSubsume

44+ :: Maybe [(P.Ident, Entailment.InstanceContext, P.Constraint)]

45+ -- ^ Additional constraints we need to satisfy

43− :: P.Environment

46+ -> P.Environment

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

47 -- ^ The Environment which contains the relevant definitions and typeclasses

45− -> Integer

48+ -> TC.CheckState

49+ -- ^ The typechecker state

46 -> P.Type

50 -> P.Type

47 -- ^ The user supplied type

51 -- ^ The user supplied type

48 -> P.Type

52 -> P.Type

49 -- ^ The type supplied by the environment

53 -- ^ The type supplied by the environment

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

54+ -> Maybe ((P.Expr, [(P.Ident, Entailment.InstanceContext, P.Constraint)]), P.Environment)

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

55+checkSubsume unsolved env st userT envT = checkInEnvironment env st $ do

52 let initializeSkolems =

56 let initializeSkolems =

53 Skolem.introduceSkolemScope

57 Skolem.introduceSkolemScope

54 <=< P.replaceAllTypeSynonyms

58 <=< P.replaceAllTypeSynonyms

@@ -62,12 +66,29 @@ checkSubsume env nextVar userT envT = checkInEnvironment env nextVar $ do

62 elab <- subsumes envT' userT'

66 elab <- subsumes envT' userT'

63 subst <- gets TC.checkSubstitution

67 subst <- gets TC.checkSubstitution

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

68 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

67typeSearch

83typeSearch

84+ :: Maybe [(P.Ident, Entailment.InstanceContext, P.Constraint)]

85+ -- ^ Additional constraints we need to satisfy

68− :: P.Environment

86+ -> P.Environment

69− -> Integer

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

88+ -> TC.CheckState

89+ -- ^ The typechecker state

70 -> P.Type

90 -> P.Type

91+ -- ^ The type we are looking for

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

92 -> Map (P.Qualified P.Ident) P.Type

72−typeSearch env nextVar type' =

93+typeSearch unsolved env st type' =

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

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 #-}

1{-# LANGUAGE OverloadedStrings #-}

2{-# LANGUAGE OverloadedStrings #-}

2{-# LANGUAGE NamedFieldPuns #-}

3{-# LANGUAGE NamedFieldPuns #-}

@@ -27,15 +28,16 @@ module Language.PureScript.TypeChecker.Types

28import Prelude.Compat

29import Prelude.Compat

30−import Control.Arrow (second)

31+import Control.Arrow (first, second, (***))

31import Control.Monad

32import Control.Monad

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

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

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

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

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

35+import Control.Monad.Supply.Class (MonadSupply)

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

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

37import Data.Bifunctor (bimap)

38import Data.Bifunctor (bimap)

38import Data.Either (lefts, rights)

39import Data.Either (lefts, rights)

40+import Data.Functor (($>))

39import Data.List (transpose, nub, (\\), partition, delete)

41import Data.List (transpose, nub, (\\), partition, delete)

40import Data.Maybe (fromMaybe)

42import Data.Maybe (fromMaybe)

41import qualified Data.Map as M

43import qualified Data.Map as M

@@ -74,17 +76,13 @@ typesOf

74 -> [(Ident, Expr)]

76 -> [(Ident, Expr)]

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

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

76typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do

78typesOf 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

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

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

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

81+ ds1 <- parU typed $ \e -> withoutWarnings $ checkTypedBindingGroupElement moduleName e dict

84− ds2 <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict

82+ ds2 <- forM untyped $ \e -> withoutWarnings $ typeForBindingGroupElement e dict untypedDict

85− return (map (\x -> (False, x)) ds1 ++ map (\x -> (True, x)) ds2)

83+ return (map (False, ) ds1 ++ map (True, ) ds2)

87− inferred <- forM tys $ \(shouldGeneralize, (ident, (val, ty))) -> do

85+ inferred <- forM tys $ \(shouldGeneralize, ((ident, (val, ty)), _)) -> do

88 -- Replace type class dictionary placeholders with actual dictionaries

86 -- Replace type class dictionary placeholders with actual dictionaries

89 (val', unsolved) <- replaceTypeClassDictionaries shouldGeneralize val

87 (val', unsolved) <- replaceTypeClassDictionaries shouldGeneralize val

90 -- Generalize and constrain the type

88 -- Generalize and constrain the type

@@ -104,7 +102,7 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do

104 $ CannotGeneralizeRecursiveFunction ident generalized

102 $ CannotGeneralizeRecursiveFunction ident generalized

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

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

106 -- unknown in the inferred type.

104 -- unknown in the inferred type.

107− forM_ unsolved $ \(_, con) -> do

105+ forM_ unsolved $ \(_, _, con) -> do

108 -- We need information about functional dependencies, since we allow

106 -- We need information about functional dependencies, since we allow

109 -- ambiguous types to be inferred if they can be solved by some functional

107 -- ambiguous types to be inferred if they can be solved by some functional

110 -- dependency.

108 -- dependency.

@@ -113,46 +111,55 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do

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

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

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

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

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

113 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

118

115

119 -- Check skolem variables did not escape their scope

116 -- Check skolem variables did not escape their scope

120 skolemEscapeCheck val'

117 skolemEscapeCheck val'

121 -- Check rows do not contain duplicate labels

118 -- Check rows do not contain duplicate labels

122 checkDuplicateLabels val'

119 checkDuplicateLabels val'

123− return (ident, (foldr (Abs . Left . fst) val' unsolved, generalized))

120+ return ((ident, (foldr (Abs . Left . (\(x, _, _) -> x)) val' unsolved, generalized)), unsolved)

124

121

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

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

126 -- instance resolution (by functional dependencies).

123 -- instance resolution (by functional dependencies).

124+ finalState <- get

125+ forM_ tys $ \(shouldGeneralize, ((_, (_, _)), w)) -> do

127− finalSubst <- gets checkSubstitution

126+ let replaceTypes' = replaceTypes (checkSubstitution finalState)

127+ runTypeSearch' = runTypeSearch (guard shouldGeneralize $> foldMap snd inferred) finalState

128+ (escalateWarningWhen isHoleError . tell . onErrorMessages (runTypeSearch' . replaceTypes')) w

128

129

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

130+ return (map fst 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

137 where

131 where

138− replaceTypes shouldRunTypeSearch subst nextVar =

132+ replaceTypes

139− (if shouldRunTypeSearch then runTypeSearch else id)

133+ :: Substitution

134+ -> ErrorMessage

135+ -> ErrorMessage

140− . onTypesInErrorMessage (substituteType subst)

136+ replaceTypes subst = onTypesInErrorMessage (substituteType subst)

141− where

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

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

147+ ErrorMessage hints (HoleInferredType x ty y (TSBefore env)) ->

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

148+ let subst = checkSubstitution st

149+ searchResult = (fmap . fmap) (substituteType subst)

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

150+ (M.toList (typeSearch cons env st (substituteType subst ty)))

145− runTypeSearch x = x

151+ in ErrorMessage hints (HoleInferredType x ty y (TSAfter searchResult))

152+ other -> other

146

153

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

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

148 generalize unsolved = varIfUnknown . constrain unsolved

155 generalize unsolved = varIfUnknown . constrain unsolved

149

156

150 -- | Add any unsolved constraints

157 -- | Add any unsolved constraints

151 constrain [] = id

158 constrain [] = id

152− constrain cs = ConstrainedType (map snd cs)

159+ constrain cs = ConstrainedType (map (\(_, _, x) -> x) cs)

153

160

154 -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values

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

156

163

157 isHoleError :: ErrorMessage -> Bool

164 isHoleError :: ErrorMessage -> Bool

158 isHoleError (ErrorMessage _ HoleInferredType{}) = True

165 isHoleError (ErrorMessage _ HoleInferredType{}) = True