+ tcHsTyVars tv_names kind_check $ \ tyvars ->
+ tcContext ctxt `thenTc` \ theta ->
+ tcHsType ty `thenTc` \ tau ->
+ checkAmbiguity full_ty tyvars theta tau `thenTc_`
+ returnTc (mkSigmaTy tyvars theta tau)
+
+ -- 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
+ --
+ -- NOTE: 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.
+ -- This is the is_free test below.
+
+checkAmbiguity full_ty forall_tyvars theta tau
+ = mapTc check_pred theta
+ where
+ tau_vars = tyVarsOfType tau
+ fds = instFunDepsOfTheta theta
+ tvFundep = tyVarFunDep fds
+ extended_tau_vars = oclose tvFundep tau_vars
+
+ is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
+ not (ct_var `elemUFM` extended_tau_vars)
+ is_free ct_var = not (ct_var `elem` forall_tyvars)
+
+ check_pred pred = checkTc (not any_ambig) (ambigErr pred full_ty) `thenTc_`
+ checkTc (not all_free) (freeErr pred full_ty)
+ where
+ ct_vars = varSetElems (tyVarsOfPred pred)
+ all_free = all is_free ct_vars
+ any_ambig = is_source_polytype && any is_ambig ct_vars
+
+ -- Notes on the 'is_source_polytype' test above
+ -- Check ambiguity only for source-program 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).
+ is_source_polytype
+ = case full_ty of
+ HsForAllTy (Just (UserTyVar _ : _)) _ _ -> True
+ other -> False