@@ -297,9 +297,9 @@ skolemEscapeCheck (TypedValue False _ _) = return ()
297297skolemEscapeCheck root@(TypedValue _ _ _) =
298298 case everythingWithContext [] (++) (mkQ ((,) []) go) root of
299299 [] -> return ()
300− ((binding, val) : _) -> throwError $ "Rigid/skolem type variable bound by " ++ prettyPrintValue binding ++ " has escaped at " ++ prettyPrintValue val
300+ ((binding, val) : _) -> throwError $ "Rigid/skolem type variable bound by " ++ maybe "<unknown>" prettyPrintValue binding ++ " has escaped at " ++ prettyPrintValue val
301301 where
302− go :: Value -> [(SkolemScope, Value)] -> ([(Value, Value)], [(SkolemScope, Value)])
302+ go :: Value -> [(SkolemScope, Value)] -> ([(Maybe Value, Value)], [(SkolemScope, Value)])
303303 go val@(TypedValue _ _ (ForAll _ _ (Just sco))) scos = ([], (sco, val) : scos)
304304 go val@(TypedValue _ _ ty) scos = case collectSkolems ty \\ map fst scos of
305305 (sco : _) -> ([(findBindingScope sco, val)], scos)
@@ -311,8 +311,8 @@ skolemEscapeCheck root@(TypedValue _ _ _) =
311311 collect (Skolem _ scope) = [scope]
312312 collect _ = []
313313 go _ scos = ([], scos)
314− findBindingScope :: SkolemScope -> Value
315− findBindingScope sco = fromMaybe (error "No introducing ForAll for skolem variable.") $ something (mkQ Nothing go) root
314+ findBindingScope :: SkolemScope -> Maybe Value
315+ findBindingScope sco = something (mkQ Nothing go) root
316316 where
317317 go val@(TypedValue _ _ (ForAll _ _ (Just sco'))) | sco == sco' = Just val
318318 go _ = Nothing
@@ -730,6 +730,10 @@ check' val t@(ConstrainedType constraints ty) = do
730730 (qualifyAllUnqualifiedNames moduleName env constraints)) $
731731 check val ty
732732 return $ TypedValue True (foldr Abs val' dictNames) t
733+check' val t@(SaturatedTypeSynonym name args) = do
734+ ty <- introduceSkolemScope <=< expandTypeSynonym name $ args
735+ val' <- check val ty
736+ return $ TypedValue True val' ty
733737check' val u@(TUnknown _) = do
734738 val'@(TypedValue _ _ ty) <- infer val
735739 -- Don't unify an unknown with an inferred polytype
@@ -812,10 +816,6 @@ check' (Constructor c) ty = do
812816 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
813817 _ <- subsumes Nothing repl ty
814818 return $ TypedValue True (Constructor c) ty
815−check' val t@(SaturatedTypeSynonym name args) = do
816− ty <- introduceSkolemScope <=< expandTypeSynonym name $ args
817− val' <- check val ty
818− return $ TypedValue True val' ty
819819check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
820820
821821-- |