@@ -1,3 +1,4 @@
1+{-# LANGUAGE LambdaCase #-}
12{-# LANGUAGE OverloadedStrings #-}
23{-# LANGUAGE NamedFieldPuns #-}
34
@@ -27,13 +28,16 @@ module Language.PureScript.TypeChecker.Types
2728
2829import Prelude.Compat
2930
31+import Control.Arrow (first, second, (***))
3032import Control.Monad
3133import Control.Monad.Error.Class (MonadError(..))
3234import Control.Monad.State.Class (MonadState(..), gets)
3335import Control.Monad.Supply.Class (MonadSupply)
3436import Control.Monad.Writer.Class (MonadWriter(..))
3537
38+import Data.Bifunctor (bimap)
3639import Data.Either (lefts, rights)
40+import Data.Functor (($>))
3741import Data.List (transpose, nub, (\\), partition, delete)
3842import Data.Maybe (fromMaybe)
3943import qualified Data.Map as M
@@ -53,9 +57,11 @@ import Language.PureScript.TypeChecker.Rows
5357import Language.PureScript.TypeChecker.Skolems
5458import Language.PureScript.TypeChecker.Subsumption
5559import Language.PureScript.TypeChecker.Synonyms
60+import Language.PureScript.TypeChecker.TypeSearch
5661import Language.PureScript.TypeChecker.Unify
5762import Language.PureScript.Types
5863
64+
5965data BindingGroupType
6066 = RecursiveBindingGroup
6167 | NonRecursiveBindingGroup
@@ -70,13 +76,13 @@ typesOf
7076 -> [(Ident, Expr)]
7177 -> m [(Ident, (Expr, Type))]
7278typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
73− (tys, w) <- withoutWarnings . capturingSubstitution tidyUp $ do
79+ tys <- capturingSubstitution tidyUp $ do
7480 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup (Just moduleName) vals
75− ds1 <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
76− ds2 <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict
77− 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)
7884
79− inferred <- forM tys $ \(shouldGeneralize, (ident, (val, ty))) -> do
85+ inferred <- forM tys $ \(shouldGeneralize, ((ident, (val, ty)), _)) -> do
8086 -- Replace type class dictionary placeholders with actual dictionaries
8187 (val', unsolved) <- replaceTypeClassDictionaries shouldGeneralize val
8288 -- Generalize and constrain the type
@@ -96,7 +102,7 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
96102 $ CannotGeneralizeRecursiveFunction ident generalized
97103 -- Make sure any unsolved type constraints only use type variables which appear
98104 -- unknown in the inferred type.
99− forM_ unsolved $ \(_, con) -> do
105+ forM_ unsolved $ \(_, _, con) -> do
100106 -- We need information about functional dependencies, since we allow
101107 -- ambiguous types to be inferred if they can be solved by some functional
102108 -- dependency.
@@ -104,33 +110,56 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
104110 TypeClassData{ typeClassDependencies } <- gets (findClass . typeClasses . checkEnv)
105111 let solved = foldMap (S.fromList . fdDetermined) typeClassDependencies
106112 let constraintTypeVars = nub . foldMap (unknownsInType . fst) . filter ((`notElem` solved) . snd) $ zip (constraintArgs con) [0..]
107− when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $
108− throwError . onErrorMessages (replaceTypes currentSubst) . errorMessage $ NoInstanceFound con
113+ when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $ do
114+ throwError . onErrorMessages (replaceTypes currentSubst) . errorMessage $ AmbiguousTypeVariables generalized con
109115
110116 -- Check skolem variables did not escape their scope
111117 skolemEscapeCheck val'
112118 -- Check rows do not contain duplicate labels
113119 checkDuplicateLabels val'
114− return (ident, (foldr (Abs . Left . fst) val' unsolved, generalized))
120+ return ((ident, (foldr (Abs . Left . (\(x, _, _) -> x)) val' unsolved, generalized)), unsolved)
115121
116122 -- Show warnings here, since types in wildcards might have been solved during
117123 -- instance resolution (by functional dependencies).
118− finalSubst <- gets checkSubstitution
119− escalateWarningWhen isHoleError . tell . onErrorMessages (replaceTypes finalSubst) $ w
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
120129
121− return inferred
130+ return (map fst inferred)
122131 where
132+ replaceTypes
133+ :: Substitution
134+ -> ErrorMessage
135+ -> ErrorMessage
123136 replaceTypes subst = onTypesInErrorMessage (substituteType subst)
124137
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
153+
125154 -- | Generalize type vars using forall and add inferred constraints
126155 generalize unsolved = varIfUnknown . constrain unsolved
127156
128157 -- | Add any unsolved constraints
129158 constrain [] = id
130− constrain cs = ConstrainedType (map snd cs)
159+ constrain cs = ConstrainedType (map (\(_, _, x) -> x) cs)
131160
132161 -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
133− 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
134163
135164 isHoleError :: ErrorMessage -> Bool
136165 isHoleError (ErrorMessage _ HoleInferredType{}) = True
@@ -199,19 +228,12 @@ typeForBindingGroupElement (ident, val) dict untypedDict = do
199228-- | Check if a value contains a type annotation
200229isTyped :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))
201230isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
231+isTyped (name, PositionedValue pos c value) =
232+ bimap (second (PositionedValue pos c))
233+ (second (\(e, t, b) -> (PositionedValue pos c e, t, b)))
234+ (isTyped (name, value))
202235isTyped (name, value) = Left (name, value)
203236
204−-- |
205−-- Map a function over type annotations appearing inside a value
206−--
207−overTypes :: (Type -> Type) -> Expr -> Expr
208−overTypes f = let (_, f', _) = everywhereOnValues id g id in f'
209− where
210− g :: Expr -> Expr
211− g (TypedValue checkTy val t) = TypedValue checkTy val (f t)
212− g (TypeClassDictionary c sco hints) = TypeClassDictionary (mapConstraintArgs (map f) c) sco hints
213− g other = other
214−
215237-- | Check the kind of a type, failing if it is not of kind *.
216238checkTypeKind ::
217239 (MonadError MultipleErrors m) =>
@@ -339,7 +361,8 @@ infer' (TypedValue checkType val ty) = do
339361infer' (Hole name) = do
340362 ty <- freshType
341363 ctx <- getLocalContext
342− tell . errorMessage $ HoleInferredType name ty ctx
364+ env <- getEnv
365+ tell . errorMessage $ HoleInferredType name ty ctx (TSBefore env)
343366 return $ TypedValue True (Hole name) ty
344367infer' (PositionedValue pos c val) = warnAndRethrowWithPositionTC pos $ do
345368 TypedValue t v ty <- infer' val
@@ -568,18 +591,14 @@ check' (Abs (Right _) _) _ = internalError "Binder was not desugared"
568591check' (App f arg) ret = do
569592 f'@(TypedValue _ _ ft) <- infer f
570593 (retTy, app) <- checkFunctionApplication f' ft arg
571− v' <- subsumes (Just app) retTy ret
572− case v' of
573− Nothing -> internalError "check: unable to check the subsumes relation."
574− Just app' -> return $ TypedValue True app' ret
594+ elaborate <- subsumes retTy ret
595+ return $ TypedValue True (elaborate app) ret
575596check' v@(Var var) ty = do
576597 checkVisibility var
577598 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable $ var
578599 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
579− v' <- subsumes (Just v) repl ty'
580− case v' of
581− Nothing -> internalError "check: unable to check the subsumes relation."
582− Just v'' -> return $ TypedValue True v'' ty'
600+ elaborate <- subsumes repl ty'
601+ return $ TypedValue True (elaborate v) ty'
583602check' (DeferredDictionary className tys) _ = do
584603 {-
585604 -- Here, we replace a placeholder for a superclass dictionary with a regular
@@ -596,12 +615,11 @@ check' (TypedValue checkType val ty1) ty2 = do
596615 checkTypeKind ty1 kind
597616 ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1
598617 ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2
599− val' <- subsumes (Just val) ty1' ty2'
600− case val' of
601− Nothing -> internalError "check: unable to check the subsumes relation."
602− Just _ -> do
603− val''' <- if checkType then withScopedTypeVars moduleName args (check val ty2') else return val
604− return $ TypedValue checkType val''' ty2'
618+ _ <- subsumes ty1' ty2'
619+ val' <- if checkType
620+ then withScopedTypeVars moduleName args (check val ty2')
621+ else return val
622+ return $ TypedValue checkType val' ty2'
605623check' (Case vals binders) ret = do
606624 (vals', ts) <- instantiateForBinders vals binders
607625 binders' <- checkBinders ts ret binders
@@ -638,10 +656,8 @@ check' v@(Constructor c) ty = do
638656 Nothing -> throwError . errorMessage . UnknownName . fmap DctorName $ c
639657 Just (_, _, ty1, _) -> do
640658 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
641− mv <- subsumes (Just v) repl ty
642− case mv of
643− Nothing -> internalError "check: unable to check the subsumes relation."
644− Just v' -> return $ TypedValue True v' ty
659+ elaborate <- subsumes repl ty
660+ return $ TypedValue True (elaborate v) ty
645661check' (Let ds val) ty = do
646662 (ds', val') <- inferLetBinding [] ds val (`check` ty)
647663 return $ TypedValue True (Let ds' val') ty
@@ -654,10 +670,8 @@ check' (PositionedValue pos c val) ty = warnAndRethrowWithPositionTC pos $ do
654670 return $ TypedValue t (PositionedValue pos c v) ty'
655671check' val ty = do
656672 TypedValue _ val' ty' <- infer val
657− mt <- subsumes (Just val') ty' ty
658− case mt of
659− Nothing -> internalError "check: unable to check the subsumes relation."
660− Just v' -> return $ TypedValue True v' ty
673+ elaborate <- subsumes ty' ty
674+ return $ TypedValue True (elaborate val') ty
661675
662676-- |
663677-- Check the type of a collection of named record fields