-- Various unifications
unifyType, unifyTypeList, unifyTheta,
unifyKind, unifyKinds, unifyFunKind,
- checkExpectedKind,
preSubType, boxyMatchTypes,
--------------------------------
go ty1 ty2 -- C.f. the isSigmaTy case for boxySubMatchType
| isSigmaTy ty1
- , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
- , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
+ , (tvs1, ps1, tau1) <- tcSplitSigmaTy ty1
+ , (tvs2, ps2, tau2) <- tcSplitSigmaTy ty2
, equalLength tvs1 tvs2
+ , equalLength ps1 ps2
= boxy_match (tmpl_tvs `delVarSetList` tvs1) tau1
(boxy_tvs `extendVarSetList` tvs2) tau2 subst
Nothing -> orig_boxy_ty
Just ty -> ty `boxyLub` orig_boxy_ty
- go _ (TyVarTy tv) | isMetaTyVar tv
+ go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv
+ -- NB: A TyVar (not TcTyVar) is possible here, representing
+ -- a skolem, because in this pure boxy_match function
+ -- we don't instantiate foralls to TcTyVars; cf Trac #2714
= subst -- Don't fail if the template has more info than the target!
-- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
-- would fail to instantiate 'a', because the meta-type-variable
unifyTypeList :: [TcTauType] -> TcM ()
unifyTypeList [] = return ()
unifyTypeList [_] = return ()
-unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
- ; unifyTypeList tys }
+unifyTypeList (ty1:tys@(ty2:_)) = do { _ <- unifyType ty1 ty2
+ ; unifyTypeList tys }
\end{code}
%************************************************************************
-> TcM CoercionI
-- We've just pushed a context describing ty1,ty2
uTysOuter nb1 ty1 nb2 ty2
- = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
+ = do { traceTc (text "uTysOuter" <+> sep [ppr ty1, ppr ty2])
; u_tys (Unify True ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 }
uTys :: InBox -> TcType -> InBox -> TcType -> TcM CoercionI
--------------
-uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types
+uTys_s :: Outer
+ -> InBox -> [TcType] -- tys1 are the *actual* types
-> InBox -> [TcType] -- tys2 are the *expected* types
-> TcM [CoercionI]
-uTys_s _ [] _ [] = return []
-uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
- ; cois <- uTys_s nb1 tys1 nb2 tys2
- ; return (coi:cois) }
-uTys_s _ _ _ _ = panic "Unify.uTys_s: mismatched type lists!"
+uTys_s outer nb1 tys1 nb2 tys2
+ = go tys1 tys2
+ where
+ go [] [] = return []
+ go (ty1:tys1) (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
+ ; cois <- go tys1 tys2
+ ; return (coi:cois) }
+ go _ _ = unifyMisMatch outer
+ -- See Note [Mismatched type lists and application decomposition]
--------------
u_tys :: Outer
; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
{ unless (equalLength theta1 theta2) (bale_out outer)
- ; _cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
- ; traceTc (text "TOMDO!")
+ ; cois <- uPreds outer nb1 theta1 nb2 theta2
; coi <- uTys nb1 tau1 nb2 tau2
-- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
-- This check comes last, because the error message is
-- extremely unhelpful.
; when (nb1 && nb2) (notMonoType ty1)
- ; return coi
+ ; let mk_fun (pred, coi_pred) (ty, coi)
+ = (mkFunTy pred_ty ty, mkFunTyCoI pred_ty coi_pred ty coi)
+ where
+ pred_ty = mkPredTy pred
+ ; return (foldr mkForAllTyCoI
+ (snd (foldr mk_fun (tau1,coi) (theta1 `zip` cois)))
+ tvs)
}}
where
(tvs1, body1) = tcSplitForAllTys ty1
= uPred outer nb1 p1 nb2 p2
-- Non-synonym type constructors must match
- go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
+ go outer _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
| con1 == con2 && not (isOpenSynTyCon con1)
- = do { cois <- uTys_s nb1 tys1 nb2 tys2
+ = do { traceTc (text "utys1" <+> ppr con1 <+> (ppr tys1 $$ ppr tys2))
+ ; cois <- uTys_s outer nb1 tys1 nb2 tys2
; return $ mkTyConAppCoI con1 tys1 cois
}
-- Family synonyms See Note [TyCon app]
| con1 == con2 && identicalOpenSynTyConApp
- = do { cois <- uTys_s nb1 tys1' nb2 tys2'
+ = do { traceTc (text "utys2" <+> ppr con1 <+> (ppr tys1' $$ ppr tys2'))
+ ; cois <- uTys_s outer nb1 tys1' nb2 tys2'
; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
}
where
identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
-- See Note [OpenSynTyCon app]
- -- If we can reduce a family app => proceed with reduct
- -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
- -- defer oversaturated applications!
- go outer sty1 ty1@(TyConApp con1 _) sty2 ty2
- | isOpenSynTyCon con1
- = do { (coi1, ty1') <- tcNormaliseFamInst ty1
- ; case coi1 of
- IdCo -> defer -- no reduction, see [Deferred Unification]
- _ -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2
- }
-
- -- If we can reduce a family app => proceed with reduct
- -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
- -- defer oversaturated applications!
- go outer sty1 ty1 sty2 ty2@(TyConApp con2 _)
- | isOpenSynTyCon con2
- = do { (coi2, ty2') <- tcNormaliseFamInst ty2
- ; case coi2 of
- IdCo -> defer -- no reduction, see [Deferred Unification]
- _ -> liftM (`mkTransCoI` mkSymCoI coi2) $
- go outer sty1 ty1 sty2 ty2'
- }
-
-- Functions; just check the two parts
go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
= do { coi_l <- uTys nb1 fun1 nb2 fun2
-- 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
+ -- See Note [Mismatched type lists and application decomposition]
go outer _ (AppTy s1 t1) _ ty2
| Just (s2,t2) <- tcSplitAppTy_maybe ty2
- = do { coi_s <- go outer s1 s1 s2 s2 -- NB recurse into go
+ = do { coi_s <- go outer s1 s1 s2 s2 -- NB recurse into go...
; coi_t <- uTys nb1 t1 nb2 t2 -- See Note [Unifying AppTy]
; return $ mkAppTyCoI s1 coi_s t1 coi_t }
; coi_t <- uTys nb1 t1 nb2 t2
; return $ mkAppTyCoI s1 coi_s t1 coi_t }
+ -- If we can reduce a family app => proceed with reduct
+ -- NB1: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+ -- defer oversaturated applications!
+ --
+ -- NB2: Do this *after* trying decomposing applications, so that decompose
+ -- (m a) ~ (F Int b)
+ -- where F has arity 1
+ go _ _ ty1@(TyConApp con1 _) _ ty2
+ | isOpenSynTyCon con1
+ = do { (coi1, ty1') <- tcNormaliseFamInst ty1
+ ; case coi1 of
+ IdCo -> defer -- no reduction, see [Deferred Unification]
+ _ -> liftM (coi1 `mkTransCoI`) $ uTys nb1 ty1' nb2 ty2
+ }
+
+ go _ _ ty1 _ ty2@(TyConApp con2 _)
+ | isOpenSynTyCon con2
+ = do { (coi2, ty2') <- tcNormaliseFamInst ty2
+ ; case coi2 of
+ IdCo -> defer -- no reduction, see [Deferred Unification]
+ _ -> liftM (`mkTransCoI` mkSymCoI coi2) $
+ uTys nb1 ty1 nb2 ty2'
+ }
+
-- Anything else fails
go outer _ _ _ _ = bale_out outer
----------
uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI
uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2)
- | n1 == n2 =
- do { coi <- uTys nb1 t1 nb2 t2
- ; return $ mkIParamPredCoI n1 coi
- }
-uPred _ nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
- | c1 == c2 =
- do { cois <- uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
- ; return $ mkClassPPredCoI c1 tys1 cois
- }
+ | n1 == n2
+ = do { coi <- uTys nb1 t1 nb2 t2
+ ; return $ mkIParamPredCoI n1 coi }
+uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
+ | c1 == c2
+ = do { traceTc (text "utys3" <+> ppr c1 <+> (ppr tys2 $$ ppr tys2))
+ ; cois <- uTys_s outer nb1 tys1 nb2 tys2
+ ; return $ mkClassPPredCoI c1 tys1 cois }
uPred outer _ _ _ _ = unifyMisMatch outer
uPreds :: Outer -> InBox -> [PredType] -> InBox -> [PredType]
uPreds _ _ _ _ _ = panic "uPreds"
\end{code}
-Note [TyCon app]
-~~~~~~~~~~~~~~~~
-When we find two TyConApps, the argument lists are guaranteed equal
-length. Reason: intially the kinds of the two types to be unified is
-the same. The only way it can become not the same is when unifying two
-AppTys (f1 a1)~(f2 a2). In that case there can't be a TyConApp in
-the f1,f2 (because it'd absorb the app). If we unify f1~f2 first,
-which we do, that ensures that f1,f2 have the same kind; and that
-means a1,a2 have the same kind. And now the argument repeats.
+Note [Mismatched type lists and application decomposition]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we find two TyConApps, you might think that the argument lists
+are guaranteed equal length. But they aren't. Consider matching
+ w (T x) ~ Foo (T x y)
+We do match (w ~ Foo) first, but in some circumstances we simply create
+a deferred constraint; and then go ahead and match (T x ~ T x y).
+This came up in Trac #3950.
+
+So either
+ (a) either we must check for identical argument kinds
+ when decomposing applications,
+
+ (b) or we must be prepared for ill-kinded unification sub-problems
+
+Currently we adopt (b) since it seems more robust -- no need to maintain
+a global invariant.
Note [OpenSynTyCon app]
~~~~~~~~~~~~~~~~~~~~~~~
-- with that type.
zapToMonotype res_ty
= do { res_tau <- newFlexiTyVarTy liftedTypeKind
- ; boxyUnify res_tau res_ty
+ ; _ <- boxyUnify res_tau res_ty
; return res_tau }
unBox :: BoxyType -> TcM TcType
%************************************************************************
%* *
- Checking kinds
-%* *
-%************************************************************************
-
----------------------------
--- We would like to get a decent error message from
--- (a) Under-applied type constructors
--- f :: (Maybe, Maybe)
--- (b) Over-applied type constructors
--- f :: Int x -> Int x
---
-
-\begin{code}
-checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
--- A fancy wrapper for 'unifyKind', which tries
--- to give decent error messages.
--- (checkExpectedKind ty act_kind exp_kind)
--- checks that the actual kind act_kind is compatible
--- with the expected kind exp_kind
--- The first argument, ty, is used only in the error message generation
-checkExpectedKind ty act_kind exp_kind
- | act_kind `isSubKind` exp_kind -- Short cut for a very common case
- = return ()
- | otherwise = do
- (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
- case mb_r of
- Just _ -> return () -- Unification succeeded
- Nothing -> do
-
- -- So there's definitely an error
- -- Now to find out what sort
- exp_kind <- zonkTcKind exp_kind
- act_kind <- zonkTcKind act_kind
-
- env0 <- tcInitTidyEnv
- let (exp_as, _) = splitKindFunTys exp_kind
- (act_as, _) = splitKindFunTys act_kind
- n_exp_as = length exp_as
- n_act_as = length act_as
-
- (env1, tidy_exp_kind) = tidyKind env0 exp_kind
- (env2, tidy_act_kind) = tidyKind env1 act_kind
-
- err | n_exp_as < n_act_as -- E.g. [Maybe]
- = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
-
- -- Now n_exp_as >= n_act_as. In the next two cases,
- -- n_exp_as == 0, and hence so is n_act_as
- | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
- = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
- <+> ptext (sLit "is unlifted")
-
- | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
- = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
- <+> ptext (sLit "is lifted")
-
- | otherwise -- E.g. Monad [Int]
- = ptext (sLit "Kind mis-match")
-
- more_info = sep [ ptext (sLit "Expected kind") <+>
- quotes (pprKind tidy_exp_kind) <> comma,
- ptext (sLit "but") <+> quotes (ppr ty) <+>
- ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
-
- failWithTcM (env2, err $$ more_info)
-\end{code}
-
-%************************************************************************
-%* *
\subsection{Checking signature type variables}
%* *
%************************************************************************