@@ -117,7 +117,7 @@ unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 +
117117 unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty
118118 unifyTypes' (ForAll ident1 ty1) (ForAll ident2 ty2) = do
119119 sk <- skolemize ident1 ty1
120− replaced <- replaceVarsWithUnknowns [ident2] ty2
120+ replaced <- replaceVarWithUnknown ident2 ty2
121121 sk `unifyTypes` replaced
122122 unifyTypes' (ForAll ident ty1) ty2 = do
123123 sk <- skolemize ident ty1
@@ -216,32 +216,14 @@ replaceRowVars name r = everywhere (mkT replace)
216216 replace t = t
217217
218218replaceAllVarsWithUnknowns :: Type -> Subst Check Type
219−replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarsWithUnknowns [ident] ty >>= replaceAllVarsWithUnknowns
219+replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
220220replaceAllVarsWithUnknowns ty = return ty
221221
222−replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type
223−replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
224− where
225− f :: Type -> StateT (M.Map String Int) (Subst Check) Type
226− f (TypeVar var) | var `elem` idents = do
227− m <- get
228− n <- lift fresh'
229− case M.lookup var m of
230− Nothing -> do
231− put (M.insert var n m)
232− return $ TUnknown (Unknown n)
233− Just u -> return $ TUnknown (Unknown u)
234− f t = return t
235− g :: Row -> StateT (M.Map String Int) (Subst Check) Row
236− g (RowVar var) | var `elem` idents = do
237− m <- get
238− n <- lift fresh'
239− case M.lookup var m of
240− Nothing -> do
241− put (M.insert var n m)
242− return $ RUnknown (Unknown n)
243− Just u -> return $ RUnknown (Unknown u)
244− g r = return r
222+replaceVarWithUnknown :: String -> Type -> Subst Check Type
223+replaceVarWithUnknown ident ty = do
224+ tu <- fresh
225+ ru <- fresh
226+ return $ replaceRowVars ident ru . replaceTypeVars ident tu $ ty
245227
246228replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
247229replaceAllTypeSynonyms d = do
@@ -380,7 +362,7 @@ inferProperty (SaturatedTypeSynonym name args) prop = do
380362 replaced <- expandTypeSynonym name args
381363 inferProperty replaced prop
382364inferProperty (ForAll ident ty) prop = do
383− replaced <- replaceVarsWithUnknowns [ident] ty
365+ replaced <- replaceVarWithUnknown ident ty
384366 inferProperty replaced prop
385367inferProperty _ prop = return Nothing
386368
@@ -742,7 +724,7 @@ checkFunctionApplication' m (Function argTys retTy) args ret = do
742724 zipWithM (check m) args argTys
743725 retTy `subsumes` ret
744726checkFunctionApplication' m (ForAll ident ty) args ret = do
745− replaced <- replaceVarsWithUnknowns [ident] ty
727+ replaced <- replaceVarWithUnknown ident ty
746728 checkFunctionApplication m replaced args ret
747729checkFunctionApplication' m u@(TUnknown _) args ret = do
748730 tyArgs <- mapM (\arg -> infer m arg >>= replaceAllVarsWithUnknowns) args
@@ -757,7 +739,7 @@ checkFunctionApplication' _ fnTy args ret = throwError $ "Cannot apply function
757739
758740subsumes :: Type -> Type -> Subst Check ()
759741subsumes (ForAll ident ty1) ty2 = do
760− replaced <- replaceVarsWithUnknowns [ident] ty1
742+ replaced <- replaceVarWithUnknown ident ty1
761743 replaced `subsumes` ty2
762744subsumes (Function args1 ret1) (Function args2 ret2) = do
763745 zipWithM subsumes args2 args1