Type subsumption and unification
\begin{code}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
module TcUnify (
-- Full-blown subsumption
- tcSubExp, tcFunResTy, tcGen,
+ tcSubExp, tcGen,
checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
-- Various unifications
unifyType, unifyTypeList, unifyTheta,
unifyKind, unifyKinds, unifyFunKind,
checkExpectedKind,
- preSubType, boxyMatchTypes,
+ preSubType, boxyMatchTypes,
--------------------------------
-- Holes
tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox,
boxyUnify, boxyUnifyList, zapToMonotype,
- boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
+ boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy,
wrapFunResCoercion
) where
import TcMType
import TcSimplify
import TcEnv
+import TcTyFuns
import TcIface
import TcRnMonad -- TcType, amongst others
import TcType
import Type
+import Coercion
import TysPrim
import Inst
import TyCon
import BasicTypes
import Util
import Outputable
+import Unique
+
+import Control.Monad
\end{code}
%************************************************************************
\begin{code}
tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType)
-tcInfer tc_infer
- = do { box <- newBoxyTyVar openTypeKind
- ; res <- tc_infer (mkTyVarTy box)
- ; res_ty <- readFilledBox box -- Guaranteed filled-in by now
- ; return (res, res_ty) }
+tcInfer tc_infer = withBox openTypeKind tc_infer
\end{code}
--
-- If (subFunTys n_args res_ty thing_inside) = (co_fn, res)
-- and the inner call to thing_inside passes args: [a1,...,an], b
--- then co_fn :: (a1 -> ... -> an -> b) -> res_ty
+-- then co_fn :: (a1 -> ... -> an -> b) ~ res_ty
--
-- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType
loop n args_so_far res_ty
| isSigmaTy res_ty -- Do this before checking n==0, because we
- -- guarantee to return a BoxyRhoType, not a BoxySigmaType
+ -- guarantee to return a BoxyRhoType, not a
+ -- BoxySigmaType
= do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
loop n args_so_far res_ty'
; return (gen_fn <.> co_fn, res) }
; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
; return (co_fn', res) }
+ -- Try to normalise synonym families and defer if that's not possible
+ loop n args_so_far ty@(TyConApp tc tys)
+ | isOpenSynTyCon tc
+ = do { (coi1, ty') <- tcNormaliseFamInst ty
+ ; case coi1 of
+ IdCo -> defer n args_so_far ty
+ -- no progress, but maybe solvable => defer
+ ACo _ -> -- progress: so lets try again
+ do { (co_fn, res) <- loop n args_so_far ty'
+ ; return $ (co_fn <.> coiToHsWrapper (mkSymCoI coi1), res)
+ }
+ }
+
-- res_ty might have a type variable at the head, such as (a b c),
-- in which case we must fill in with (->). Simplest thing to do
-- is to use boxyUnify, but we catch failure and generate our own
-- error message on failure
loop n args_so_far res_ty@(AppTy _ _)
= do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
- ; (_, mb_unit) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty')
- ; if isNothing mb_unit then bale_out args_so_far
- else loop n args_so_far (FunTy arg_ty' res_ty') }
+ ; (_, mb_coi) <- tryTcErrs $
+ boxyUnify res_ty (FunTy arg_ty' res_ty')
+ ; if isNothing mb_coi then bale_out args_so_far
+ else do { let coi = expectJust "subFunTys" mb_coi
+ ; (co_fn, res) <- loop n args_so_far (FunTy arg_ty'
+ res_ty')
+ ; return (co_fn <.> coiToHsWrapper coi, res)
+ }
+ }
- loop n args_so_far (TyVarTy tv)
+ loop n args_so_far ty@(TyVarTy tv)
| isTyConableTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> loop n args_so_far ty
- Flexi -> do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
- ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty
- ; return (idHsWrapper, res) } }
+ Flexi ->
+ do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
+ ; res <- thing_inside (reverse args_so_far ++ arg_tys)
+ res_ty
+ ; return (idHsWrapper, res) } }
+ | otherwise -- defer as tyvar may be refined by equalities
+ = defer n args_so_far ty
where
mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
mk_res_ty [] = panic "TcUnify.mk_res_ty1"
loop n args_so_far res_ty = bale_out args_so_far
+ -- build a template type a1 -> ... -> an -> b and defer an equality
+ -- between that template and the expected result type res_ty; then,
+ -- use the template to type the thing_inside
+ defer n args_so_far ty
+ = do { arg_tys <- newFlexiTyVarTys n argTypeKind
+ ; res_ty' <- newFlexiTyVarTy openTypeKind
+ ; let fun_ty = mkFunTys arg_tys res_ty'
+ err = error_herald <> comma $$
+ text "which does not match its type"
+ ; coi <- addErrCtxt err $
+ defer_unification False False fun_ty ty
+ ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty'
+ ; return (coiToHsWrapper coi, res)
+ }
+
bale_out args_so_far
= do { env0 <- tcInitTidyEnv
; res_ty' <- zonkTcType res_ty
----------------------
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) -- T a b c ~ orig_ty
+ -- It's used for wired-in tycons, so we call checkWiredInTyCon
-- Precondition: never called with FunTyCon
-- Precondition: input type :: *
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
+ ; traceTc $ text "boxySplitTyConApp:" <+>
+ ppr ty <+> text "==>" <+> ppr 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
= do { cts <- readMetaTyVar tv
; 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) }
- }
+ Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
+ ; 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
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
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}
withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType)
-- Allocate a *boxy* tyvar
withBox kind thing_inside
- = do { box_tv <- newMetaTyVar BoxTv kind
+ = do { box_tv <- newBoxyTyVar kind
; res <- thing_inside (mkTyVarTy box_tv)
- ; ty <- readFilledBox box_tv
+ ; ty <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv
; return (res, ty) }
\end{code}
(boxy_tvs `extendVarSetList` tvs2) tau2 subst
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
- | tc1 == tc2 = go_s tys1 tys2
+ | tc1 == tc2
+ , not $ isOpenSynTyCon tc1
+ = go_s tys1 tys2
go (FunTy arg1 res1) (FunTy arg2 res2)
= go_s [arg1,res1] [arg2,res2]
-- Look inside type synonyms, but only if the naive version fails
go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
- | Just ty2' <- tcView ty2 = go ty1 ty2'
+ | Just ty2' <- tcView ty1 = go ty1 ty2'
-- For now, we don't look inside ForAlls, PredTys
go ty1 ty2 = orig_ty1 -- Default
All the tcSub calls have the form
- tcSub expected_ty offered_ty
+ tcSub actual_ty expected_ty
which checks
- offered_ty <= expected_ty
+ actual_ty <= expected_ty
-That is, that a value of type offered_ty is acceptable in
+That is, that a value of type actual_ty is acceptable in
a place expecting a value of type expected_ty.
It returns a coercion function
- co_fn :: offered_ty -> expected_ty
-which takes an HsExpr of type offered_ty into one of type
+ co_fn :: actual_ty ~ expected_ty
+which takes an HsExpr of type actual_ty into one of type
expected_ty.
\begin{code}
-----------------
-tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
+tcSubExp :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper
-- (tcSub act exp) checks that
-- act <= exp
-tcSubExp actual_ty expected_ty
+tcSubExp orig actual_ty expected_ty
= -- addErrCtxtM (unifyCtxt actual_ty expected_ty) $
-- Adding the error context here leads to some very confusing error
-- messages, such as "can't match forall a. a->a with forall a. a->a"
-- So instead I'm adding the error context when moving from tc_sub to u_tys
traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >>
- tc_sub SubOther actual_ty actual_ty False expected_ty expected_ty
+ tc_sub orig actual_ty actual_ty False expected_ty expected_ty
-tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
-tcFunResTy fun actual_ty expected_ty
- = traceTc (text "tcFunResTy" <+> ppr actual_ty <+> ppr expected_ty) >>
- tc_sub (SubFun fun) actual_ty actual_ty False expected_ty expected_ty
-
-----------------
-data SubCtxt = SubDone -- Error-context already pushed
- | SubFun Name -- Context is tcFunResTy
- | SubOther -- Context is something else
-
-tc_sub :: SubCtxt -- How to add an error-context
+tc_sub :: InstOrigin
-> BoxySigmaType -- actual_ty, before expanding synonyms
-> BoxySigmaType -- ..and after
-> InBox -- True <=> expected_ty is inside a box
-- This invariant is needed so that we can "see" the foralls, ad
-- e.g. in the SPEC rule where we just use splitSigmaTy
-tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty
= traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >>
- tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
-- This indirection is just here to make
-- it easy to insert a debug trace!
-tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
- | Just exp_ty' <- tcView exp_ty = tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty'
-tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
- | Just act_ty' <- tcView act_ty = tc_sub sub_ctxt act_sty act_ty' exp_ib exp_sty exp_ty
+tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
+ | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty'
+tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
+ | Just act_ty' <- tcView act_ty = tc_sub orig act_sty act_ty' exp_ib exp_sty exp_ty
-----------------------------------
-- Rule SBOXY, plus other cases when act_ty is a type variable
-- Just defer to boxy matching
-- This rule takes precedence over SKOL!
-tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
- = do { addSubCtxt sub_ctxt act_sty exp_sty $
- uVar True False tv exp_ib exp_sty exp_ty
- ; return idHsWrapper }
+tc_sub1 orig act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
+ = do { traceTc (text "tc_sub1 - case 1")
+ ; coi <- addSubCtxt orig act_sty exp_sty $
+ uVar True False tv exp_ib exp_sty exp_ty
+ ; traceTc (case coi of
+ IdCo -> text "tc_sub1 (Rule SBOXY) IdCo"
+ ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co)
+ ; return $ coiToHsWrapper coi
+ }
-----------------------------------
-- Skolemisation case (rule SKOL)
-- g :: Ord b => b->b
-- Consider f g !
-tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
- | isSigmaTy exp_ty
- = if exp_ib then -- SKOL does not apply if exp_ty is inside a box
- defer_to_boxy_matching sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
+ | isSigmaTy exp_ty = do
+ { traceTc (text "tc_sub1 - case 2") ;
+ if exp_ib then -- SKOL does not apply if exp_ty is inside a box
+ defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
else do
{ (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
- tc_sub sub_ctxt act_sty act_ty False body_exp_ty body_exp_ty
+ tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
; return (gen_fn <.> co_fn) }
+ }
where
act_tvs = tyVarsOfType act_ty
-- It's really important to check for escape wrt
-- expected_ty: Int -> Int
-- co_fn e = e Int dOrdInt
-tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
-- Implements the new SPEC rule in the Appendix of the paper
-- "Boxy types: inference for higher rank types and impredicativity"
-- (This appendix isn't in the published version.)
-- Pre-subsumpion finds a|->Int, and that works fine, whereas
-- just running full subsumption would fail.
| isSigmaTy actual_ty
- = do { -- Perform pre-subsumption, and instantiate
+ = do { traceTc (text "tc_sub1 - case 3")
+ ; -- Perform pre-subsumption, and instantiate
-- the type with info from the pre-subsumption;
-- boxy tyvars if pre-subsumption gives no info
let (tyvars, theta, tau) = tcSplitSigmaTy actual_ty
; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty,
ppr tyvars <+> ppr theta <+> ppr tau,
ppr tau'])
- ; co_fn2 <- tc_sub sub_ctxt tau' tau' exp_ib exp_sty expected_ty
+ ; co_fn2 <- tc_sub orig tau' tau' exp_ib exp_sty expected_ty
-- Deal with the dictionaries
- -- The origin gives a helpful origin when we have
- -- a function with type f :: Int -> forall a. Num a => ...
- -- This way the (Num a) dictionary gets an OccurrenceOf f origin
- ; let orig = case sub_ctxt of
- SubFun n -> OccurrenceOf n
- other -> InstSigOrigin -- Unhelpful
; co_fn1 <- instCall orig inst_tys (substTheta subst' theta)
; return (co_fn2 <.> co_fn1) }
-----------------------------------
-- Function case (rule F1)
-tc_sub1 sub_ctxt act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
- = addSubCtxt sub_ctxt act_sty exp_sty $
- tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
+tc_sub1 orig act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
+ = do { traceTc (text "tc_sub1 - case 4")
+ ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
+ }
-- Function case (rule F2)
-tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
+tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
| isBoxyTyVar exp_tv
- = addSubCtxt sub_ctxt act_sty exp_sty $
- do { cts <- readMetaTyVar exp_tv
+ = do { traceTc (text "tc_sub1 - case 5")
+ ; cts <- readMetaTyVar exp_tv
; case cts of
- Indirect ty -> tc_sub SubDone act_sty act_ty True exp_sty ty
- Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
- ; tc_sub_funs act_arg act_res True arg_ty res_ty } }
+ Indirect ty -> tc_sub orig act_sty act_ty True exp_sty ty
+ Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
+ ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } }
where
mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
mk_res_ty other = panic "TcUnify.mk_res_ty3"
fun_kinds = [argTypeKind, openTypeKind]
-- Everything else: defer to boxy matching
-tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
- = defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv)
+ = do { traceTc (text "tc_sub1 - case 6a" <+> ppr [isBoxyTyVar exp_tv, isMetaTyVar exp_tv, isSkolemTyVar exp_tv, isExistentialTyVar exp_tv,isSigTyVar exp_tv] )
+ ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
+ }
+
+tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
+ = do { traceTc (text "tc_sub1 - case 6")
+ ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
+ }
-----------------------------------
-defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
- = do { addSubCtxt sub_ctxt act_sty exp_sty $
- u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty
- ; return idHsWrapper }
- where
- outer = case sub_ctxt of -- Ugh
- SubDone -> False
- other -> True
+defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
+ = do { coi <- addSubCtxt orig act_sty exp_sty $
+ u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty
+ ; return $ coiToHsWrapper coi }
-----------------------------------
-tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
- = do { uTys False act_arg exp_ib exp_arg
- ; co_fn_res <- tc_sub SubDone act_res act_res exp_ib exp_res exp_res
- ; wrapFunResCoercion [exp_arg] co_fn_res }
+tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
+ = do { arg_coi <- addSubCtxt orig act_arg exp_arg $
+ uTysOuter False act_arg exp_ib exp_arg
+ ; co_fn_res <- tc_sub orig act_res act_res exp_ib exp_res exp_res
+ ; wrapper1 <- wrapFunResCoercion [exp_arg] co_fn_res
+ ; let wrapper2 = case arg_coi of
+ IdCo -> idHsWrapper
+ ACo co -> WpCo $ FunTy co act_res
+ ; return (wrapper1 <.> wrapper2) }
-----------------------------------
wrapFunResCoercion
-> HsWrapper -- HsExpr a -> HsExpr b
-> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
wrapFunResCoercion arg_tys co_fn_res
- | isIdHsWrapper co_fn_res = return idHsWrapper
- | null arg_tys = return co_fn_res
- | otherwise
+ | isIdHsWrapper co_fn_res
+ = return idHsWrapper
+ | null arg_tys
+ = return co_fn_res
+ | otherwise
= do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys
; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) }
\end{code}
tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
-- If not, the call is a no-op
- = do { -- We want the GenSkol info in the skolemised type variables to
+ = do { traceTc (text "tcGen")
+ -- We want the GenSkol info in the skolemised type variables to
-- mention the *instantiated* tyvar names, so that we get a
-- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
-- Hence the tiresome but innocuous fixM
- ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
+ ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
-- Get loation from monad, not from expected_ty
; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
-- list of "free vars" for the signature check.
; loc <- getInstLoc (SigOrigin skol_info)
- ; dicts <- newDictBndrs loc theta'
+ ; dicts <- newDictBndrs loc theta' -- Includes equalities
; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
; checkSigTyVarsWrt free_tvs tvs'
; let
-- The WpLet binds any Insts which came out of the simplification.
- dict_ids = map instToId dicts
- co_fn = mkWpTyLams tvs' <.> mkWpLams dict_ids <.> WpLet inst_binds
- ; returnM (co_fn, result) }
+ dict_vars = map instToVar dicts
+ co_fn = mkWpTyLams tvs' <.> mkWpLams dict_vars <.> WpLet inst_binds
+ ; return (co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
-\end{code}
+\end{code}
non-exported generic functions.
\begin{code}
-boxyUnify :: BoxyType -> BoxyType -> TcM ()
+boxyUnify :: BoxyType -> BoxyType -> TcM CoercionI
-- Acutal and expected, respectively
boxyUnify ty1 ty2
= addErrCtxtM (unifyCtxt ty1 ty2) $
uTysOuter False ty1 False ty2
---------------
-boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM ()
+boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM [CoercionI]
-- Arguments should have equal length
-- Acutal and expected types
boxyUnifyList tys1 tys2 = uList boxyUnify tys1 tys2
---------------
-unifyType :: TcTauType -> TcTauType -> TcM ()
+unifyType :: TcTauType -> TcTauType -> TcM CoercionI
-- No boxes expected inside these types
-- Acutal and expected types
unifyType ty1 ty2 -- ty1 expected, ty2 inferred
uTysOuter True ty1 True ty2
---------------
-unifyPred :: PredType -> PredType -> TcM ()
+unifyPred :: PredType -> PredType -> TcM CoercionI
-- Acutal and expected types
unifyPred p1 p2 = addErrCtxtM (unifyCtxt (mkPredTy p1) (mkPredTy p2)) $
- uPred True True p1 True p2
+ uPred True True p1 True p2
-unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
+unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI]
-- Acutal and expected types
unifyTheta theta1 theta2
= do { checkTc (equalLength theta1 theta2)
(vcat [ptext SLIT("Contexts differ in length"),
nest 2 $ parens $ ptext SLIT("Use -fglasgow-exts to allow this")])
- ; uList unifyPred theta1 theta2 }
+ ; uList unifyPred theta1 theta2
+ }
---------------
-uList :: (a -> a -> TcM ())
- -> [a] -> [a] -> TcM ()
+uList :: (a -> a -> TcM b)
+ -> [a] -> [a] -> TcM [b]
-- Unify corresponding elements of two lists of types, which
--- should be f equal length. We charge down the list explicitly so that
+-- should be of equal length. We charge down the list explicitly so that
-- we can complain if their lengths differ.
-uList unify [] [] = return ()
-uList unify (ty1:tys1) (ty2:tys2) = do { unify ty1 ty2; uList unify tys1 tys2 }
+uList unify [] [] = return []
+uList unify (ty1:tys1) (ty2:tys2) = do { x <- unify ty1 ty2;
+ ; xs <- uList unify tys1 tys2
+ ; return (x:xs)
+ }
uList unify ty1s ty2s = panic "Unify.uList: mismatched type lists!"
\end{code}
\begin{code}
unifyTypeList :: [TcTauType] -> TcM ()
-unifyTypeList [] = returnM ()
-unifyTypeList [ty] = returnM ()
+unifyTypeList [] = return ()
+unifyTypeList [ty] = return ()
unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
; unifyTypeList tys }
\end{code}
%* *
%************************************************************************
-@uTys@ is the heart of the unifier. Each arg happens twice, because
-we want to report errors in terms of synomyms if poss. The first of
+@uTys@ is the heart of the unifier. Each arg occurs twice, because
+we want to report errors in terms of synomyms if possible. The first of
the pair is used in error messages only; it is always the same as the
second, except that if the first is a synonym then the second may be a
de-synonym'd version. This way we get better error messages.
We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
\begin{code}
+type SwapFlag = Bool
+ -- False <=> the two args are (actual, expected) respectively
+ -- True <=> the two args are (expected, actual) respectively
+
type InBox = Bool -- True <=> we are inside a box
-- False <=> we are outside a box
-- The importance of this is that if we get "filled-box meets
-- pop the context to remove the "Expected/Acutal" context
uTysOuter, uTys
- :: InBox -> TcType -- ty1 is the *expected* type
- -> InBox -> TcType -- ty2 is the *actual* type
- -> TcM ()
-uTysOuter nb1 ty1 nb2 ty2 = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
- ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 }
-uTys nb1 ty1 nb2 ty2 = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
- ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 }
+ :: InBox -> TcType -- ty1 is the *actual* type
+ -> InBox -> TcType -- ty2 is the *expected* type
+ -> TcM CoercionI
+uTysOuter nb1 ty1 nb2 ty2
+ = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
+ ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 }
+uTys nb1 ty1 nb2 ty2
+ = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
+ ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 }
--------------
-uTys_s :: InBox -> [TcType] -- ty1 is the *actual* types
- -> InBox -> [TcType] -- ty2 is the *expected* types
- -> TcM ()
-uTys_s nb1 [] nb2 [] = returnM ()
-uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { uTys nb1 ty1 nb2 ty2
- ; uTys_s nb1 tys1 nb2 tys2 }
+uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types
+ -> InBox -> [TcType] -- tys2 are the *expected* types
+ -> TcM [CoercionI]
+uTys_s nb1 [] nb2 [] = 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 nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!"
--------------
u_tys :: Outer
-> InBox -> TcType -> TcType -- ty1 is the *actual* type
-> InBox -> TcType -> TcType -- ty2 is the *expected* type
- -> TcM ()
+ -> TcM CoercionI
u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
- = go outer ty1 ty2
+ = do { traceTc (text "u_tys " <+> ppr ty1 <+> text " " <+> ppr ty2)
+ ; coi <- go outer ty1 ty2
+ ; traceTc (case coi of
+ ACo co -> text "u_tys yields coercion: " <+> ppr co
+ IdCo -> text "u_tys yields no coercion")
+ ; return coi
+ }
where
- -- Always expand synonyms (see notes at end)
+ go :: Outer -> TcType -> TcType -> TcM CoercionI
+ go outer ty1 ty2 =
+ do { traceTc (text "go " <+> ppr orig_ty1 <+> text "/" <+> ppr ty1
+ <+> ppr orig_ty2 <+> text "/" <+> ppr ty2)
+ ; go1 outer ty1 ty2
+ }
+
+ go1 :: Outer -> TcType -> TcType -> TcM CoercionI
+ -- Always expand synonyms: see Note [Unification and synonyms]
-- (this also throws away FTVs)
- go outer ty1 ty2
+ go1 outer ty1 ty2
| Just ty1' <- tcView ty1 = go False ty1' ty2
| Just ty2' <- tcView ty2 = go False ty1 ty2'
-- Variables; go for uVar
- go outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
- go outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 ty1
+ go1 outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
+ go1 outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 ty1
-- "True" means args swapped
-- The case for sigma-types must *follow* the variable cases
-- because a boxy variable can be filed with a polytype;
-- but must precede FunTy, because ((?x::Int) => ty) look
-- like a FunTy; there isn't necy a forall at the top
- go _ ty1 ty2
+ go1 _ ty1 ty2
| isSigmaTy ty1 || isSigmaTy ty2
- = do { checkM (equalLength tvs1 tvs2)
+ = do { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2)
+ ; unless (equalLength tvs1 tvs2)
(unifyMisMatch outer False orig_ty1 orig_ty2)
-
+ ; traceTc (text "We're past the first length test")
; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
-- Get location from monad, not from tvs1
; let tys = mkTyVarTys tvs
(theta2,tau2) = tcSplitPhiTy phi2
; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
- { checkM (equalLength theta1 theta2)
+ { unless (equalLength theta1 theta2)
(unifyMisMatch outer False orig_ty1 orig_ty2)
- ; uPreds False nb1 theta1 nb2 theta2
- ; uTys nb1 tau1 nb2 tau2
+ ; cois <- uPreds False nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
+ ; traceTc (text "TOMDO!")
+ ; coi <- uTys nb1 tau1 nb2 tau2
-- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
- ; ifM (any (`elemVarSet` free_tvs) tvs)
+ ; when (any (`elemVarSet` free_tvs) tvs)
(bleatEscapedTvs free_tvs tvs tvs)
-- If both sides are inside a box, we are in a "box-meets-box"
-- the same polytype... but it should be a monotype.
-- This check comes last, because the error message is
-- extremely unhelpful.
- ; ifM (nb1 && nb2) (notMonoType ty1)
+ ; when (nb1 && nb2) (notMonoType ty1)
+ ; return coi
}}
where
(tvs1, body1) = tcSplitForAllTys ty1
(tvs2, body2) = tcSplitForAllTys ty2
-- Predicates
- go outer (PredTy p1) (PredTy p2) = uPred False nb1 p1 nb2 p2
+ go1 outer (PredTy p1) (PredTy p2)
+ = uPred False nb1 p1 nb2 p2
-- Type constructors must match
- go _ (TyConApp con1 tys1) (TyConApp con2 tys2)
- | con1 == con2 = uTys_s nb1 tys1 nb2 tys2
+ go1 _ (TyConApp con1 tys1) (TyConApp con2 tys2)
+ | con1 == con2 && not (isOpenSynTyCon con1)
+ = do { cois <- uTys_s nb1 tys1 nb2 tys2
+ ; return $ mkTyConAppCoI con1 tys1 cois
+ }
-- See Note [TyCon app]
+ | con1 == con2 && identicalOpenSynTyConApp
+ = do { cois <- uTys_s nb1 tys1' nb2 tys2'
+ ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
+ }
+ where
+ n = tyConArity con1
+ (idxTys1, tys1') = splitAt n tys1
+ (idxTys2, tys2') = splitAt n tys2
+ identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
+ -- See Note [OpenSynTyCon app]
-- Functions; just check the two parts
- go _ (FunTy fun1 arg1) (FunTy fun2 arg2)
- = do { uTys nb1 fun1 nb2 fun2
- ; uTys nb1 arg1 nb2 arg2 }
+ go1 _ (FunTy fun1 arg1) (FunTy fun2 arg2)
+ = do { coi_l <- uTys nb1 fun1 nb2 fun2
+ ; coi_r <- uTys nb1 arg1 nb2 arg2
+ ; return $ mkFunTyCoI fun1 coi_l arg1 coi_r
+ }
-- Applications need a bit of care!
-- 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
- go outer (AppTy s1 t1) ty2
+ go1 outer (AppTy s1 t1) ty2
| Just (s2,t2) <- tcSplitAppTy_maybe ty2
- = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
+ = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2
+ ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
-- Now the same, but the other way round
-- Don't swap the types, because the error messages get worse
- go outer ty1 (AppTy s2 t2)
+ go1 outer ty1 (AppTy s2 t2)
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
- = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
+ = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2
+ ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
+
+ -- One or both outermost constructors are type family applications.
+ -- If we can normalise them away, proceed as usual; otherwise, we
+ -- need to defer unification by generating a wanted equality constraint.
+ go1 outer ty1 ty2
+ | ty1_is_fun || ty2_is_fun
+ = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1
+ else return (IdCo, ty1)
+ ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2
+ else return (IdCo, ty2)
+ ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2'
+ then do { -- One type family app can't be reduced yet
+ -- => defer
+ ; ty1'' <- zonkTcType ty1'
+ ; ty2'' <- zonkTcType ty2'
+ ; if tcEqType ty1'' ty2''
+ then return IdCo
+ else -- see [Deferred Unification]
+ defer_unification outer False orig_ty1 orig_ty2
+ }
+ else -- unification can proceed
+ go outer ty1' ty2'
+ ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2)
+ }
+ where
+ ty1_is_fun = isOpenSynTyConApp ty1
+ ty2_is_fun = isOpenSynTyConApp ty2
+ -- Anything else fails
+ go1 outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
- -- Anything else fails
- go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
----------
uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
- | n1 == n2 = uTys nb1 t1 nb2 t2
+ | 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 = uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
+ | c1 == c2 =
+ do { cois <- uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
+ ; return $ mkClassPPredCoI c1 tys1 cois
+ }
uPred outer _ p1 _ p2 = unifyMisMatch outer False (mkPredTy p1) (mkPredTy p2)
-uPreds outer nb1 [] nb2 [] = return ()
-uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) = uPred outer nb1 p1 nb2 p2 >> uPreds outer nb1 ps1 nb2 ps2
+uPreds outer nb1 [] nb2 [] = return []
+uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
+ do { coi <- uPred outer nb1 p1 nb2 p2
+ ; cois <- uPreds outer nb1 ps1 nb2 ps2
+ ; return (coi:cois)
+ }
uPreds outer nb1 ps1 nb2 ps2 = panic "uPreds"
\end{code}
-Note [Tycon app]
+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
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 [OpenSynTyCon app]
+~~~~~~~~~~~~~~~~~~~~~~~
+Given
-Notes on synonyms
-~~~~~~~~~~~~~~~~~
+ type family T a :: * -> *
+
+the two types (T () a) and (T () Int) must unify, even if there are
+no type instances for T at all. Should we just turn them into an
+equality (T () a ~ T () Int)? I don't think so. We currently try to
+eagerly unify everything we can before generating equalities; otherwise,
+we could turn the unification of [Int] with [a] into an equality, too.
+
+Note [Unification and synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If you are tempted to make a short cut on synonyms, as in this
pseudocode...
\begin{code}
uVar :: Outer
- -> Bool -- False => tyvar is the "expected"
- -- True => ty is the "expected" thing
+ -> SwapFlag -- False => tyvar is the "actual" (ty is "expected")
+ -- True => ty is the "actual" (tyvar is "expected")
-> TcTyVar
-> InBox -- True <=> definitely no boxes in t2
-> TcTauType -> TcTauType -- printing and real versions
- -> TcM ()
+ -> TcM CoercionI
uVar outer swapped tv1 nb2 ps_ty2 ty2
= do { let expansion | showSDoc (ppr ty2) == showSDoc (ppr ps_ty2) = empty
----------------
uUnfilledVar :: Outer
- -> Bool -- Args are swapped
+ -> SwapFlag
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
-> TcTauType -> TcTauType -- Type 2
- -> TcM ()
+ -> TcM CoercionI
-- Invariant: tyvar 1 is not unified with anything
uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
MetaTv BoxTv ref1 -- A boxy type variable meets itself;
-- this is box-meets-box, so fill in with a tau-type
-> do { tau_tv <- tcInstTyVar tv1
- ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) }
- other -> returnM () -- No-op
+ ; updateMeta tv1 ref1 (mkTyVarTy tau_tv)
+ ; return IdCo
+ }
+ other -> return IdCo -- No-op
- -- Distinct type variables
- | otherwise
+ | otherwise -- Distinct type variables
= do { lookup2 <- lookupTcTyVar tv2
; case lookup2 of
- IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2'
+ IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2'
DoneTv details2 -> uUnfilledVars outer swapped tv1 details1 tv2 details2
}
-uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2 -- ty2 is not a type variable
- = case details1 of
- MetaTv (SigTv _) ref1 -> mis_match -- Can't update a skolem with a non-type-variable
- MetaTv info ref1 -> uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2
- skolem_details -> mis_match
+uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2
+ = -- ty2 is not a type variable
+ case details1 of
+ MetaTv (SigTv _) _ -> rigid_variable
+ MetaTv info ref1 ->
+ uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2
+ SkolemTv _ -> rigid_variable
where
- mis_match = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2
+ rigid_variable
+ | isOpenSynTyConApp non_var_ty2
+ = -- 'non_var_ty2's outermost constructor is a type family,
+ -- which we may may be able to normalise
+ do { (coi2, ty2') <- tcNormaliseFamInst non_var_ty2
+ ; case coi2 of
+ IdCo -> -- no progress, but maybe after other instantiations
+ defer_unification outer swapped (TyVarTy tv1) ps_ty2
+ ACo co -> -- progress: so lets try again
+ do { traceTc $
+ ppr co <+> text "::"<+> ppr non_var_ty2 <+> text "~" <+>
+ ppr ty2'
+ ; coi <- uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2'
+ ; let coi2' = (if swapped then id else mkSymCoI) coi2
+ ; return $ coi2' `mkTransCoI` coi
+ }
+ }
+ | SkolemTv RuntimeUnkSkol <- details1
+ -- runtime unknown will never match
+ = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2
+ | otherwise -- defer as a given equality may still resolve this
+ = defer_unification outer swapped (TyVarTy tv1) ps_ty2
+\end{code}
+
+Note [Deferred Unification]
+~~~~~~~~~~~~~~~~~~~~
+We may encounter a unification ty1 = ty2 that cannot be performed syntactically,
+and yet its consistency is undetermined. Previously, there was no way to still
+make it consistent. So a mismatch error was issued.
+
+Now these unfications are deferred until constraint simplification, where type
+family instances and given equations may (or may not) establish the consistency.
+Deferred unifications are of the form
+ F ... ~ ...
+or x ~ ...
+where F is a type function and x is a type variable.
+E.g.
+ id :: x ~ y => x -> y
+ id e = e
+
+involves the unfication x = y. It is deferred until we bring into account the
+context x ~ y to establish that it holds.
+
+If available, we defer original types (rather than those where closed type
+synonyms have already been expanded via tcCoreView). This is, as usual, to
+improve error messages.
+
+We need to both 'unBox' and zonk deferred types. We need to unBox as
+functions, such as TcExpr.tcMonoExpr promise to fill boxes in the expected
+type. We need to zonk as the types go into the kind of the coercion variable
+`cotv' and those are not zonked in Inst.zonkInst. (Maybe it would be better
+to zonk in zonInst instead. Would that be sufficient?)
+
+\begin{code}
+defer_unification :: Bool -- pop innermost context?
+ -> SwapFlag
+ -> TcType
+ -> TcType
+ -> TcM CoercionI
+defer_unification outer True ty1 ty2
+ = defer_unification outer False ty2 ty1
+defer_unification outer False ty1 ty2
+ = do { ty1' <- unBox ty1 >>= zonkTcType -- unbox *and* zonk..
+ ; ty2' <- unBox ty2 >>= zonkTcType -- ..see preceding note
+ ; traceTc $ text "deferring:" <+> ppr ty1 <+> text "~" <+> ppr ty2
+ ; cotv <- newMetaCoVar ty1' ty2'
+ -- put ty1 ~ ty2 in LIE
+ -- Left means "wanted"
+ ; inst <- (if outer then popErrCtxt else id) $
+ mkEqInst (EqPred ty1' ty2') (Left cotv)
+ ; extendLIE inst
+ ; return $ ACo $ TyVarTy cotv }
----------------
-uMetaVar :: Bool
+uMetaVar :: Bool -- pop innermost context?
+ -> SwapFlag
-> TcTyVar -> BoxInfo -> IORef MetaDetails
-> TcType -> TcType
- -> TcM ()
+ -> TcM CoercionI
-- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
-- ty2 is not a type variable
-uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
+uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
= -- tv1 is a BoxTv. So we must unbox ty2, to ensure
-- that any boxes in ty2 are filled with monotypes
--
; case meta_details of
Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
return () -- This really should *not* happen
- Flexi -> return ()
+ Flexi -> return ()
#endif
- ; checkUpdateMeta swapped tv1 ref1 final_ty }
-
-uMetaVar swapped tv1 info1 ref1 ps_ty2 non_var_ty2
- = do { final_ty <- checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check
- ; checkUpdateMeta swapped tv1 ref1 final_ty }
+ ; checkUpdateMeta swapped tv1 ref1 final_ty
+ ; return IdCo
+ }
+
+uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_ty2
+ = do { -- Occurs check + monotype check
+ ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2
+ ; case mb_final_ty of
+ Nothing -> -- tv1 occured in type family parameter
+ defer_unification outer swapped (mkTyVarTy tv1) ps_ty2
+ Just final_ty ->
+ do { checkUpdateMeta swapped tv1 ref1 final_ty
+ ; return IdCo
+ }
+ }
----------------
uUnfilledVars :: Outer
- -> Bool -- Args are swapped
+ -> SwapFlag
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
-> TcTyVar -> TcTyVarDetails -- Tyvar 2
- -> TcM ()
+ -> TcM CoercionI
-- Invarant: The type variables are distinct,
-- Neither is filled in yet
-- They might be boxy or not
uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (SkolemTv _)
- = unifyMisMatch outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
+ = -- see [Deferred Unification]
+ defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _)
- = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2)
+ = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo
uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2)
- = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+ = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo
-- ToDo: this function seems too long for what it acutally does!
uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
= case (info1, info2) of
- (BoxTv, BoxTv) -> box_meets_box
+ (BoxTv, BoxTv) -> box_meets_box >> return IdCo
-- If a box meets a TauTv, but the fomer has the smaller kind
-- then we must create a fresh TauTv with the smaller kind
- (_, BoxTv) | k1_sub_k2 -> update_tv2
- | otherwise -> box_meets_box
- (BoxTv, _ ) | k2_sub_k1 -> update_tv1
- | otherwise -> box_meets_box
+ (_, BoxTv) | k1_sub_k2 -> update_tv2 >> return IdCo
+ | otherwise -> box_meets_box >> return IdCo
+ (BoxTv, _ ) | k2_sub_k1 -> update_tv1 >> return IdCo
+ | otherwise -> box_meets_box >> return IdCo
-- Avoid SigTvs if poss
- (SigTv _, _ ) | k1_sub_k2 -> update_tv2
- (_, SigTv _) | k2_sub_k1 -> update_tv1
+ (SigTv _, _ ) | k1_sub_k2 -> update_tv2 >> return IdCo
+ (_, SigTv _) | k2_sub_k1 -> update_tv1 >> return IdCo
(_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
- then update_tv1 -- Same kinds
- else update_tv2
- | k2_sub_k1 -> update_tv1
- | otherwise -> kind_err
+ then update_tv1 >> return IdCo -- Same kinds
+ else update_tv2 >> return IdCo
+ | k2_sub_k1 -> update_tv1 >> return IdCo
+ | otherwise -> kind_err >> return IdCo
-- Update the variable with least kind info
-- See notes on type inference in Kind.lhs
-- Try to update sys-y type variables in preference to ones
-- gotten (say) by instantiating a polymorphic function with
-- a user-written type sig
-
-----------------
-checkUpdateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
--- Update tv1, which is flexi; occurs check is alrady done
--- The 'check' version does a kind check too
--- We do a sub-kind check here: we might unify (a b) with (c d)
--- where b::*->* and d::*; this should fail
-
-checkUpdateMeta swapped tv1 ref1 ty2
- = do { checkKinds swapped tv1 ty2
- ; updateMeta tv1 ref1 ty2 }
-
-updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
-updateMeta tv1 ref1 ty2
- = ASSERT( isMetaTyVar tv1 )
- ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
- do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
- ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
- ; writeMutVar ref1 (Indirect ty2) }
-
-----------------
-checkKinds swapped tv1 ty2
--- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
--- ty2 has been zonked at this stage, which ensures that
--- its kind has as much boxity information visible as possible.
- | tk2 `isSubKind` tk1 = returnM ()
-
- | otherwise
- -- Either the kinds aren't compatible
- -- (can happen if we unify (a b) with (c d))
- -- or we are unifying a lifted type variable with an
- -- unlifted type: e.g. (id 3#) is illegal
- = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
- unifyKindMisMatch k1 k2
- where
- (k1,k2) | swapped = (tk2,tk1)
- | otherwise = (tk1,tk2)
- tk1 = tyVarKind tv1
- tk2 = typeKind ty2
-
-----------------
-checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType
--- (checkTauTvUpdate tv ty)
--- We are about to update the TauTv tv with ty.
--- Check (a) that tv doesn't occur in ty (occurs check)
--- (b) that ty is a monotype
--- Furthermore, in the interest of (b), if you find an
--- empty box (BoxTv that is Flexi), fill it in with a TauTv
---
--- Returns the (non-boxy) type to update the type variable with, or fails
-
-checkTauTvUpdate orig_tv orig_ty
- = go orig_ty
- where
- go (TyConApp tc tys)
- | isSynTyCon tc = go_syn tc tys
- | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') }
- go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
- go (PredTy p) = do { p' <- go_pred p; return (PredTy p') }
- go (FunTy arg res) = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') }
- go (AppTy fun arg) = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') }
- -- NB the mkAppTy; we might have instantiated a
- -- type variable to a type constructor, so we need
- -- to pull the TyConApp to the top.
- go (ForAllTy tv ty) = notMonoType orig_ty -- (b)
-
- go (TyVarTy tv)
- | orig_tv == tv = occurCheck tv orig_ty -- (a)
- | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv)
- | otherwise = return (TyVarTy tv)
- -- Ordinary (non Tc) tyvars
- -- occur inside quantified types
-
- go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') }
- go_pred (IParam n ty) = do { ty' <- go ty; return (IParam n ty') }
- go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') }
-
- go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
- go_tyvar tv (MetaTv box ref)
- = do { cts <- readMutVar ref
- ; case cts of
- Indirect ty -> go ty
- Flexi -> case box of
- BoxTv -> fillBoxWithTau tv ref
- other -> return (TyVarTy tv)
- }
-
- -- go_syn is called for synonyms only
- -- See Note [Type synonyms and the occur check]
- go_syn tc tys
- | not (isTauTyCon tc)
- = notMonoType orig_ty -- (b) again
- | otherwise
- = do { (msgs, mb_tys') <- tryTc (mapM go tys)
- ; case mb_tys' of
- Just tys' -> return (TyConApp tc tys')
- -- Retain the synonym (the common case)
- Nothing | isOpenTyCon tc
- -> notMonoArgs (TyConApp tc tys)
- -- Synonym families must have monotype args
- | otherwise
- -> go (expectJust "checkTauTvUpdate"
- (tcView (TyConApp tc tys)))
- -- Try again, expanding the synonym
- }
-
-fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
--- (fillBoxWithTau tv ref) fills ref with a freshly allocated
--- tau-type meta-variable, whose print-name is the same as tv
--- Choosing the same name is good: when we instantiate a function
--- we allocate boxy tyvars with the same print-name as the quantified
--- tyvar; and then we often fill the box with a tau-tyvar, and again
--- we want to choose the same name.
-fillBoxWithTau tv ref
- = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget
- ; let tau = mkTyVarTy tv' -- name of the type variable
- ; writeMutVar ref (Indirect tau)
- ; return tau }
\end{code}
-Note [Type synonyms and the occur check]
-~~~~~~~~~~~~~~~~~~~~
-Basically we want to update tv1 := ps_ty2
-because ps_ty2 has type-synonym info, which improves later error messages
-
-But consider
- type A a = ()
-
- f :: (A a -> a -> ()) -> ()
- f = \ _ -> ()
-
- x :: ()
- x = f (\ x p -> p x)
-
-In the application (p x), we try to match "t" with "A t". If we go
-ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
-an infinite loop later.
-But we should not reject the program, because A t = ().
-Rather, we should bind t to () (= non_var_ty2).
-
\begin{code}
refineBox :: TcType -> TcM TcType
-- Unbox the outer box of a boxy type (if any)
| isMetaTyVar box_tv
= do { cts <- readMetaTyVar box_tv
; case cts of
- Flexi -> return ty
+ Flexi -> return ty
Indirect ty -> return ty }
refineBox other_ty = return other_ty
, MetaTv BoxTv ref <- tcTyVarDetails box_tv
= do { cts <- readMutVar ref
; case cts of
- Flexi -> fillBoxWithTau box_tv ref
+ Flexi -> fillBoxWithTau box_tv ref
Indirect ty -> return ty }
refineBoxToTau other_ty = return other_ty
--
-- For once, it's safe to treat synonyms as opaque!
-unBox (NoteTy n ty) = do { ty' <- unBox ty; return (NoteTy n ty') }
unBox (TyConApp tc tys) = do { tys' <- mapM unBox tys; return (TyConApp tc tys') }
unBox (AppTy f a) = do { f' <- unBox f; a' <- unBox a; return (mkAppTy f' a') }
unBox (FunTy f a) = do { f' <- unBox f; a' <- unBox a; return (FunTy f' a') }
, MetaTv BoxTv ref <- tcTyVarDetails tv -- NB: non-TcTyVars are possible
= do { cts <- readMutVar ref -- under nested quantifiers
; case cts of
- Flexi -> fillBoxWithTau tv ref
+ Flexi -> fillBoxWithTau tv ref
Indirect ty -> do { non_boxy_ty <- unBox ty
; if isTauTy non_boxy_ty
then return non_boxy_ty
----------------
-- If an error happens we try to figure out whether the function
-- function has been given too many or too few arguments, and say so.
-addSubCtxt SubDone actual_res_ty expected_res_ty thing_inside
- = thing_inside
-addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside
+addSubCtxt orig actual_res_ty expected_res_ty thing_inside
= addErrCtxtM mk_err thing_inside
where
mk_err tidy_env
len_act_args = length act_args
len_exp_args = length exp_args
- message = case sub_ctxt of
- SubFun fun | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun
- | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
- other -> mkExpectedActualMsg act_ty'' exp_ty''
+ message = case orig of
+ OccurrenceOf fun
+ | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun
+ | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
+ other -> mkExpectedActualMsg act_ty'' exp_ty''
; return (env2, message) }
wrongArgsCtxt too_many_or_few fun
------------------
unifyForAllCtxt tvs phi1 phi2 env
- = returnM (env2, msg)
+ = return (env2, msg)
where
(env', tvs') = tidyOpenTyVars env tvs -- NB: not tidyTyVarBndrs
(env1, phi1') = tidyOpenType env' phi1
msg = vcat [ptext SLIT("When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')),
ptext SLIT(" and") <+> quotes (ppr (mkForAllTys tvs' phi2'))]
-------------------
-unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
- -- tv1 and ty2 are zonked already
- = returnM msg
- where
- msg = (env2, ptext SLIT("When matching the kinds of") <+>
- sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
-
- (pp_expected, pp_actual) | swapped = (pp2, pp1)
- | otherwise = (pp1, pp2)
- (env1, tv1') = tidyOpenTyVar tidy_env tv1
- (env2, ty2') = tidyOpenType env1 ty2
- pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
- pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
-
+-----------------------
unifyMisMatch outer swapped ty1 ty2
- = do { (env, msg) <- if swapped then misMatchMsg ty1 ty2
- else misMatchMsg ty2 ty1
-
- -- This is the whole point of the 'outer' stuff
- ; if outer then popErrCtxt (failWithTcM (env, msg))
- else failWithTcM (env, msg)
- }
-
-misMatchMsg ty1 ty2
- = do { env0 <- tcInitTidyEnv
- ; (env1, pp1, extra1) <- ppr_ty env0 ty1
- ; (env2, pp2, extra2) <- ppr_ty env1 ty2
- ; return (env2, sep [sep [ptext SLIT("Couldn't match expected type") <+> pp1,
- nest 7 (ptext SLIT("against inferred type") <+> pp2)],
- nest 2 extra1, nest 2 extra2]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty
- = do { ty' <- zonkTcType ty
- ; let (env1,tidy_ty) = tidyOpenType env ty'
- simple_result = (env1, quotes (ppr tidy_ty), empty)
- ; case tidy_ty of
- TyVarTy tv
- | isSkolemTyVar tv || isSigTyVar tv
- -> return (env2, pp_rigid tv', pprSkolTvBinding tv')
- | otherwise -> return simple_result
- where
- (env2, tv') = tidySkolemTyVar env1 tv
- other -> return simple_result }
- where
- pp_rigid tv = quotes (ppr tv) <+> parens (ptext SLIT("a rigid variable"))
-
-
-notMonoType ty
- = do { ty' <- zonkTcType ty
- ; env0 <- tcInitTidyEnv
- ; let (env1, tidy_ty) = tidyOpenType env0 ty'
- msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
- ; failWithTcM (env1, msg) }
-
-notMonoArgs ty
- = do { ty' <- zonkTcType ty
- ; env0 <- tcInitTidyEnv
- ; let (env1, tidy_ty) = tidyOpenType env0 ty'
- msg = ptext SLIT("Arguments of synonym family must be monotypes") <+> quotes (ppr tidy_ty)
- ; failWithTcM (env1, msg) }
-
-occurCheck tyvar ty
- = do { env0 <- tcInitTidyEnv
- ; ty' <- zonkTcType ty
- ; let (env1, tidy_tyvar) = tidyOpenTyVar env0 tyvar
- (env2, tidy_ty) = tidyOpenType env1 ty'
- extra = sep [ppr tidy_tyvar, char '=', ppr tidy_ty]
- ; failWithTcM (env2, hang msg 2 extra) }
- where
- msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
+ | swapped = unifyMisMatch outer False ty2 ty1
+ | outer = popErrCtxt $ unifyMisMatch False swapped ty1 ty2 -- This is the whole point of the 'outer' stuff
+ | otherwise = failWithMisMatch ty1 ty2
\end{code}
-> TcKind -- Actual
-> TcM ()
unifyKind (TyConApp kc1 []) (TyConApp kc2 [])
- | isSubKindCon kc2 kc1 = returnM ()
+ | isSubKindCon kc2 kc1 = return ()
unifyKind (FunTy a1 r1) (FunTy a2 r2)
= do { unifyKind a2 a1; unifyKind r1 r2 }
unifyKind k1 k2 = unifyKindMisMatch k1 k2
unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
-unifyKinds [] [] = returnM ()
-unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
- unifyKinds ks1 ks2
-unifyKinds _ _ = panic "unifyKinds: length mis-match"
+unifyKinds [] [] = return ()
+unifyKinds (k1:ks1) (k2:ks2) = do unifyKind k1 k2
+ unifyKinds ks1 ks2
+unifyKinds _ _ = panic "unifyKinds: length mis-match"
----------------
uKVar :: Bool -> KindVar -> TcKind -> TcM ()
----------------
uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
uUnboundKVar swapped kv1 k2@(TyVarTy kv2)
- | kv1 == kv2 = returnM ()
+ | kv1 == kv2 = return ()
| otherwise -- Distinct kind variables
= do { mb_k2 <- readKindVar kv2
; case mb_k2 of
Indirect k2 -> uUnboundKVar swapped kv1 k2
- Flexi -> writeKindVar kv1 k2 }
+ Flexi -> writeKindVar kv1 k2 }
uUnboundKVar swapped kv1 non_var_k2
= do { k2' <- zonkTcKind non_var_k2
kindOccurCheckErr tyvar ty
= hang (ptext SLIT("Occurs check: cannot construct the infinite kind:"))
2 (sep [ppr tyvar, char '=', ppr ty])
-
-unifyKindMisMatch ty1 ty2
- = zonkTcKind ty1 `thenM` \ ty1' ->
- zonkTcKind ty2 `thenM` \ ty2' ->
- let
- msg = hang (ptext SLIT("Couldn't match kind"))
- 2 (sep [quotes (ppr ty1'),
- ptext SLIT("against"),
- quotes (ppr ty2')])
- in
- failWithTc msg
\end{code}
\begin{code}
unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
-- Like unifyFunTy, but does not fail; instead just returns Nothing
-unifyFunKind (TyVarTy kvar)
- = readKindVar kvar `thenM` \ maybe_kind ->
+unifyFunKind (TyVarTy kvar) = do
+ maybe_kind <- readKindVar kvar
case maybe_kind of
Indirect fun_kind -> unifyFunKind fun_kind
- Flexi ->
+ Flexi ->
do { arg_kind <- newKindVar
; res_kind <- newKindVar
; writeKindVar kvar (mkArrowKind arg_kind res_kind)
- ; returnM (Just (arg_kind,res_kind)) }
+ ; return (Just (arg_kind,res_kind)) }
-unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
-unifyFunKind other = returnM Nothing
+unifyFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
+unifyFunKind other = return Nothing
\end{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
- = returnM ()
- | otherwise
- = tryTc (unifyKind exp_kind act_kind) `thenM` \ (_errs, mb_r) ->
- case mb_r of {
- Just r -> returnM () ; -- Unification succeeded
- Nothing ->
+ = return ()
+ | otherwise = do
+ (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
+ case mb_r of
+ Just r -> return () ; -- Unification succeeded
+ Nothing -> do
-- So there's definitely an error
-- Now to find out what sort
- zonkTcKind exp_kind `thenM` \ exp_kind ->
- zonkTcKind act_kind `thenM` \ act_kind ->
-
- tcInitTidyEnv `thenM` \ env0 ->
- 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)]
- in
- failWithTcM (env2, err $$ more_info)
- }
+ 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}
%************************************************************************
-- Guaranteed to be skolems
-> TcM ()
check_sig_tyvars extra_tvs []
- = returnM ()
+ = return ()
check_sig_tyvars extra_tvs sig_tvs
= ASSERT( all isSkolemTyVar sig_tvs )
do { gbl_tvs <- tcGetGlobalTyVars
text "extra_tvs" <+> ppr extra_tvs]))
; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
- ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
- (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
+ ; when (any (`elemVarSet` env_tvs) sig_tvs)
+ (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
}
bleatEscapedTvs :: TcTyVarSet -- The global tvs
| not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
| otherwise
= do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
- ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
+ ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
-----------------------
escape_msg sig_tv zonked_tv globs
\begin{code}
sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
-> TidyEnv -> TcM (TidyEnv, Message)
-sigCtxt id sig_tvs sig_theta sig_tau tidy_env
- = zonkTcType sig_tau `thenM` \ actual_tau ->
+sigCtxt id sig_tvs sig_theta sig_tau tidy_env = do
+ actual_tau <- zonkTcType sig_tau
let
(env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
(env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
]
msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),
nest 2 sub_msg]
- in
- returnM (env3, msg)
+
+ return (env3, msg)
\end{code}