-checkTauTvUpdate orig_tv orig_ty
- = go orig_ty
- where
- go (TyConApp tc tys)
- | isSynTyCon tc = go_syn tc tys
- | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') }
- go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
- go (PredTy p) = do { p' <- go_pred p; return (PredTy p') }
- go (FunTy arg res) = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') }
- go (AppTy fun arg) = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') }
- -- NB the mkAppTy; we might have instantiated a
- -- type variable to a type constructor, so we need
- -- to pull the TyConApp to the top.
- go (ForAllTy tv ty) = notMonoType orig_ty -- (b)
-
- go (TyVarTy tv)
- | orig_tv == tv = occurCheck tv -- (a)
- | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv)
- | otherwise = return (TyVarTy tv)
- -- Ordinary (non Tc) tyvars
- -- occur inside quantified types
-
- go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') }
- go_pred (IParam n ty) = do { ty' <- go ty; return (IParam n ty') }
- go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') }
-
- go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
- go_tyvar tv (MetaTv box ref)
- = do { cts <- readMutVar ref
- ; case cts of
- Indirect ty -> go ty
- Flexi -> case box of
- BoxTv -> fillBoxWithTau tv ref
- other -> return (TyVarTy tv)
- }
-
- -- go_syn is called for synonyms only
- -- See Note [Type synonyms and the occur check]
- go_syn tc tys
- | not (isTauTyCon tc)
- = notMonoType orig_ty -- (b) again
- | otherwise
- = do { (msgs, mb_tys') <- tryTc (mapM go tys)
- ; case mb_tys' of
- Just tys' -> return (TyConApp tc tys')
- -- Retain the synonym (the common case)
- Nothing | isOpenTyCon tc
- -> notMonoArgs (TyConApp tc tys)
- -- Synonym families must have monotype args
- | otherwise
- -> go (expectJust "checkTauTvUpdate"
- (tcView (TyConApp tc tys)))
- -- Try again, expanding the synonym
- }
-
- occurCheck tv = occurCheckErr (mkTyVarTy tv) orig_ty
-
-fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
--- (fillBoxWithTau tv ref) fills ref with a freshly allocated
--- tau-type meta-variable, whose print-name is the same as tv
--- Choosing the same name is good: when we instantiate a function
--- we allocate boxy tyvars with the same print-name as the quantified
--- tyvar; and then we often fill the box with a tau-tyvar, and again
--- we want to choose the same name.
-fillBoxWithTau tv ref
- = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget
- ; let tau = mkTyVarTy tv' -- name of the type variable
- ; writeMutVar ref (Indirect tau)
- ; return tau }
-\end{code}
-
-Error mesages in case of kind mismatch.
-
-\begin{code}
-unifyKindMisMatch ty1 ty2
- = zonkTcKind ty1 `thenM` \ ty1' ->
- zonkTcKind ty2 `thenM` \ ty2' ->
- let
- msg = hang (ptext SLIT("Couldn't match kind"))
- 2 (sep [quotes (ppr ty1'),
- ptext SLIT("against"),
- quotes (ppr ty2')])
- in
- failWithTc msg
-
-unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
- -- tv1 and ty2 are zonked already
- = returnM msg
- where
- msg = (env2, ptext SLIT("When matching the kinds of") <+>
- sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
-
- (pp_expected, pp_actual) | swapped = (pp2, pp1)
- | otherwise = (pp1, pp2)
- (env1, tv1') = tidyOpenTyVar tidy_env tv1
- (env2, ty2') = tidyOpenType env1 ty2
- pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
- pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)