where
-- In 'loop', the parameter 'arg_tys' accumulates
-- the arg types so far, in *reverse order*
+ -- INVARIANT: res_ty :: *
loop n args_so_far res_ty
| Just res_ty' <- tcView res_ty = loop n args_so_far res_ty'
else loop n args_so_far (FunTy arg_ty' res_ty') }
loop n args_so_far (TyVarTy tv)
- | not (isImmutableTyVar tv)
+ | isTyConableTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> loop n args_so_far ty
return (args ++ args_so_far)
loop n_req args_so_far (AppTy fun arg)
+ | n_req > 0
= loop (n_req - 1) (arg:args_so_far) fun
loop n_req args_so_far (TyVarTy tv)
- | not (isImmutableTyVar tv)
+ | isTyConableTyVar tv
+ , res_kind `isSubKind` tyVarKind tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> loop n_req args_so_far ty
}
where
mk_res_ty arg_tys' = mkTyConApp tc arg_tys'
- arg_kinds = map tyVarKind (take n_req (tyConTyVars tc))
+ (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc)
loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty
----------------------
boxySplitAppTy :: BoxyRhoType -- Type to split: m a
-> TcM (BoxySigmaType, BoxySigmaType) -- Returns m, a
--- Assumes (m: * -> k), where k is the kind of the incoming type
+-- If the incoming type is a mutable type variable of kind k, then
+-- boxySplitAppTy returns a new type variable (m: * -> k); note the *.
-- If the incoming type is boxy, then so are the result types; and vice versa
boxySplitAppTy orig_ty
= return (fun_ty, arg_ty)
loop (TyVarTy tv)
- | not (isImmutableTyVar tv)
+ | isTyConableTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> loop ty
-----------------------------------
defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
= do { addSubCtxt sub_ctxt act_sty exp_sty $
- u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty
+ u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty
; return idHsWrapper }
+ where
+ outer = case sub_ctxt of -- Ugh
+ SubDone -> False
+ other -> True
-----------------------------------
tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
-- Get location from monad, not from tvs1
; let tys = mkTyVarTys tvs
in_scope = mkInScopeSet (mkVarSet tvs)
- subst1 = mkTvSubst in_scope (zipTyEnv tvs1 tys)
- subst2 = mkTvSubst in_scope (zipTyEnv tvs2 tys)
- (theta1,tau1) = tcSplitPhiTy (substTy subst1 body1)
- (theta2,tau2) = tcSplitPhiTy (substTy subst2 body2)
+ phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
+ phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
+ (theta1,tau1) = tcSplitPhiTy phi1
+ (theta2,tau2) = tcSplitPhiTy phi2
- ; checkM (equalLength theta1 theta2)
+ ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
+ { checkM (equalLength theta1 theta2)
(unifyMisMatch outer False orig_ty1 orig_ty2)
; uPreds False nb1 theta1 nb2 theta2
; uTys nb1 tau1 nb2 tau2
+ -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
+ ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
+ ; ifM (any (`elemVarSet` free_tvs) tvs)
+ (bleatEscapedTvs free_tvs tvs tvs)
+
-- If both sides are inside a box, we are in a "box-meets-box"
-- situation, and we should not have a polytype at all.
-- If we get here we have two boxes, already filled with
-- This check comes last, because the error message is
-- extremely unhelpful.
; ifM (nb1 && nb2) (notMonoType ty1)
- }
+ }}
where
(tvs1, body1) = tcSplitForAllTys ty1
(tvs2, body2) = tcSplitForAllTys ty2
; case mb_tys' of
Just tys' -> return (TyConApp tc tys')
-- Retain the synonym (the common case)
- Nothing -> go (expectJust "checkTauTvUpdate"
+ 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
}
<+> ptext SLIT("arguments")
------------------
+unifyForAllCtxt tvs phi1 phi2 env
+ = returnM (env2, msg)
+ where
+ (env', tvs') = tidyOpenTyVars env tvs -- NB: not tidyTyVarBndrs
+ (env1, phi1') = tidyOpenType env' phi1
+ (env2, phi2') = tidyOpenType env1 phi2
+ msg = vcat [ptext SLIT("When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')),
+ ptext SLIT(" and") <+> quotes (ppr (mkForAllTys tvs' phi2'))]
+
+------------------
unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
-- tv1 and ty2 are zonked already
= returnM msg
msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
; failWithTcM (env1, msg) }
+notMonoArgs ty
+ = do { ty' <- zonkTcType ty
+ ; env0 <- tcInitTidyEnv
+ ; let (env1, tidy_ty) = tidyOpenType env0 ty'
+ msg = ptext SLIT("Arguments of synonym family must be monotypes") <+> quotes (ppr tidy_ty)
+ ; failWithTcM (env1, msg) }
+
occurCheck tyvar ty
= do { env0 <- tcInitTidyEnv
; ty' <- zonkTcType ty
projects / ghc-hetmet.git / blobdiff