-Using oclose
-~~~~~~~~~~~~
-oclose is used
-
-a) When determining ambiguity. The type
- forall a,b. C a b => a
-is not ambiguous (given the above class decl for C) because
-a determines b.
-
-b) When generalising a type T. Usually we take FV(T) \ FV(Env),
-but in fact we need
- FV(T) \ (FV(Env)+)
-where the '+' is the oclosure operation. Notice that we do not
-take FV(T)+. This puzzled me for a bit. Consider
-
- f = E
-
-and suppose e have that E :: C a b => a, and suppose that b is
-free in the environment. Then we quantify over 'a' only, giving
-the type forall a. C a b => a. Since a->b but we don't have b->a,
-we might have instance decls like
- instance C Bool Int where ...
- instance C Char Int where ...
-so knowing that b=Int doesn't fix 'a'; so we quantify over it.
-
- ---------------
- A WORRY: ToDo!
- ---------------
-If we have class C a b => D a b where ....
- class D a b | a -> b where ...
-and the preds are [C (x,y) z], then we want to see the fd in D,
-even though it is not explicit in C, giving [({x,y},{z})]
-
-Similarly for instance decls? E.g. Suppose we have
- instance C a b => Eq (T a b) where ...
-and we infer a type t with constraints Eq (T a b) for a particular
-expression, and suppose that 'a' is free in the environment.
-We could generalise to
- forall b. Eq (T a b) => t
-but if we reduced the constraint, to C a b, we'd see that 'a' determines
-b, so that a better type might be
- t (with free constraint C a b)
-Perhaps it doesn't matter, because we'll still force b to be a
-particular type at the call sites. Generalising over too many
-variables (provided we don't shadow anything by quantifying over a
-variable that is actually free in the envt) may postpone errors; it
-won't hide them altogether.
-
+oclose is used (only) when generalising a type T; see extensive
+notes in TcSimplify.
+
+Note [Important subtlety in oclose]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (oclose (C Int t) {}), where class C a b | a->b
+Then, since a->b, 't' is fully determined by Int, and the
+uniform thing is to return {t}.
+
+However, consider
+ class D a b c | b->c
+ f x = e -- 'e' generates constraint (D s Int t)
+ -- \x.e has type s->s
+Then, if (oclose (D s Int t) {}) = {t}, we'll make the function
+monomorphic in 't', thus
+ f :: forall s. D s Int t => s -> s
+
+But if this function is never called, 't' will never be instantiated;
+the functional dependencies that fix 't' may well be instance decls in
+some importing module. But the top-level defaulting of unconstrained
+type variables will fix t=GHC.Prim.Any, and that's simply a bug.
+
+Conclusion: oclose only returns a type variable as "fixed" if it
+depends on at least one type variable in the input fixed_tvs.
+
+Remember, it's always sound for oclose to return a smaller set.
+An interesting example is tcfail093, where we get this inferred type:
+ class C a b | a->b
+ dup :: forall h. (Call (IO Int) h) => () -> Int -> h
+This is perhaps a bit silly, because 'h' is fixed by the (IO Int);
+previously GHC rejected this saying 'no instance for Call (IO Int) h'.
+But it's right on the borderline. If there was an extra, otherwise
+uninvolved type variable, like 's' in the type of 'f' above, then
+we must accept the function. So, for now anyway, we accept 'dup' too.