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
= loop (n_req - 1) (arg:args_so_far) fun
loop n_req args_so_far (TyVarTy tv)
- | not (isImmutableTyVar tv)
+ | isTyConableTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> loop n_req args_so_far 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