+----------------------------------------
+check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
+check_poly_type (Rank 0) ubx_tup ty
+ = check_tau_type (Rank 0) ubx_tup ty
+
+check_poly_type rank ubx_tup ty
+ = let
+ (tvs, theta, tau) = tcSplitSigmaTy ty
+ in
+ check_valid_theta SigmaCtxt theta `thenTc_`
+ check_tau_type (decRank rank) ubx_tup tau `thenTc_`
+ checkFreeness tvs theta `thenTc_`
+ checkAmbiguity tvs theta (tyVarsOfType tau)
+
+----------------------------------------
+check_arg_type :: Type -> TcM ()
+-- The sort of type that can instantiate a type variable,
+-- or be the argument of a type constructor.
+-- Not an unboxed tuple, not a forall.
+-- Other unboxed types are very occasionally allowed as type
+-- arguments depending on the kind of the type constructor
+--
+-- For example, we want to reject things like:
+--
+-- instance Ord a => Ord (forall s. T s a)
+-- and
+-- g :: T s (forall b.b)
+--
+-- NB: unboxed tuples can have polymorphic or unboxed args.
+-- This happens in the workers for functions returning
+-- product types with polymorphic components.
+-- But not in user code.
+-- Anyway, they are dealt with by a special case in check_tau_type
+
+check_arg_type ty
+ = check_tau_type (Rank 0) UT_NotOk ty `thenTc_`
+ checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
+
+----------------------------------------
+check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
+-- Rank is allowed rank for function args
+-- No foralls otherwise
+
+check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
+ check_source_ty dflags TypeCtxt sty
+check_tau_type rank ubx_tup (TyVarTy _) = returnTc ()
+check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
+ = check_poly_type rank UT_NotOk arg_ty `thenTc_`
+ check_tau_type rank UT_Ok res_ty
+
+check_tau_type rank ubx_tup (AppTy ty1 ty2)
+ = check_arg_type ty1 `thenTc_` check_arg_type ty2
+
+check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
+ -- Synonym notes are built only when the synonym is
+ -- saturated (see Type.mkSynTy)
+ = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
+ (if gla_exts then
+ -- If -fglasgow-exts then don't check the 'note' part.
+ -- This allows us to instantiate a synonym defn with a
+ -- for-all type, or with a partially-applied type synonym.
+ -- e.g. type T a b = a
+ -- type S m = m ()
+ -- f :: S (T Int)
+ -- Here, T is partially applied, so it's illegal in H98.
+ -- But if you expand S first, then T we get just
+ -- f :: Int
+ -- which is fine.
+ returnTc ()
+ else
+ -- For H98, do check the un-expanded part
+ check_tau_type rank ubx_tup syn
+ ) `thenTc_`
+
+ check_tau_type rank ubx_tup ty
+
+check_tau_type rank ubx_tup (NoteTy other_note ty)
+ = check_tau_type rank ubx_tup ty
+
+check_tau_type rank ubx_tup ty@(TyConApp tc tys)
+ | isSynTyCon tc
+ = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
+ -- synonym application, leaving it to checkValidType (i.e. right here)
+ -- to find the error
+ checkTc syn_arity_ok arity_msg `thenTc_`
+ mapTc_ check_arg_type tys
+
+ | isUnboxedTupleTyCon tc
+ = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
+ checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenTc_`
+ mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
+ -- Args are allowed to be unlifted, or
+ -- more unboxed tuples, so can't use check_arg_ty
+
+ | otherwise
+ = mapTc_ check_arg_type tys
+
+ where
+ ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
+
+ syn_arity_ok = tc_arity <= n_args
+ -- It's OK to have an *over-applied* type synonym
+ -- data Tree a b = ...
+ -- type Foo a = Tree [a]
+ -- f :: Foo a b -> ...
+ n_args = length tys
+ tc_arity = tyConArity tc
+
+ arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
+ ubx_tup_msg = ubxArgTyErr ty
+
+----------------------------------------
+forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
+unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
+ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
+kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind