+Check for ambiguity
+~~~~~~~~~~~~~~~~~~~
+ forall V. P => tau
+is ambiguous if P contains generic variables
+(i.e. one of the Vs) that are not mentioned in tau
+
+However, we need to take account of functional dependencies
+when we speak of 'mentioned in tau'. Example:
+ class C a b | a -> b where ...
+Then the type
+ forall x y. (C x y) => x
+is not ambiguous because x is mentioned and x determines y
+
+NB; the ambiguity check is only used for *user* types, not for types
+coming from inteface files. The latter can legitimately have
+ambiguous types. Example
+
+ class S a where s :: a -> (Int,Int)
+ instance S Char where s _ = (1,1)
+ f:: S a => [a] -> Int -> (Int,Int)
+ f (_::[a]) x = (a*x,b)
+ where (a,b) = s (undefined::a)
+
+Here the worker for f gets the type
+ fw :: forall a. S a => Int -> (# Int, Int #)
+
+If the list of tv_names is empty, we have a monotype, and then we
+don't need to check for ambiguity either, because the test can't fail
+(see is_ambig).
+
+\begin{code}
+checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
+checkAmbiguity forall_tyvars theta tau_tyvars
+ = mappM_ complain (filter is_ambig theta)
+ where
+ complain pred = addErrTc (ambigErr pred)
+ extended_tau_vars = grow theta tau_tyvars
+
+ -- Only a *class* predicate can give rise to ambiguity
+ -- An *implicit parameter* cannot. For example:
+ -- foo :: (?x :: [a]) => Int
+ -- foo = length ?x
+ -- is fine. The call site will suppply a particular 'x'
+ is_ambig pred = isClassPred pred &&
+ any ambig_var (varSetElems (tyVarsOfPred pred))
+
+ ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
+ not (ct_var `elemVarSet` extended_tau_vars)
+
+ambigErr pred
+ = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
+ nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
+ ptext SLIT("must be reachable from the type after the '=>'"))]
+\end{code}
+
+In addition, GHC insists that at least one type variable
+in each constraint is in V. So we disallow a type like
+ forall a. Eq b => b -> b
+even in a scope where b is in scope.
+