From: Manuel M T Chakravarty Date: Fri, 28 Sep 2007 22:55:41 +0000 (+0000) Subject: FIX: Make boxy splitters aware of type families X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=bfe55fb767d566b5105c5584f698af1dd4a57346 FIX: Make boxy splitters aware of type families MERGE TO STABLE --- diff --git a/compiler/hsSyn/HsPat.lhs b/compiler/hsSyn/HsPat.lhs index d4b0e1b..ddd6ec2 100644 --- a/compiler/hsSyn/HsPat.lhs +++ b/compiler/hsSyn/HsPat.lhs @@ -19,7 +19,7 @@ module HsPat ( HsConPatDetails, hsConPatArgs, HsRecFields(..), HsRecField(..), hsRecFields, - mkPrefixConPat, mkCharLitPat, mkNilPat, mkCoPat, + mkPrefixConPat, mkCharLitPat, mkNilPat, mkCoPat, mkCoPatCoI, isBangHsBind, patsAreAllCons, isConPat, isSigPat, isWildPat, @@ -37,6 +37,7 @@ import HsLit import HsTypes import BasicTypes -- others: +import Coercion import PprCore ( {- instance OutputableBndr TyVar -} ) import TysWiredIn import Var @@ -292,10 +293,14 @@ mkNilPat ty = mkPrefixConPat nilDataCon [] ty mkCharLitPat :: Char -> OutPat id mkCharLitPat c = mkPrefixConPat charDataCon [noLoc $ LitPat (HsCharPrim c)] charTy -mkCoPat :: HsWrapper -> OutPat id -> Type -> OutPat id -mkCoPat co lpat@(L loc pat) ty - | isIdHsWrapper co = lpat - | otherwise = L loc (CoPat co pat ty) +mkCoPat :: HsWrapper -> Pat id -> Type -> Pat id +mkCoPat co pat ty + | isIdHsWrapper co = pat + | otherwise = CoPat co pat ty + +mkCoPatCoI :: CoercionI -> Pat id -> Type -> Pat id +mkCoPatCoI IdCo pat ty = pat +mkCoPatCoI (ACo co) pat ty = mkCoPat (WpCo co) pat ty \end{code} diff --git a/compiler/hsSyn/HsUtils.lhs b/compiler/hsSyn/HsUtils.lhs index 3b9271a..0f75769 100644 --- a/compiler/hsSyn/HsUtils.lhs +++ b/compiler/hsSyn/HsUtils.lhs @@ -32,6 +32,7 @@ import HsLit import RdrName import Var +import Coercion import Type import DataCon import Name @@ -89,6 +90,10 @@ mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id mkHsWrap co_fn e | isIdHsWrapper co_fn = e | otherwise = HsWrap co_fn e +mkHsWrapCoI :: CoercionI -> HsExpr id -> HsExpr id +mkHsWrapCoI IdCo e = e +mkHsWrapCoI (ACo co) e = mkHsWrap (WpCo co) e + mkHsLam :: [LPat id] -> LHsExpr id -> LHsExpr id mkHsLam pats body = mkHsPar (L (getLoc body) (HsLam matches)) where diff --git a/compiler/typecheck/TcArrows.lhs b/compiler/typecheck/TcArrows.lhs index c575808..8276bc8 100644 --- a/compiler/typecheck/TcArrows.lhs +++ b/compiler/typecheck/TcArrows.lhs @@ -31,6 +31,7 @@ import TcGadt import TcPat import TcUnify import TcRnMonad +import Coercion import Inst import Name import TysWiredIn @@ -52,16 +53,18 @@ import Util \begin{code} tcProc :: InPat Name -> LHsCmdTop Name -- proc pat -> expr -> BoxyRhoType -- Expected type of whole proc expression - -> TcM (OutPat TcId, LHsCmdTop TcId) + -> TcM (OutPat TcId, LHsCmdTop TcId, CoercionI) tcProc pat cmd exp_ty = newArrowScope $ - do { (exp_ty1, res_ty) <- boxySplitAppTy exp_ty - ; (arr_ty, arg_ty) <- boxySplitAppTy exp_ty1 + do { ((exp_ty1, res_ty), coi) <- boxySplitAppTy exp_ty + ; ((arr_ty, arg_ty), coi1) <- boxySplitAppTy exp_ty1 ; let cmd_env = CmdEnv { cmd_arr = arr_ty } ; (pat', cmd') <- tcLamPat pat arg_ty (emptyRefinement, res_ty) $ tcCmdTop cmd_env cmd [] - ; return (pat', cmd') } + ; let res_coi = mkTransCoI coi (mkAppTyCoI exp_ty1 coi1 res_ty IdCo) + ; return (pat', cmd', res_coi) + } \end{code} diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index e03f65d..2c17568 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -133,7 +133,7 @@ tcExpr (HsVar name) res_ty = tcId (OccurrenceOf name) name res_ty tcExpr (HsLit lit) res_ty = do { let lit_ty = hsLitType lit ; coi <- boxyUnify lit_ty res_ty - ; return $ wrapExprCoI (HsLit lit) coi + ; return $ mkHsWrapCoI coi (HsLit lit) } tcExpr (HsPar expr) res_ty = do { expr' <- tcMonoExpr expr res_ty @@ -289,33 +289,21 @@ tcExpr (HsDo do_or_lc stmts body _) res_ty = tcDoStmts do_or_lc stmts body res_ty tcExpr in_expr@(ExplicitList _ exprs) res_ty -- Non-empty list - = do { elt_ty <- boxySplitListTy res_ty + = do { (elt_ty, coi) <- boxySplitListTy res_ty ; exprs' <- mappM (tc_elt elt_ty) exprs - ; return (ExplicitList elt_ty exprs') } + ; return $ mkHsWrapCoI coi (ExplicitList elt_ty exprs') } where tc_elt elt_ty expr = tcPolyExpr expr elt_ty -{- TODO: Version from Tom's original patch. Unfortunately, we cannot do it this - way, but need to teach boxy splitters about match deferral and coercions. - = do { elt_tv <- newBoxyTyVar argTypeKind - ; let elt_ty = TyVarTy elt_tv - ; coi <- boxyUnify (mkTyConApp listTyCon [elt_ty]) res_ty - -- ; elt_ty <- boxySplitListTy res_ty - ; exprs' <- mappM (tc_elt elt_ty) exprs - ; return $ wrapExprCoI (ExplicitList elt_ty exprs') coi } - -- ; return (ExplicitList elt_ty exprs') } - where - tc_elt elt_ty expr = tcPolyExpr expr elt_ty - -} tcExpr in_expr@(ExplicitPArr _ exprs) res_ty -- maybe empty - = do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty + = do { (elt_ty, coi) <- boxySplitPArrTy res_ty ; exprs' <- mappM (tc_elt elt_ty) exprs ; ifM (null exprs) (zapToMonotype elt_ty) -- If there are no expressions in the comprehension -- we must still fill in the box -- (Not needed for [] and () becuase they happen -- to parse as data constructors.) - ; return (ExplicitPArr elt_ty exprs') } + ; return $ mkHsWrapCoI coi (ExplicitPArr elt_ty exprs') } where tc_elt elt_ty expr = tcPolyExpr expr elt_ty @@ -335,8 +323,8 @@ tcExpr (ExplicitTuple exprs boxity) res_ty ; return (mkHsWrap co_fn (ExplicitTuple exprs' boxity)) } tcExpr (HsProc pat cmd) res_ty - = do { (pat', cmd') <- tcProc pat cmd res_ty - ; return (HsProc pat' cmd') } + = do { (pat', cmd', coi) <- tcProc pat cmd res_ty + ; return $ mkHsWrapCoI coi (HsProc pat' cmd') } tcExpr e@(HsArrApp _ _ _ _ _) _ = failWithTc (vcat [ptext SLIT("The arrow command"), nest 2 (ppr e), @@ -527,54 +515,58 @@ tcExpr expr@(RecordUpd record_expr rbinds _ _ _) res_ty \begin{code} tcExpr (ArithSeq _ seq@(From expr)) res_ty - = do { elt_ty <- boxySplitListTy res_ty + = do { (elt_ty, coi) <- boxySplitListTy res_ty ; expr' <- tcPolyExpr expr elt_ty ; enum_from <- newMethodFromName (ArithSeqOrigin seq) elt_ty enumFromName - ; return (ArithSeq (HsVar enum_from) (From expr')) } + ; return $ mkHsWrapCoI coi (ArithSeq (HsVar enum_from) (From expr')) } tcExpr in_expr@(ArithSeq _ seq@(FromThen expr1 expr2)) res_ty - = do { elt_ty <- boxySplitListTy res_ty + = do { (elt_ty, coi) <- boxySplitListTy res_ty ; expr1' <- tcPolyExpr expr1 elt_ty ; expr2' <- tcPolyExpr expr2 elt_ty ; enum_from_then <- newMethodFromName (ArithSeqOrigin seq) elt_ty enumFromThenName - ; return (ArithSeq (HsVar enum_from_then) (FromThen expr1' expr2')) } - + ; return $ mkHsWrapCoI coi + (ArithSeq (HsVar enum_from_then) (FromThen expr1' expr2')) } tcExpr in_expr@(ArithSeq _ seq@(FromTo expr1 expr2)) res_ty - = do { elt_ty <- boxySplitListTy res_ty + = do { (elt_ty, coi) <- boxySplitListTy res_ty ; expr1' <- tcPolyExpr expr1 elt_ty ; expr2' <- tcPolyExpr expr2 elt_ty ; enum_from_to <- newMethodFromName (ArithSeqOrigin seq) elt_ty enumFromToName - ; return (ArithSeq (HsVar enum_from_to) (FromTo expr1' expr2')) } + ; return $ mkHsWrapCoI coi + (ArithSeq (HsVar enum_from_to) (FromTo expr1' expr2')) } tcExpr in_expr@(ArithSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty - = do { elt_ty <- boxySplitListTy res_ty + = do { (elt_ty, coi) <- boxySplitListTy res_ty ; expr1' <- tcPolyExpr expr1 elt_ty ; expr2' <- tcPolyExpr expr2 elt_ty ; expr3' <- tcPolyExpr expr3 elt_ty ; eft <- newMethodFromName (ArithSeqOrigin seq) elt_ty enumFromThenToName - ; return (ArithSeq (HsVar eft) (FromThenTo expr1' expr2' expr3')) } + ; return $ mkHsWrapCoI coi + (ArithSeq (HsVar eft) (FromThenTo expr1' expr2' expr3')) } tcExpr in_expr@(PArrSeq _ seq@(FromTo expr1 expr2)) res_ty - = do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty + = do { (elt_ty, coi) <- boxySplitPArrTy res_ty ; expr1' <- tcPolyExpr expr1 elt_ty ; expr2' <- tcPolyExpr expr2 elt_ty ; enum_from_to <- newMethodFromName (PArrSeqOrigin seq) elt_ty enumFromToPName - ; return (PArrSeq (HsVar enum_from_to) (FromTo expr1' expr2')) } + ; return $ mkHsWrapCoI coi + (PArrSeq (HsVar enum_from_to) (FromTo expr1' expr2')) } tcExpr in_expr@(PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty - = do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty + = do { (elt_ty, coi) <- boxySplitPArrTy res_ty ; expr1' <- tcPolyExpr expr1 elt_ty ; expr2' <- tcPolyExpr expr2 elt_ty ; expr3' <- tcPolyExpr expr3 elt_ty ; eft <- newMethodFromName (PArrSeqOrigin seq) elt_ty enumFromThenToPName - ; return (PArrSeq (HsVar eft) (FromThenTo expr1' expr2' expr3')) } + ; return $ mkHsWrapCoI coi + (PArrSeq (HsVar eft) (FromThenTo expr1' expr2' expr3')) } tcExpr (PArrSeq _ _) _ = panic "TcExpr.tcMonoExpr: Infinite parallel array!" @@ -1214,9 +1206,3 @@ polySpliceErr id = ptext SLIT("Can't splice the polymorphic local variable") <+> quotes (ppr id) #endif \end{code} - -\begin{code} -wrapExprCoI :: HsExpr a -> CoercionI -> HsExpr a -wrapExprCoI expr IdCo = expr -wrapExprCoI expr (ACo co) = mkHsWrap (WpCo co) expr -\end{code} diff --git a/compiler/typecheck/TcMatches.lhs b/compiler/typecheck/TcMatches.lhs index 54f8756..3569038 100644 --- a/compiler/typecheck/TcMatches.lhs +++ b/compiler/typecheck/TcMatches.lhs @@ -222,29 +222,31 @@ tcDoStmts :: HsStmtContext Name -> BoxyRhoType -> TcM (HsExpr TcId) -- Returns a HsDo tcDoStmts ListComp stmts body res_ty - = do { elt_ty <- boxySplitListTy res_ty + = do { (elt_ty, coi) <- boxySplitListTy res_ty ; (stmts', body') <- tcStmts ListComp (tcLcStmt listTyCon) stmts (emptyRefinement,elt_ty) $ tcBody body - ; return (HsDo ListComp stmts' body' (mkListTy elt_ty)) } + ; return $ mkHsWrapCoI coi + (HsDo ListComp stmts' body' (mkListTy elt_ty)) } tcDoStmts PArrComp stmts body res_ty - = do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty + = do { (elt_ty, coi) <- boxySplitPArrTy res_ty ; (stmts', body') <- tcStmts PArrComp (tcLcStmt parrTyCon) stmts (emptyRefinement, elt_ty) $ tcBody body - ; return (HsDo PArrComp stmts' body' (mkPArrTy elt_ty)) } + ; return $ mkHsWrapCoI coi + (HsDo PArrComp stmts' body' (mkPArrTy elt_ty)) } tcDoStmts DoExpr stmts body res_ty - = do { (m_ty, elt_ty) <- boxySplitAppTy res_ty + = do { ((m_ty, elt_ty), coi) <- boxySplitAppTy res_ty ; let res_ty' = mkAppTy m_ty elt_ty -- The boxySplit consumes res_ty ; (stmts', body') <- tcStmts DoExpr (tcDoStmt m_ty) stmts (emptyRefinement, res_ty') $ tcBody body - ; return (HsDo DoExpr stmts' body' res_ty') } + ; return $ mkHsWrapCoI coi (HsDo DoExpr stmts' body' res_ty') } tcDoStmts ctxt@(MDoExpr _) stmts body res_ty - = do { (m_ty, elt_ty) <- boxySplitAppTy res_ty + = do { ((m_ty, elt_ty), coi) <- boxySplitAppTy res_ty ; let res_ty' = mkAppTy m_ty elt_ty -- The boxySplit consumes res_ty tc_rhs rhs = withBox liftedTypeKind $ \ pat_ty -> tcMonoExpr rhs (mkAppTy m_ty pat_ty) @@ -255,7 +257,9 @@ tcDoStmts ctxt@(MDoExpr _) stmts body res_ty ; let names = [mfixName, bindMName, thenMName, returnMName, failMName] ; insts <- mapM (newMethodFromName DoOrigin m_ty) names - ; return (HsDo (MDoExpr (names `zip` insts)) stmts' body' res_ty') } + ; return $ + mkHsWrapCoI coi + (HsDo (MDoExpr (names `zip` insts)) stmts' body' res_ty') } tcDoStmts ctxt stmts body res_ty = pprPanic "tcDoStmts" (pprStmtContext ctxt) diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 0640675..f009db5 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -408,20 +408,21 @@ tc_pat pstate pat@(TypePat ty) pat_ty thing_inside ------------------------ -- Lists, tuples, arrays tc_pat pstate (ListPat pats _) pat_ty thing_inside - = do { elt_ty <- boxySplitListTy pat_ty + = do { (elt_ty, coi) <- boxySplitListTy pat_ty ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty) pats pstate thing_inside - ; return (ListPat pats' elt_ty, pats_tvs, res) } + ; return (mkCoPatCoI coi (ListPat pats' elt_ty) pat_ty, pats_tvs, res) } tc_pat pstate (PArrPat pats _) pat_ty thing_inside - = do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty + = do { (elt_ty, coi) <- boxySplitPArrTy pat_ty ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty) pats pstate thing_inside - ; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr - ; return (PArrPat pats' elt_ty, pats_tvs, res) } + ; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr + ; return (mkCoPatCoI coi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res) } tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside - = do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty + = do { let tc = tupleTyCon boxity (length pats) + ; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys) pstate thing_inside @@ -429,13 +430,17 @@ tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside -- so that we can experiment with lazy tuple-matching. -- This is a pretty odd place to make the switch, but -- it was easy to do. - ; let unmangled_result = TuplePat pats' boxity pat_ty + ; let pat_ty' = mkTyConApp tc arg_tys + -- pat_ty /= pat_ty iff coi /= IdCo + unmangled_result = TuplePat pats' boxity pat_ty' possibly_mangled_result - | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result) - | otherwise = unmangled_result + | opt_IrrefutableTuples && + isBoxed boxity = LazyPat (noLoc unmangled_result) + | otherwise = unmangled_result - ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced - return (possibly_mangled_result, pats_tvs, res) } + ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced + return (mkCoPatCoI coi possibly_mangled_result pat_ty, pats_tvs, res) + } ------------------------ -- Data constructors @@ -455,7 +460,8 @@ tc_pat pstate (LitPat simple_lit) pat_ty thing_inside -- pattern coercions have to -- be of kind: pat_ty ~ lit_ty -- hence, sym coi - ; returnM (wrapPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, [], res) } + ; returnM (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, + [], res) } ------------------------ -- Overloaded patterns: n, and n+k @@ -571,7 +577,7 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside origin = SigOrigin skol_info -- Instantiate the constructor type variables [a->ty] - ; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty + ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs -- Get location from monad, -- not from ex_tvs ; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs) @@ -593,13 +599,16 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside ; addDataConStupidTheta data_con ctxt_res_tys - ; return - (unwrapFamInstScrutinee tycon ctxt_res_tys $ - ConPatOut { pat_con = L con_span data_con, - pat_tvs = ex_tvs' ++ co_vars, - pat_dicts = map instToVar dicts, - pat_binds = dict_binds, - pat_args = arg_pats', pat_ty = pat_ty }, + ; let pat_ty' = mkTyConApp tycon ctxt_res_tys + -- pat_ty /= pat_ty iff coi /= IdCo + res_pat = ConPatOut { pat_con = L con_span data_con, + pat_tvs = ex_tvs' ++ co_vars, + pat_dicts = map instToVar dicts, + pat_binds = dict_binds, + pat_args = arg_pats', pat_ty = pat_ty' } + ; return + (mkCoPatCoI coi + (unwrapFamInstScrutinee tycon ctxt_res_tys res_pat) pat_ty, ex_tvs' ++ inner_tvs, res) } where @@ -610,10 +619,10 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside case tyConFamInst_maybe tycon of Nothing -> boxySplitTyConApp tycon pat_ty Just (fam_tycon, instTys) -> - do { scrutinee_arg_tys <- boxySplitTyConApp fam_tycon pat_ty + do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon) ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys - ; return freshTvs + ; return (freshTvs, coi) } where traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+> @@ -992,9 +1001,3 @@ nonRigidResult res_ty inaccessibleAlt msg = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg \end{code} - -\begin{code} -wrapPatCoI :: CoercionI -> Pat a -> TcType -> Pat a -wrapPatCoI IdCo pat ty = pat -wrapPatCoI (ACo co) pat ty = CoPat (WpCo co) pat ty -\end{code} diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 233e87d..67cdf20 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -28,7 +28,7 @@ module TcUnify ( -- Holes tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, boxyUnify, boxyUnifyList, zapToMonotype, - boxySplitListTy, boxySplitTyConApp, boxySplitAppTy, + boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy, wrapFunResCoercion ) where @@ -191,8 +191,9 @@ subFunTys error_herald n_pats res_ty thing_inside ---------------------- boxySplitTyConApp :: TyCon -- T :: k1 -> ... -> kn -> * -> BoxyRhoType -- Expected type (T a b c) - -> TcM [BoxySigmaType] -- Element types, a b c - -- It's used for wired-in tycons, so we call checkWiredInTyCOn + -> TcM ([BoxySigmaType], -- Element types, a b c + CoercionI) + -- It's used for wired-in tycons, so we call checkWiredInTyCon -- Precondition: never called with FunTyCon -- Precondition: input type :: * @@ -203,14 +204,26 @@ boxySplitTyConApp tc orig_ty loop n_req args_so_far ty | Just ty' <- tcView ty = loop n_req args_so_far ty' - loop n_req args_so_far (TyConApp tycon args) + loop n_req args_so_far ty@(TyConApp tycon args) | tc == tycon = ASSERT( n_req == length args) -- ty::* - return (args ++ args_so_far) + return (args ++ args_so_far, IdCo) + + | isOpenSynTyCon tycon -- try to normalise type family application + = do { (coi1, ty') <- tcNormaliseFamInst ty + ; case coi1 of + IdCo -> defer -- no progress, but maybe solvable => defer + ACo _ -> -- progress: so lets try again + do { (args, coi2) <- loop n_req args_so_far ty' + ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1) + } + } loop n_req args_so_far (AppTy fun arg) | n_req > 0 - = loop (n_req - 1) (arg:args_so_far) fun + = do { (args, coi) <- loop (n_req - 1) (arg:args_so_far) fun + ; return (args, mkAppTyCoI fun coi arg IdCo) + } loop n_req args_so_far (TyVarTy tv) | isTyConableTyVar tv @@ -219,23 +232,42 @@ boxySplitTyConApp tc orig_ty ; case cts of Indirect ty -> loop n_req args_so_far ty Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty - ; return (arg_tys ++ args_so_far) } - } + ; return (arg_tys ++ args_so_far, IdCo) } + } + | otherwise -- defer as tyvar may be refined by equalities + = defer where - mk_res_ty arg_tys' = mkTyConApp tc arg_tys' (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc) - loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty + loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) + orig_ty + + -- defer splitting by generating an equality constraint + defer = boxySplitDefer arg_kinds mk_res_ty orig_ty + where + (arg_kinds, _) = splitKindFunTys (tyConKind tc) + + -- apply splitted tycon to arguments + mk_res_ty = mkTyConApp tc ---------------------- -boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType -- Special case for lists -boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty - ; return elt_ty } +boxySplitListTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI) +-- Special case for lists +boxySplitListTy exp_ty + = do { ([elt_ty], coi) <- boxySplitTyConApp listTyCon exp_ty + ; return (elt_ty, coi) } +---------------------- +boxySplitPArrTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI) +-- Special case for parrs +boxySplitPArrTy exp_ty + = do { ([elt_ty], coi) <- boxySplitTyConApp parrTyCon exp_ty + ; return (elt_ty, coi) } ---------------------- boxySplitAppTy :: BoxyRhoType -- Type to split: m a - -> TcM (BoxySigmaType, BoxySigmaType) -- Returns m, a + -> TcM ((BoxySigmaType, BoxySigmaType), -- Returns m, a + CoercionI) -- 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 @@ -248,18 +280,29 @@ boxySplitAppTy orig_ty loop ty | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty - = return (fun_ty, arg_ty) + = return ((fun_ty, arg_ty), IdCo) + + loop ty@(TyConApp tycon args) + | isOpenSynTyCon tycon -- try to normalise type family application + = do { (coi1, ty') <- tcNormaliseFamInst ty + ; case coi1 of + IdCo -> defer -- no progress, but maybe solvable => defer + ACo co -> -- progress: so lets try again + do { (args, coi2) <- loop ty' + ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1) + } + } loop (TyVarTy tv) | isTyConableTyVar tv = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> loop ty - Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty - ; return (fun_ty, arg_ty) } } + Flexi -> do { [fun_ty, arg_ty] <- withMetaTvs tv kinds mk_res_ty + ; return ((fun_ty, arg_ty), IdCo) } } + | otherwise -- defer as tyvar may be refined by equalities + = defer where - mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty' - mk_res_ty other = panic "TcUnify.mk_res_ty2" tv_kind = tyVarKind tv kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind), -- m :: * -> k @@ -271,11 +314,36 @@ boxySplitAppTy orig_ty loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty + -- defer splitting by generating an equality constraint + defer = do { ([ty1, ty2], coi) <- boxySplitDefer arg_kinds mk_res_ty orig_ty + ; return ((ty1, ty2), coi) + } + where + orig_kind = typeKind orig_ty + arg_kinds = [mkArrowKind liftedTypeKind (defaultKind orig_kind), + -- m :: * -> k + liftedTypeKind] -- arg type :: * + + -- build type application + mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty' + mk_res_ty _other = panic "TcUnify.mk_res_ty2" + ------------------ boxySplitFailure actual_ty expected_ty = unifyMisMatch False False actual_ty expected_ty -- "outer" is False, so we don't pop the context -- which is what we want since we have not pushed one! + +------------------ +boxySplitDefer :: [Kind] -- kinds of required arguments + -> ([TcType] -> TcTauType) -- construct lhs from argument tyvars + -> BoxyRhoType -- type to split + -> TcM ([TcType], CoercionI) +boxySplitDefer kinds mkTy orig_ty + = do { tau_tys <- mapM newFlexiTyVarTy kinds + ; coi <- defer_unification False False (mkTy tau_tys) orig_ty + ; return (tau_tys, coi) + } \end{code}