@@ -107,7 +107,6 @@ unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 +
107107 sk `unifyTypes` ty2
108108 unifyTypes' ForAll{} _ = throwError "Skolem variable scope is unspecified"
109109 unifyTypes' ty f@ForAll{} = f `unifyTypes` ty
110− unifyTypes' (Object row1) (Object row2) = row1 =?= row2
111110 unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
112111 unifyTypes' (TypeConstructor c1) (TypeConstructor c2) =
113112 guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (c1 == c2)
@@ -475,6 +474,12 @@ expandTypeSynonym name args = do
475474 env <- getEnv
476475 either throwError return $ expandTypeSynonym' env name args
477476
477+expandAllTypeSynonyms :: (Functor m, Monad m, MonadState CheckState m, MonadError String m) => Type -> m Type
478+expandAllTypeSynonyms = everywhereM' (mkM go)
479+ where
480+ go (SaturatedTypeSynonym name args) = expandTypeSynonym name args
481+ go other = return other
482+
478483-- |
479484-- Ensure a set of property names and value does not contain duplicate labels
480485--
@@ -503,7 +508,7 @@ infer' (ObjectLiteral ps) = do
503508 ensureNoDuplicateProperties ps
504509 ts <- mapM (infer . snd) ps
505510 let fields = zipWith (\name (TypedValue _ _ t) -> (name, t)) (map fst ps) ts
506− ty = Object $ rowFromList (fields, REmpty)
511+ ty = TypeApp tyObject $ rowFromList (fields, REmpty)
507512 return $ TypedValue True (ObjectLiteral (zip (map fst ps) ts)) ty
508513infer' (ObjectUpdate o ps) = do
509514 ensureNoDuplicateProperties ps
@@ -511,9 +516,9 @@ infer' (ObjectUpdate o ps) = do
511516 newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps
512517 let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals
513518 oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh
514− let oldTy = Object $ rowFromList (oldTys, row)
519+ let oldTy = TypeApp tyObject $ rowFromList (oldTys, row)
515520 o' <- TypedValue True <$> check o oldTy <*> pure oldTy
516− return $ TypedValue True (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)
521+ return $ TypedValue True (ObjectUpdate o' newVals) $ TypeApp tyObject $ rowFromList (newTys, row)
517522infer' (Accessor prop val) = do
518523 typed@(TypedValue _ _ objTy) <- infer val
519524 propTy <- inferProperty objTy prop
@@ -521,7 +526,7 @@ infer' (Accessor prop val) = do
521526 Nothing -> do
522527 field <- fresh
523528 rest <- fresh
524− _ <- subsumes Nothing objTy (Object (RCons prop field rest))
529+ _ <- subsumes Nothing objTy (TypeApp tyObject (RCons prop field rest))
525530 return $ TypedValue True (Accessor prop typed) field
526531 Just ty -> return $ TypedValue True (Accessor prop typed) ty
527532infer' (Abs (Left arg) ret) = do
@@ -593,7 +598,7 @@ inferLetBinding _ _ _ _ = error "Invalid argument to fromValueDeclaration"
593598-- Infer the type of a property inside a record with a given type
594599--
595600inferProperty :: Type -> String -> UnifyT Type Check (Maybe Type)
596−inferProperty (Object row) prop = do
601+inferProperty (TypeApp obj row) prop | obj == tyObject = do
597602 let (props, _) = rowToList row
598603 return $ lookup prop props
599604inferProperty (SaturatedTypeSynonym name args) prop = do
@@ -632,7 +637,7 @@ inferBinder val (ObjectBinder props) = do
632637 row <- fresh
633638 rest <- fresh
634639 m1 <- inferRowProperties row rest props
635− val =?= Object row
640+ val =?= TypeApp tyObject row
636641 return m1
637642 where
638643 inferRowProperties :: Type -> Type -> [(String, Binder)] -> UnifyT Type Check (M.Map Ident Type)
@@ -736,8 +741,7 @@ check' val t@(ConstrainedType constraints ty) = do
736741 return $ TypedValue True (foldr (Abs . Left) val' dictNames) t
737742check' val (SaturatedTypeSynonym name args) = do
738743 ty <- introduceSkolemScope <=< expandTypeSynonym name $ args
739− val' <- check val ty
740− return $ TypedValue True val' ty
744+ check val ty
741745check' val u@(TUnknown _) = do
742746 val'@(TypedValue _ _ ty) <- infer val
743747 -- Don't unify an unknown with an inferred polytype
@@ -792,22 +796,22 @@ check' (IfThenElse cond th el) ty = do
792796 th' <- check th ty
793797 el' <- check el ty
794798 return $ TypedValue True (IfThenElse cond' th' el') ty
795−check' (ObjectLiteral ps) t@(Object row) = do
799+check' (ObjectLiteral ps) t@(TypeApp obj row) | obj == tyObject = do
796800 ensureNoDuplicateProperties ps
797801 ps' <- checkProperties ps row False
798802 return $ TypedValue True (ObjectLiteral ps') t
799−check' (ObjectUpdate obj ps) t@(Object row) = do
803+check' (ObjectUpdate obj ps) t@(TypeApp o row) | o == tyObject = do
800804 ensureNoDuplicateProperties ps
801805 us <- zip (map fst ps) <$> replicateM (length ps) fresh
802806 let (propsToCheck, rest) = rowToList row
803807 propsToRemove = map fst ps
804808 remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck
805− obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))
809+ obj' <- check obj (TypeApp tyObject (rowFromList (us ++ remainingProps, rest)))
806810 ps' <- checkProperties ps row True
807811 return $ TypedValue True (ObjectUpdate obj' ps') t
808812check' (Accessor prop val) ty = do
809813 rest <- fresh
810− val' <- check val (Object (RCons prop ty rest))
814+ val' <- check val (TypeApp tyObject (RCons prop ty rest))
811815 return $ TypedValue True (Accessor prop val') ty
812816check' (Constructor c) ty = do
813817 env <- getEnv
@@ -820,8 +824,16 @@ check' (Constructor c) ty = do
820824check' (Let ds val) ty = do
821825 (ds', val') <- inferLetBinding [] ds val (flip check ty)
822826 return $ TypedValue True (Let ds' val') ty
827+check' val ty | containsTypeSynonyms ty = do
828+ ty' <- introduceSkolemScope <=< expandAllTypeSynonyms $ ty
829+ check val ty'
823830check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
824831
832+containsTypeSynonyms :: Type -> Bool
833+containsTypeSynonyms = everything (||) (mkQ False go) where
834+ go (SaturatedTypeSynonym _ _) = True
835+ go _ = False
836+
825837-- |
826838-- Check the type of a collection of named record fields
827839--
@@ -854,7 +866,7 @@ checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
854866 v' <- check v ty
855867 ps'' <- go ps' (delete (p, ty) ts) r
856868 return $ (p, v') : ps''
857− go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (Object row)
869+ go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (TypeApp tyObject row)
858870
859871-- |
860872-- Check the type of a function application, rethrowing errors to provide a better error message
@@ -939,7 +951,7 @@ subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do
939951 dicts <- getTypeClassDictionaries
940952 _ <- subsumes' Nothing ty1 ty2
941953 return . Just $ foldl App val (map (flip TypeClassDictionary dicts) constraints)
942−subsumes' val (Object r1) (Object r2) = do
954+subsumes' val (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyObject && f2 == tyObject = do
943955 let
944956 (ts1, r1') = rowToList r1
945957 (ts2, r2') = rowToList r2
@@ -959,7 +971,7 @@ subsumes' val (Object r1) (Object r2) = do
959971 | otherwise = do rest <- fresh
960972 r1' =?= RCons p2 ty2 rest
961973 go ((p1, ty1) : ts1) ts2 rest r2'
962−subsumes' val ty1 ty2@(Object _) = subsumes val ty2 ty1
974+subsumes' val ty1 ty2@(TypeApp obj _) | obj == tyObject = subsumes val ty2 ty1
963975subsumes' val ty1 ty2 = do
964976 ty1 =?= ty2
965977 return val