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
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}
%************************************************************************
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
; 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
-- 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