-\begin{code}
-uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
- -- ty1 is the *expected* type
-
- -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
- -- ty2 is the *actual* type
- -> TcM ()
-
- -- Always expand synonyms (see notes at end)
- -- (this also throws away FTVs)
-uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
-uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
-
- -- Ignore usage annotations inside typechecker
-uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
-uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
-
- -- Variables; go for uVar
-uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
-uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
- -- "True" means args swapped
-
- -- Predicates
-uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
- | n1 == n2 = uTys t1 t1 t2 t2
-uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
- | c1 == c2 = unifyTauTyLists tys1 tys2
-uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
- | tc1 == tc2 = unifyTauTyLists tys1 tys2
-
- -- Functions; just check the two parts
-uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
- = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
-
- -- Type constructors must match
-uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
- | con1 == con2 && length tys1 == length tys2
- = unifyTauTyLists tys1 tys2
-
- | con1 == openKindCon
- -- When we are doing kind checking, we might match a kind '?'
- -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
- -- (CCallable Int) and (CCallable Int#) are both OK
- = unifyOpenTypeKind ps_ty2
-
- -- Applications need a bit of care!
- -- They can match FunTy and TyConApp, so use splitAppTy_maybe
- -- NB: we've already dealt with type variables and Notes,
- -- so if one type is an App the other one jolly well better be too
-uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
- = case tcSplitAppTy_maybe ty2 of
- Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
- Nothing -> unifyMisMatch ps_ty1 ps_ty2
-
- -- Now the same, but the other way round
- -- Don't swap the types, because the error messages get worse
-uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
- = case tcSplitAppTy_maybe ty1 of
- Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
- Nothing -> unifyMisMatch ps_ty1 ps_ty2
-
- -- Not expecting for-alls in unification
- -- ... but the error message from the unifyMisMatch more informative
- -- than a panic message!
-
- -- Anything else fails
-uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
-\end{code}
+check_poly_type rank ubx_tup ty
+ = let
+ (tvs, theta, tau) = tcSplitSigmaTy ty
+ in
+ check_valid_theta SigmaCtxt theta `thenM_`
+ check_tau_type (decRank rank) ubx_tup tau `thenM_`
+ checkFreeness tvs theta `thenM_`
+ 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 `thenM_`
+ 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 ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
+ -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
+
+-- Naked PredTys don't usually show up, but they can as a result of
+-- {-# SPECIALISE instance Ord Char #-}
+-- The Right Thing would be to fix the way that SPECIALISE instance pragmas
+-- are handled, but the quick thing is just to permit PredTys here.
+check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
+ check_source_ty dflags TypeCtxt sty
+
+check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
+check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
+ = check_poly_type rank UT_NotOk arg_ty `thenM_`
+ check_tau_type rank UT_Ok res_ty
+
+check_tau_type rank ubx_tup (AppTy ty1 ty2)
+ = check_arg_type ty1 `thenM_` 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)
+ = doptM Opt_GlasgowExts `thenM` \ 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.
+ returnM ()
+ else
+ -- For H98, do check the un-expanded part
+ check_tau_type rank ubx_tup syn
+ ) `thenM_`
+
+ 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 `thenM_`
+ mappM_ check_arg_type tys
+
+ | isUnboxedTupleTyCon tc
+ = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
+ checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
+ mappM_ (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
+ = mappM_ check_arg_type tys