Commit bfe55fb7 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.

FIX: Make boxy splitters aware of type families

MERGE TO STABLE
parent a07a4634
......@@ -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}
......
......@@ -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
......
......@@ -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}
......
......@@ -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}
......@@ -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)
......
......@@ -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}
......@@ -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}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment