+Note [Non-injective type functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's very confusing to get a message like
+ Couldn't match expected type `Depend s'
+ against inferred type `Depend s1'
+so pp_open_tc adds:
+ NB: `Depend' is type function, and hence may not be injective
+
+Currently we add this independently for each argument, so we also get
+ Couldn't match expected type `a'
+ against inferred type `Dual (Dual a)'
+ NB: `Dual' is a (non-injective) type function
+which is arguably redundant. But on the other hand, it's probably
+a good idea for the programmer to know the error involves type functions
+so I've left it in for now. The obvious alternative is to only add
+this NB in the case of matching (T ...) ~ (T ...).
+
+