X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcUnify.lhs;h=04a804d0ae197787f3b012ebe70b1fa13406c047;hb=bfc3c306e8ed18f3d5ccebda94a38e89316f5b00;hp=fd2255758e58c82c0b42f96fd8561803b4431951;hpb=9f24a6953e29dbee1b299099553fc4dd34029a39;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index fd22557..04a804d 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -6,18 +6,21 @@ \begin{code} module TcUnify ( -- Full-blown subsumption - tcSubOff, tcSubExp, tcGen, subFunTy, TcHoleType, + tcSubOff, tcSubExp, tcGen, checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals, -- Various unifications unifyTauTy, unifyTauTyList, unifyTauTyLists, - unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy, - unifyKind, unifyKinds, unifyOpenTypeKind, unifyFunKind, + unifyKind, unifyKinds, unifyFunKind, - -- Coercions - Coercion, ExprCoFn, PatCoFn, - (<$>), (<.>), mkCoercion, - idCoercion, isIdCoercion + -------------------------------- + -- Holes + Expected(..), newHole, readExpectedType, + zapExpectedType, zapExpectedTo, zapExpectedBranches, + subFunTys, unifyFunTy, + zapToListTy, unifyListTy, + zapToPArrTy, unifyPArrTy, + zapToTupleTy, unifyTupleTy ) where @@ -25,41 +28,38 @@ module TcUnify ( import HsSyn ( HsExpr(..) ) -import TcHsSyn ( TypecheckedHsExpr, TcPat, mkHsLet ) -import TypeRep ( Type(..), SourceType(..), TyNote(..), openKindCon ) +import TcHsSyn ( mkHsLet, + ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) ) +import TypeRep ( Type(..), PredType(..), TyNote(..), typeCon, openKindCon, isSuperKind ) import TcRnMonad -- TcType, amongst others import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType, TcTyVarSet, TcThetaType, TyVarDetails(SigTv), - isTauTy, isSigmaTy, + isTauTy, isSigmaTy, mkFunTys, mkTyConApp, tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcGetTyVar_maybe, tcGetTyVar, - mkTyConApp, mkFunTy, tyVarsOfType, mkPhiTy, + mkFunTy, tyVarsOfType, mkPhiTy, typeKind, tcSplitFunTy_maybe, mkForAllTys, - isHoleTyVar, isSkolemTyVar, isUserTyVar, + isSkolemTyVar, isUserTyVar, tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, eqKind, openTypeKind, liftedTypeKind, isTypeKind, mkArrowKind, - hasMoreBoxityInfo, allDistinctTyVars - ) -import qualified Type ( getTyVar_maybe ) + hasMoreBoxityInfo, allDistinctTyVars, pprType, pprKind ) import Inst ( newDicts, instToId, tcInstCall ) -import TcMType ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult, newKindVar, - newTyVarTy, newTyVarTys, newOpenTypeKind, newHoleTyVarTy, - zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar ) +import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newKindVar, + newTyVarTy, newTyVarTys, newOpenTypeKind, + zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV ) import TcSimplify ( tcSimplifyCheck ) -import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy ) -import TcEnv ( TcTyThing(..), tcGetGlobalTyVars, findGlobals ) -import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity ) -import PprType ( pprType ) -import Id ( Id, mkSysLocal, idType ) +import TysWiredIn ( listTyCon, parrTyCon, tupleTyCon ) +import TcEnv ( tcGetGlobalTyVars, findGlobals ) +import TyCon ( TyCon, tyConArity, isTupleTyCon, tupleTyConBoxity ) +import Id ( Id, mkSysLocal ) import Var ( Var, varName, tyVarKind ) import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems ) import VarEnv -import Name ( isSystemName, getSrcLoc ) +import Name ( isSystemName ) import ErrUtils ( Message ) import BasicTypes ( Boxity, Arity, isBoxed ) -import Util ( equalLength, notNull ) -import Maybe ( isNothing ) +import Util ( equalLength, lengthExceeds, notNull ) import Outputable \end{code} @@ -69,6 +69,198 @@ Notes on holes %************************************************************************ %* * +\subsection{'hole' type variables} +%* * +%************************************************************************ + +\begin{code} +data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference + | Check ty -- The type to check during type checking + +newHole :: TcM (TcRef ty) +newHole = newMutVar (error "Empty hole in typechecker") + +readExpectedType :: Expected ty -> TcM ty +readExpectedType (Infer hole) = readMutVar hole +readExpectedType (Check ty) = returnM ty + +zapExpectedType :: Expected TcType -> TcM TcTauType +-- In the inference case, ensure we have a monotype +zapExpectedType (Infer hole) + = do { ty <- newTyVarTy openTypeKind ; + writeMutVar hole ty ; + return ty } + +zapExpectedType (Check ty) = return ty + +zapExpectedTo :: Expected TcType -> TcTauType -> TcM () +zapExpectedTo (Infer hole) ty2 = writeMutVar hole ty2 +zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2 + +zapExpectedBranches :: [a] -> Expected TcType -> TcM (Expected TcType) +-- Zap the expected type to a monotype if there is more than one branch +zapExpectedBranches branches exp_ty + | lengthExceeds branches 1 = zapExpectedType exp_ty `thenM` \ exp_ty' -> + return (Check exp_ty') + | otherwise = returnM exp_ty + +instance Outputable ty => Outputable (Expected ty) where + ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty + ppr (Infer hole) = ptext SLIT("Inferring type") +\end{code} + + +%************************************************************************ +%* * +\subsection[Unify-fun]{@unifyFunTy@} +%* * +%************************************************************************ + +@subFunTy@ and @unifyFunTy@ is used to avoid the fruitless +creation of type variables. + +* subFunTy is used when we might be faced with a "hole" type variable, + in which case we should create two new holes. + +* unifyFunTy is used when we expect to encounter only "ordinary" + type variables, so we should create new ordinary type variables + +\begin{code} +subFunTys :: [pat] + -> Expected TcRhoType -- Fail if ty isn't a function type + -> ([(pat, Expected TcRhoType)] -> Expected TcRhoType -> TcM a) + -> TcM a + +subFunTys pats (Infer hole) thing_inside + = -- This is the interesting case + mapM new_pat_hole pats `thenM` \ pats_w_holes -> + newHole `thenM` \ res_hole -> + + -- Do the business + thing_inside pats_w_holes (Infer res_hole) `thenM` \ answer -> + + -- Extract the answers + mapM read_pat_hole pats_w_holes `thenM` \ arg_tys -> + readMutVar res_hole `thenM` \ res_ty -> + + -- Write the answer into the incoming hole + writeMutVar hole (mkFunTys arg_tys res_ty) `thenM_` + + -- And return the answer + returnM answer + where + new_pat_hole pat = newHole `thenM` \ hole -> return (pat, Infer hole) + read_pat_hole (pat, Infer hole) = readMutVar hole + +subFunTys pats (Check ty) thing_inside + = go pats ty `thenM` \ (pats_w_tys, res_ty) -> + thing_inside pats_w_tys res_ty + where + go [] ty = return ([], Check ty) + go (pat:pats) ty = unifyFunTy ty `thenM` \ (arg,res) -> + go pats res `thenM` \ (pats_w_tys, final_res) -> + return ((pat, Check arg) : pats_w_tys, final_res) + +unifyFunTy :: TcRhoType -- Fail if ty isn't a function type + -> TcM (TcType, TcType) -- otherwise return arg and result types + +unifyFunTy ty@(TyVarTy tyvar) + = getTcTyVar tyvar `thenM` \ maybe_ty -> + case maybe_ty of + Just ty' -> unifyFunTy ty' + Nothing -> unify_fun_ty_help ty + +unifyFunTy ty + = case tcSplitFunTy_maybe ty of + Just arg_and_res -> returnM arg_and_res + Nothing -> unify_fun_ty_help ty + +unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification + = newTyVarTy openTypeKind `thenM` \ arg -> + newTyVarTy openTypeKind `thenM` \ res -> + unifyTauTy ty (mkFunTy arg res) `thenM_` + returnM (arg,res) +\end{code} + +\begin{code} +---------------------- +zapToListTy, zapToPArrTy :: Expected TcType -- expected list type + -> TcM TcType -- list element type +unifyListTy, unifyPArrTy :: TcType -> TcM TcType +zapToListTy = zapToXTy listTyCon +unifyListTy = unifyXTy listTyCon +zapToPArrTy = zapToXTy parrTyCon +unifyPArrTy = unifyXTy parrTyCon + +---------------------- +zapToXTy :: TyCon -- T :: *->* + -> Expected TcType -- Expected type (T a) + -> TcM TcType -- Element type, a + +zapToXTy tc (Check ty) = unifyXTy tc ty +zapToXTy tc (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ; + writeMutVar hole (mkTyConApp tc [elt_ty]) ; + return elt_ty } + +---------------------- +unifyXTy :: TyCon -> TcType -> TcM TcType +unifyXTy tc ty@(TyVarTy tyvar) + = getTcTyVar tyvar `thenM` \ maybe_ty -> + case maybe_ty of + Just ty' -> unifyXTy tc ty' + other -> unify_x_ty_help tc ty + +unifyXTy tc ty + = case tcSplitTyConApp_maybe ty of + Just (tycon, [arg_ty]) | tycon == tc -> returnM arg_ty + other -> unify_x_ty_help tc ty + +unify_x_ty_help tc ty -- Revert to ordinary unification + = newTyVarTy liftedTypeKind `thenM` \ elt_ty -> + unifyTauTy ty (mkTyConApp tc [elt_ty]) `thenM_` + returnM elt_ty +\end{code} + +\begin{code} +---------------------- +zapToTupleTy :: Boxity -> Arity -> Expected TcType -> TcM [TcType] +zapToTupleTy boxity arity (Check ty) = unifyTupleTy boxity arity ty +zapToTupleTy boxity arity (Infer hole) = do { (tup_ty, arg_tys) <- new_tuple_ty boxity arity ; + writeMutVar hole tup_ty ; + return arg_tys } + +unifyTupleTy boxity arity ty@(TyVarTy tyvar) + = getTcTyVar tyvar `thenM` \ maybe_ty -> + case maybe_ty of + Just ty' -> unifyTupleTy boxity arity ty' + other -> unify_tuple_ty_help boxity arity ty + +unifyTupleTy boxity arity ty + = case tcSplitTyConApp_maybe ty of + Just (tycon, arg_tys) + | isTupleTyCon tycon + && tyConArity tycon == arity + && tupleTyConBoxity tycon == boxity + -> returnM arg_tys + other -> unify_tuple_ty_help boxity arity ty + +unify_tuple_ty_help boxity arity ty + = new_tuple_ty boxity arity `thenM` \ (tup_ty, arg_tys) -> + unifyTauTy ty tup_ty `thenM_` + returnM arg_tys + +new_tuple_ty boxity arity + = newTyVarTys arity kind `thenM` \ arg_tys -> + return (mkTyConApp tup_tc arg_tys, arg_tys) + where + tup_tc = tupleTyCon boxity arity + kind | isBoxed boxity = liftedTypeKind + | otherwise = openTypeKind +\end{code} + + +%************************************************************************ +%* * \subsection{Subsumption} %* * %************************************************************************ @@ -88,19 +280,16 @@ which takes an HsExpr of type offered_ty into one of type expected_ty. \begin{code} -type TcHoleType = TcSigmaType -- Either a TcSigmaType, - -- or else a hole - -tcSubExp :: TcHoleType -> TcSigmaType -> TcM ExprCoFn -tcSubOff :: TcSigmaType -> TcHoleType -> TcM ExprCoFn -tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn +tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn +tcSubOff :: TcSigmaType -> Expected TcSigmaType -> TcM ExprCoFn \end{code} These two check for holes \begin{code} tcSubExp expected_ty offered_ty - = checkHole expected_ty offered_ty tcSub + = traceTc (text "tcSubExp" <+> (ppr expected_ty $$ ppr offered_ty)) `thenM_` + checkHole expected_ty offered_ty tcSub tcSubOff expected_ty offered_ty = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off) @@ -111,25 +300,21 @@ tcSubOff expected_ty offered_ty -- Otherwise it calls thing_inside, passing the two args, looking -- through any instantiated hole -checkHole (TyVarTy tv) other_ty thing_inside - | isHoleTyVar tv - = getTcTyVar tv `thenM` \ maybe_ty -> - case maybe_ty of - Just ty -> thing_inside ty other_ty - Nothing -> putTcTyVar tv other_ty `thenM_` - returnM idCoercion +checkHole (Infer hole) other_ty thing_inside + = do { writeMutVar hole other_ty; return idCoercion } -checkHole ty other_ty thing_inside +checkHole (Check ty) other_ty thing_inside = thing_inside ty other_ty \end{code} No holes expected now. Add some error-check context info. \begin{code} +tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only tcSub expected_ty actual_ty = traceTc (text "tcSub" <+> details) `thenM_` addErrCtxtM (unifyCtxt "type" expected_ty actual_ty) - (tc_sub expected_ty expected_ty actual_ty actual_ty) + (tc_sub expected_ty expected_ty actual_ty actual_ty) where details = vcat [text "Expected:" <+> ppr expected_ty, text "Actual: " <+> ppr actual_ty] @@ -179,7 +364,7 @@ tc_sub exp_sty expected_ty act_sty actual_ty | isSigmaTy actual_ty = tcInstCall Rank2Origin actual_ty `thenM` \ (inst_fn, body_ty) -> tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn -> - returnM (co_fn <.> mkCoercion inst_fn) + returnM (co_fn <.> inst_fn) ----------------------------------- -- Function case @@ -199,19 +384,29 @@ tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res) -- when the arg/res is not a tau-type? -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int -- then x = (f,f) --- is perfectly fine! +-- is perfectly fine, because we can instantiat f's type to a monotype +-- +-- However, we get can get jolly unhelpful error messages. +-- e.g. foo = id runST +-- +-- Inferred type is less polymorphic than expected +-- Quantified type variable `s' escapes +-- Expected type: ST s a -> t +-- Inferred type: (forall s1. ST s1 a) -> a +-- In the first argument of `id', namely `runST' +-- In a right-hand side of function `foo': id runST +-- +-- I'm not quite sure what to do about this! tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv) - = ASSERT( not (isHoleTyVar tv) ) - getTcTyVar tv `thenM` \ maybe_ty -> + = getTcTyVar tv `thenM` \ maybe_ty -> case maybe_ty of Just ty -> tc_sub exp_sty exp_ty ty ty Nothing -> imitateFun tv exp_sty `thenM` \ (act_arg, act_res) -> tcSub_fun exp_arg exp_res act_arg act_res tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res) - = ASSERT( not (isHoleTyVar tv) ) - getTcTyVar tv `thenM` \ maybe_ty -> + = getTcTyVar tv `thenM` \ maybe_ty -> case maybe_ty of Just ty -> tc_sub ty ty act_sty act_ty Nothing -> imitateFun tv act_sty `thenM` \ (exp_arg, exp_res) -> @@ -257,8 +452,7 @@ tcSub_fun exp_arg exp_res act_arg act_res imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType) imitateFun tv ty - = ASSERT( not (isHoleTyVar tv) ) - -- NB: tv is an *ordinary* tyvar and so are the new ones + = -- NB: tv is an *ordinary* tyvar and so are the new ones -- Check that tv isn't a type-signature type variable -- (This would be found later in checkSigTyVars, but @@ -339,39 +533,6 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall %************************************************************************ %* * -\subsection{Coercion functions} -%* * -%************************************************************************ - -\begin{code} -type Coercion a = Maybe (a -> a) - -- Nothing => identity fn - -type ExprCoFn = Coercion TypecheckedHsExpr -type PatCoFn = Coercion TcPat - -(<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition -Nothing <.> Nothing = Nothing -Nothing <.> Just f = Just f -Just f <.> Nothing = Just f -Just f1 <.> Just f2 = Just (f1 . f2) - -(<$>) :: Coercion a -> a -> a -Just f <$> e = f e -Nothing <$> e = e - -mkCoercion :: (a -> a) -> Coercion a -mkCoercion f = Just f - -idCoercion :: Coercion a -idCoercion = Nothing - -isIdCoercion :: Coercion a -> Bool -isIdCoercion = isNothing -\end{code} - -%************************************************************************ -%* * \subsection[Unify-exported]{Exported unification functions} %* * %************************************************************************ @@ -450,18 +611,20 @@ uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1 -- "True" means args swapped -- Predicates -uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2)) +uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2)) | n1 == n2 = uTys t1 t1 t2 t2 -uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2)) +uTys _ (PredTy (ClassP c1 tys1)) _ (PredTy (ClassP c2 tys2)) | c1 == c2 = unifyTauTyLists tys1 tys2 -uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2)) - | tc1 == tc2 = unifyTauTyLists tys1 tys2 -- Functions; just check the two parts uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2) = uTys fun1 fun1 fun2 fun2 `thenM_` uTys arg1 arg1 arg2 arg2 - -- Type constructors must match + -- NewType constructors must match +uTys _ (NewTcApp tc1 tys1) _ (NewTcApp tc2 tys2) + | tc1 == tc2 = unifyTauTyLists tys1 tys2 + + -- Ordinary type constructors must match uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2) | con1 == con2 && equalLength tys1 tys2 = unifyTauTyLists tys1 tys2 @@ -470,7 +633,7 @@ uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2) -- When we are doing kind checking, we might match a kind '?' -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and -- (CCallable Int) and (CCallable Int#) are both OK - = unifyOpenTypeKind ps_ty2 + = unifyTypeKind ps_ty2 -- Applications need a bit of care! -- They can match FunTy and TyConApp, so use splitAppTy_maybe @@ -711,8 +874,9 @@ okToUnifyWith tv ty ok (AppTy t1 t2) = ok t1 `and` ok t2 ok (FunTy t1 t2) = ok t1 `and` ok t2 ok (TyConApp _ ts) = oks ts + ok (NewTcApp _ ts) = oks ts ok (ForAllTy _ _) = Just NotMonoType - ok (SourceTy st) = ok_st st + ok (PredTy st) = ok_st st ok (NoteTy (FTVNote _) t) = ok t ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2 -- Type variables may be free in t1 but not t2 @@ -722,7 +886,6 @@ okToUnifyWith tv ty ok_st (ClassP _ ts) = oks ts ok_st (IParam _ t) = ok t - ok_st (NType _ ts) = oks ts Nothing `and` m = m Just p `and` m = Just p @@ -730,146 +893,6 @@ okToUnifyWith tv ty %************************************************************************ %* * -\subsection[Unify-fun]{@unifyFunTy@} -%* * -%************************************************************************ - -@subFunTy@ and @unifyFunTy@ is used to avoid the fruitless -creation of type variables. - -* subFunTy is used when we might be faced with a "hole" type variable, - in which case we should create two new holes. - -* unifyFunTy is used when we expect to encounter only "ordinary" - type variables, so we should create new ordinary type variables - -\begin{code} -subFunTy :: TcHoleType -- Fail if ty isn't a function type - -- If it's a hole, make two holes, feed them to... - -> (TcHoleType -> TcHoleType -> TcM a) -- the thing inside - -> TcM a -- and bind the function type to the hole - -subFunTy ty@(TyVarTy tyvar) thing_inside - | isHoleTyVar tyvar - = -- This is the interesting case - getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of { - Just ty' -> subFunTy ty' thing_inside ; - Nothing -> - - newHoleTyVarTy `thenM` \ arg_ty -> - newHoleTyVarTy `thenM` \ res_ty -> - - -- Do the business - thing_inside arg_ty res_ty `thenM` \ answer -> - - -- Extract the answers - readHoleResult arg_ty `thenM` \ arg_ty' -> - readHoleResult res_ty `thenM` \ res_ty' -> - - -- Write the answer into the incoming hole - putTcTyVar tyvar (mkFunTy arg_ty' res_ty') `thenM_` - - -- And return the answer - returnM answer } - -subFunTy ty thing_inside - = unifyFunTy ty `thenM` \ (arg,res) -> - thing_inside arg res - - -unifyFunTy :: TcRhoType -- Fail if ty isn't a function type - -> TcM (TcType, TcType) -- otherwise return arg and result types - -unifyFunTy ty@(TyVarTy tyvar) - = ASSERT( not (isHoleTyVar tyvar) ) - getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyFunTy ty' - Nothing -> unify_fun_ty_help ty - -unifyFunTy ty - = case tcSplitFunTy_maybe ty of - Just arg_and_res -> returnM arg_and_res - Nothing -> unify_fun_ty_help ty - -unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification - = newTyVarTy openTypeKind `thenM` \ arg -> - newTyVarTy openTypeKind `thenM` \ res -> - unifyTauTy ty (mkFunTy arg res) `thenM_` - returnM (arg,res) -\end{code} - -\begin{code} -unifyListTy :: TcType -- expected list type - -> TcM TcType -- list element type - -unifyListTy ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyListTy ty' - other -> unify_list_ty_help ty - -unifyListTy ty - = case tcSplitTyConApp_maybe ty of - Just (tycon, [arg_ty]) | tycon == listTyCon -> returnM arg_ty - other -> unify_list_ty_help ty - -unify_list_ty_help ty -- Revert to ordinary unification - = newTyVarTy liftedTypeKind `thenM` \ elt_ty -> - unifyTauTy ty (mkListTy elt_ty) `thenM_` - returnM elt_ty - --- variant for parallel arrays --- -unifyPArrTy :: TcType -- expected list type - -> TcM TcType -- list element type - -unifyPArrTy ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyPArrTy ty' - _ -> unify_parr_ty_help ty -unifyPArrTy ty - = case tcSplitTyConApp_maybe ty of - Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnM arg_ty - _ -> unify_parr_ty_help ty - -unify_parr_ty_help ty -- Revert to ordinary unification - = newTyVarTy liftedTypeKind `thenM` \ elt_ty -> - unifyTauTy ty (mkPArrTy elt_ty) `thenM_` - returnM elt_ty -\end{code} - -\begin{code} -unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType] -unifyTupleTy boxity arity ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyTupleTy boxity arity ty' - other -> unify_tuple_ty_help boxity arity ty - -unifyTupleTy boxity arity ty - = case tcSplitTyConApp_maybe ty of - Just (tycon, arg_tys) - | isTupleTyCon tycon - && tyConArity tycon == arity - && tupleTyConBoxity tycon == boxity - -> returnM arg_tys - other -> unify_tuple_ty_help boxity arity ty - -unify_tuple_ty_help boxity arity ty - = newTyVarTys arity kind `thenM` \ arg_tys -> - unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenM_` - returnM arg_tys - where - kind | isBoxed boxity = liftedTypeKind - | otherwise = openTypeKind -\end{code} - - -%************************************************************************ -%* * \subsection{Kind unification} %* * %************************************************************************ @@ -888,23 +911,23 @@ unifyKinds _ _ = panic "unifyKinds: length mis-match" \end{code} \begin{code} -unifyOpenTypeKind :: TcKind -> TcM () --- Ensures that the argument kind is of the form (Type bx) --- for some boxity bx +unifyTypeKind :: TcKind -> TcM () +-- Ensures that the argument kind is a liftedTypeKind or unliftedTypeKind +-- If it's a kind variable, make it (Type bx), for a fresh boxity variable bx -unifyOpenTypeKind ty@(TyVarTy tyvar) +unifyTypeKind ty@(TyVarTy tyvar) = getTcTyVar tyvar `thenM` \ maybe_ty -> case maybe_ty of - Just ty' -> unifyOpenTypeKind ty' - other -> unify_open_kind_help ty - -unifyOpenTypeKind ty + Just ty' -> unifyTypeKind ty' + Nothing -> newOpenTypeKind `thenM` \ kind -> + putTcTyVar tyvar kind `thenM_` + returnM () + +unifyTypeKind ty | isTypeKind ty = returnM () - | otherwise = unify_open_kind_help ty - -unify_open_kind_help ty -- Revert to ordinary unification - = newOpenTypeKind `thenM` \ open_kind -> - unifyKind ty open_kind + | otherwise -- Failure + = zonkTcType ty `thenM` \ ty1 -> + failWithTc (ptext SLIT("Type expected but") <+> quotes (ppr ty1) <+> ptext SLIT("found")) \end{code} \begin{code} @@ -969,6 +992,8 @@ unifyMisMatch ty1 ty2 zonkTcType ty2 `thenM` \ ty2' -> let (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2'] + ppr | isSuperKind (typeKind ty1) = pprKind + | otherwise = pprType msg = hang (ptext SLIT("Couldn't match")) 4 (sep [quotes (ppr tidy_ty1), ptext SLIT("against"),