+Note [Avoid deferring]
+~~~~~~~~~~~~~~~~~~~~~~
+We try to avoid creating deferred constraints for two reasons.
+ * First, efficiency.
+ * Second, currently we can only defer some constraints
+ under a forall. See unifySigmaTy.
+So expanding synonyms here is a good thing to do. Example (Trac #4917)
+ a ~ Const a b
+where type Const a b = a. We can solve this immediately, even when
+'a' is a skolem, just by expanding the synonym; and we should do so
+ in case this unification happens inside unifySigmaTy (sigh).
+
+Note [Type synonyms and the occur check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generally speaking we try to update a variable with type synonyms not
+expanded, which improves later error messages, unless looking
+inside a type synonym may help resolve a spurious occurs check
+error. Consider:
+ type A a = ()
+
+ f :: (A a -> a -> ()) -> ()
+ f = \ _ -> ()
+
+ x :: ()
+ x = f (\ x p -> p x)
+
+We will eventually get a constraint of the form t ~ A t. The ok function above will
+properly expand the type (A t) to just (), which is ok to be unified with t. If we had
+unified with the original type A t, we would lead the type checker into an infinite loop.
+
+Hence, if the occurs check fails for a type synonym application, then (and *only* then),
+the ok function expands the synonym to detect opportunities for occurs check success using
+the underlying definition of the type synonym.
+
+The same applies later on in the constraint interaction code; see TcInteract,
+function @occ_check_ok@.
+
+