@@ -34,13 +34,14 @@ import Control.Monad.Supply.Class (MonadSupply)
3434import Control.Monad.Writer.Class (MonadWriter(..))
3535
3636import Data.Bifunctor (bimap)
37−import Data.Either (lefts, rights)
37+import Data.Either (partitionEithers)
3838import Data.Functor (($>))
3939import Data.List (transpose, nub, (\\), partition, delete)
4040import Data.Maybe (fromMaybe)
4141import Data.Monoid ((<>))
4242import qualified Data.Map as M
4343import qualified Data.Set as S
44+import Data.Traversable (for)
4445
4546import Language.PureScript.AST
4647import Language.PureScript.Crash
@@ -62,7 +63,6 @@ import Language.PureScript.Types
6263import Language.PureScript.Label (Label(..))
6364import Language.PureScript.PSString (PSString)
6465
65−
6666data BindingGroupType
6767 = RecursiveBindingGroup
6868 | NonRecursiveBindingGroup
@@ -78,9 +78,9 @@ typesOf
7878 -> m [(Ident, (Expr, Type))]
7979typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
8080 tys <- capturingSubstitution tidyUp $ do
81− (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup (Just moduleName) vals
81+ SplitBindingGroup untyped typed dict <- typeDictionaryForBindingGroup (Just moduleName) vals
8282 ds1 <- parU typed $ \e -> withoutWarnings $ checkTypedBindingGroupElement moduleName e dict
83− ds2 <- forM untyped $ \e -> withoutWarnings $ typeForBindingGroupElement e dict untypedDict
83+ ds2 <- forM untyped $ \e -> withoutWarnings $ typeForBindingGroupElement e dict
8484 return (map (False, ) ds1 ++ map (True, ) ds2)
8585
8686 inferred <- forM tys $ \(shouldGeneralize, ((ident, (val, ty)), _)) -> do
@@ -166,81 +166,101 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
166166 isHoleError (ErrorMessage _ HoleInferredType{}) = True
167167 isHoleError _ = False
168168
169−type TypeData = M.Map (Qualified Ident) (Type, NameKind, NameVisibility)
170−
171−type UntypedData = [(Ident, Type)]
172−
169+-- | A binding group contains multiple value definitions, some of which are typed
170+-- and some which are not.
171+--
172+-- This structure breaks down a binding group into typed and untyped parts.
173+data SplitBindingGroup = SplitBindingGroup
174+ { _splitBindingGroupUntyped :: [(Ident, (Expr, Type))]
175+ -- ^ The untyped expressions
176+ , _splitBindingGroupTyped :: [(Ident, (Expr, Type, Bool))]
177+ -- ^ The typed expressions, along with their type annotations
178+ , _splitBindingGroupNames :: M.Map (Qualified Ident) (Type, NameKind, NameVisibility)
179+ -- ^ A map containing all expressions and their assigned types (which might be
180+ -- fresh unification variables). These will be added to the 'Environment' after
181+ -- the binding group is checked, so the value type of the 'Map' is chosen to be
182+ -- compatible with the type of 'bindNames'.
183+ }
184+
185+-- | This function breaks a binding group down into two sets of declarations:
186+-- those which contain type annotations, and those which don't.
187+-- This function also generates fresh unification variables for the types of
188+-- declarations without type annotations, returned in the 'UntypedData' structure.
173189typeDictionaryForBindingGroup
174− :: (MonadState CheckState m)
190+ :: (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
175191 => Maybe ModuleName
176192 -> [(Ident, Expr)]
177− -> m ([(Ident, Expr)], [(Ident, (Expr, Type, Bool))], TypeData, UntypedData)
193+ -> m SplitBindingGroup
178194typeDictionaryForBindingGroup moduleName vals = do
179− let
180− -- Map each declaration to a name/value pair, with an optional type, if the declaration is typed
181− es = map isTyped vals
182− -- Filter the typed and untyped declarations
183− untyped = lefts es
184− typed = rights es
185− -- Make a map of names to typed declarations
186− typedDict = map (\(ident, (_, ty, _)) -> (ident, ty)) typed
187−
188− -- Create fresh unification variables for the types of untyped declarations
189− untypedNames <- replicateM (length untyped) freshType
190−
191− let
192− -- Make a map of names to the unification variables of untyped declarations
193− untypedDict = zip (map fst untyped) untypedNames
194− -- Create the dictionary of all name/type pairs, which will be added to the environment during type checking
195− dict = M.fromList (map (\(ident, ty) -> (Qualified moduleName ident, (ty, Private, Undefined))) $ typedDict ++ untypedDict)
196− return (untyped, typed, dict, untypedDict)
197−
195+ -- Filter the typed and untyped declarations and make a map of names to typed declarations.
196+ -- Replace type wildcards here so that the resulting dictionary of types contains the
197+ -- fully expanded types.
198+ let (untyped, typed) = partitionEithers (map splitTypeAnnotation vals)
199+ (typedDict, typed') <- fmap unzip . for typed $ \(ident, (expr, ty, checkType)) -> do
200+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
201+ return ((ident, ty'), (ident, (expr, ty', checkType)))
202+ -- Create fresh unification variables for the types of untyped declarations
203+ (untypedDict, untyped') <- fmap unzip . for untyped $ \(ident, expr) -> do
204+ ty <- freshType
205+ return ((ident, ty), (ident, (expr, ty)))
206+ -- Create the dictionary of all name/type pairs, which will be added to the
207+ -- environment during type checking
208+ let dict = M.fromList [ (Qualified moduleName ident, (ty, Private, Undefined))
209+ | (ident, ty) <- typedDict <> untypedDict
210+ ]
211+ return (SplitBindingGroup untyped' typed' dict)
212+ where
213+ -- | Check if a value contains a type annotation, and if so, separate it
214+ -- from the value itself.
215+ splitTypeAnnotation :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))
216+ splitTypeAnnotation (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
217+ splitTypeAnnotation (name, PositionedValue pos c value) =
218+ bimap (second (PositionedValue pos c))
219+ (second (\(e, t, b) -> (PositionedValue pos c e, t, b)))
220+ (splitTypeAnnotation (name, value))
221+ splitTypeAnnotation (name, value) = Left (name, value)
222+
223+-- | Check the type annotation of a typed value in a binding group.
198224checkTypedBindingGroupElement
199225 :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
200226 => ModuleName
201227 -> (Ident, (Expr, Type, Bool))
202− -> TypeData
228+ -- ^ The identifier we are trying to define, along with the expression and its type annotation
229+ -> M.Map (Qualified Ident) (Type, NameKind, NameVisibility)
230+ -- ^ Names brought into scope in this binding group
203231 -> m (Ident, (Expr, Type))
204−checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do
205− -- Replace type wildcards
206− ty' <- replaceTypeWildcards ty
232+checkTypedBindingGroupElement mn (ident, (val, ty, checkType)) dict = do
207233 -- Kind check
208234 (kind, args) <- kindOfWithScopedVars ty
209235 checkTypeKind ty kind
210236 -- Check the type with the new names in scope
211− ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'
212− val'' <- if checkType
213− then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''
214− else return (TypedValue False val' ty'')
215− return (ident, (val'', ty''))
237+ val' <- if checkType
238+ then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val ty <*> pure ty
239+ else return (TypedValue False val ty)
240+ return (ident, (val', ty))
216241
242+-- | Infer a type for a value in a binding group which lacks an annotation.
217243typeForBindingGroupElement
218244 :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
219− => (Ident, Expr)
220− -> TypeData
221− -> UntypedData
245+ => (Ident, (Expr, Type))
246+ -- ^ The identifier we are trying to define, along with the expression and its assigned type
247+ -- (at this point, this should be a unification variable)
248+ -> M.Map (Qualified Ident) (Type, NameKind, NameVisibility)
249+ -- ^ Names brought into scope in this binding group
222250 -> m (Ident, (Expr, Type))
223−typeForBindingGroupElement (ident, val) dict untypedDict = do
251+typeForBindingGroupElement (ident, (val, ty)) dict = do
224252 -- Infer the type with the new names in scope
225− TypedValue _ val' ty <- bindNames dict $ infer val
226− unifyTypes ty $ fromMaybe (internalError "name not found in dictionary") (lookup ident untypedDict)
227− return (ident, (TypedValue True val' ty, ty))
228−
229−-- | Check if a value contains a type annotation
230−isTyped :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))
231−isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
232−isTyped (name, PositionedValue pos c value) =
233− bimap (second (PositionedValue pos c))
234− (second (\(e, t, b) -> (PositionedValue pos c e, t, b)))
235− (isTyped (name, value))
236−isTyped (name, value) = Left (name, value)
253+ TypedValue _ val' ty' <- bindNames dict $ infer val
254+ -- Unify the type with the unification variable we chose for this definition
255+ unifyTypes ty ty'
256+ return (ident, (TypedValue True val' ty', ty'))
237257
238258-- | Check the kind of a type, failing if it is not of kind *.
239−checkTypeKind ::
240− (MonadError MultipleErrors m) =>
241− Type ->
242− Kind ->
243− m ()
259+checkTypeKind
260+ :: MonadError MultipleErrors m
261+ => Type
262+ -> Kind
263+ -> m ()
244264checkTypeKind ty kind = guardWith (errorMessage (ExpectedType ty kind)) $ kind == kindType
245265
246266-- | Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
@@ -248,11 +268,11 @@ checkTypeKind ty kind = guardWith (errorMessage (ExpectedType ty kind)) $ kind =
248268--
249269-- This is necessary during type checking to avoid unifying a polymorphic type with a
250270-- unification variable.
251−instantiatePolyTypeWithUnknowns ::
252− (MonadState CheckState m, MonadError MultipleErrors m) =>
253− Expr ->
254− Type ->
255− m (Expr, Type)
271+instantiatePolyTypeWithUnknowns
272+ :: (MonadState CheckState m, MonadError MultipleErrors m)
273+ => Expr
274+ -> Type
275+ -> m (Expr, Type)
256276instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do
257277 ty' <- replaceVarWithUnknown ident ty
258278 instantiatePolyTypeWithUnknowns val ty'
@@ -263,17 +283,17 @@ instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do
263283instantiatePolyTypeWithUnknowns val ty = return (val, ty)
264284
265285-- | Infer a type for a value, rethrowing any error to provide a more useful error message
266−infer ::
267− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
268− Expr ->
269− m Expr
286+infer
287+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
288+ => Expr
289+ -> m Expr
270290infer val = withErrorMessageHint (ErrorInferringType val) $ infer' val
271291
272292-- | Infer a type for a value
273−infer' ::
274− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
275− Expr ->
276− m Expr
293+infer'
294+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
295+ => Expr
296+ -> m Expr
277297infer' v@(Literal (NumericLiteral (Left _))) = return $ TypedValue True v tyInt
278298infer' v@(Literal (NumericLiteral (Right _))) = return $ TypedValue True v tyNumber
279299infer' v@(Literal (StringLiteral _)) = return $ TypedValue True v tyString
@@ -370,13 +390,13 @@ infer' (PositionedValue pos c val) = warnAndRethrowWithPositionTC pos $ do
370390 return $ TypedValue t (PositionedValue pos c v) ty
371391infer' v = internalError $ "Invalid argument to infer: " ++ show v
372392
373−inferLetBinding ::
374− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
375− [Declaration] ->
376− [Declaration] ->
377− Expr ->
378− (Expr -> m Expr) ->
379− m ([Declaration], Expr)
393+inferLetBinding
394+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
395+ => [Declaration]
396+ -> [Declaration]
397+ -> Expr
398+ -> (Expr -> m Expr)
399+ -> m ([Declaration], Expr)
380400inferLetBinding seen [] ret j = (,) seen <$> withBindingGroupVisible (j ret)
381401inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do
382402 Just moduleName <- checkCurrentModule <$> get
@@ -394,9 +414,9 @@ inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret
394414 bindNames (M.singleton (Qualified Nothing ident) (valTy', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right val')]) rest ret j
395415inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do
396416 Just moduleName <- checkCurrentModule <$> get
397− (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup Nothing (map (\(i, _, v) -> (i, v)) ds)
417+ SplitBindingGroup untyped typed dict <- typeDictionaryForBindingGroup Nothing (map (\(i, _, v) -> (i, v)) ds)
398418 ds1' <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
399− ds2' <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict
419+ ds2' <- forM untyped $ \e -> typeForBindingGroupElement e dict
400420 let ds' = [(ident, Private, val') | (ident, (val', _)) <- ds1' ++ ds2']
401421 bindNames dict $ do
402422 makeBindingGroupVisible
@@ -407,11 +427,12 @@ inferLetBinding seen (PositionedDeclaration pos com d : ds) ret j = warnAndRethr
407427inferLetBinding _ _ _ _ = internalError "Invalid argument to inferLetBinding"
408428
409429-- | Infer the types of variables brought into scope by a binder
410−inferBinder :: forall m.
411− (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
412− Type ->
413− Binder ->
414− m (M.Map Ident Type)
430+inferBinder
431+ :: forall m
432+ . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
433+ => Type
434+ -> Binder
435+ -> m (M.Map Ident Type)
415436inferBinder _ NullBinder = return M.empty
416437inferBinder val (LiteralBinder (StringLiteral _)) = unifyTypes val tyString >> return M.empty
417438inferBinder val (LiteralBinder (CharLiteral _)) = unifyTypes val tyChar >> return M.empty
@@ -486,11 +507,11 @@ binderRequiresMonotype (PositionedBinder _ _ b) = binderRequiresMonotype b
486507binderRequiresMonotype _ = True
487508
488509-- | Instantiate polytypes only when necessitated by a binder.
489−instantiateForBinders ::
490− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
491− [Expr] ->
492− [CaseAlternative] ->
493− m ([Expr], [Type])
510+instantiateForBinders
511+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
512+ => [Expr]
513+ -> [CaseAlternative]
514+ -> m ([Expr], [Type])
494515instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do
495516 TypedValue _ val' ty <- infer val
496517 if inst
@@ -503,12 +524,12 @@ instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do
503524-- |
504525-- Check the types of the return values in a set of binders in a case statement
505526--
506−checkBinders ::
507− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
508− [Type] ->
509− Type ->
510− [CaseAlternative] ->
511− m [CaseAlternative]
527+checkBinders
528+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
529+ => [Type]
530+ -> Type
531+ -> [CaseAlternative]
532+ -> m [CaseAlternative]
512533checkBinders _ _ [] = return []
513534checkBinders nvals ret (CaseAlternative binders result : bs) = do
514535 guardWith (errorMessage $ OverlappingArgNames Nothing) $
@@ -532,11 +553,11 @@ checkBinders nvals ret (CaseAlternative binders result : bs) = do
532553-- |
533554-- Check the type of a value, rethrowing errors to provide a better error message
534555--
535−check ::
536− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
537− Expr ->
538− Type ->
539− m Expr
556+check
557+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
558+ => Expr
559+ -> Type
560+ -> m Expr
540561check val ty = withErrorMessageHint (ErrorCheckingType val ty) $ check' val ty
541562
542563-- |
@@ -679,13 +700,13 @@ check' val ty = do
679700--
680701-- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case.
681702--
682−checkProperties ::
683− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
684− Expr ->
685− [(PSString, Expr)] ->
686− Type ->
687− Bool ->
688− m [(PSString, Expr)]
703+checkProperties
704+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
705+ => Expr
706+ -> [(PSString, Expr)]
707+ -> Type
708+ -> Bool
709+ -> m [(PSString, Expr)]
689710checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' where
690711 go [] [] REmpty = return []
691712 go [] [] u@(TUnknown _)