%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
-\section{Type subsumption and unification}
+
+Type subsumption and unification
\begin{code}
module TcUnify (
--------------------------------
-- Holes
- tcInfer, subFunTys, unBox, stripBoxyType, withBox,
+ tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox,
boxyUnify, boxyUnifyList, zapToMonotype,
boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
wrapFunResCoercion
#include "HsVersions.h"
-import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) )
-import TypeRep ( Type(..), PredType(..) )
-
-import TcMType ( lookupTcTyVar, LookupTyVarResult(..),
- tcInstSkolType, tcInstBoxyTyVar, newKindVar, newMetaTyVar,
- newBoxyTyVar, newBoxyTyVarTys, readFilledBox,
- readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy,
- tcInstSkolTyVars, tcInstTyVar,
- zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
- readKindVar, writeKindVar )
-import TcSimplify ( tcSimplifyCheck )
-import TcEnv ( tcGetGlobalTyVars, findGlobals )
-import TcIface ( checkWiredInTyCon )
+import HsSyn
+import TypeRep
+
+import TcMType
+import TcSimplify
+import TcEnv
+import TcIface
import TcRnMonad -- TcType, amongst others
-import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType,
- BoxySigmaType, BoxyRhoType, BoxyType,
- TcTyVarSet, TcThetaType, TcTyVarDetails(..), BoxInfo(..),
- SkolemInfo( GenSkol, UnkSkol ), MetaDetails(..), isImmutableTyVar,
- pprSkolTvBinding, isTauTy, isTauTyCon, isSigmaTy,
- mkFunTy, mkFunTys, mkTyConApp, isMetaTyVar,
- tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys,
- tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
- typeKind, mkForAllTys, mkAppTy, isBoxyTyVar,
- tcView, exactTyVarsOfType,
- tidyOpenType, tidyOpenTyVar, tidyOpenTyVars,
- pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar,
- TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst,
- substTy, substTheta,
- lookupTyVar, extendTvSubst )
-import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
- openTypeKind, liftedTypeKind, unliftedTypeKind,
- mkArrowKind, defaultKind,
- isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
- isSubKind, pprKind, splitKindFunTys )
-import TysPrim ( alphaTy, betaTy )
-import Inst ( newDicts, instToId )
-import TyCon ( TyCon, tyConArity, tyConTyVars, isSynTyCon )
-import TysWiredIn ( listTyCon )
-import Id ( Id, mkSysLocal )
-import Var ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails )
+import TcType
+import Type
+import TysPrim
+import Inst
+import TyCon
+import TysWiredIn
+import Var
import VarSet
import VarEnv
-import Name ( Name, isSystemName )
-import ErrUtils ( Message )
-import Maybes ( expectJust, isNothing )
-import BasicTypes ( Arity )
-import UniqSupply ( uniqsFromSupply )
-import Util ( notNull, equalLength )
+import Name
+import ErrUtils
+import Maybes
+import BasicTypes
+import Util
import Outputable
-
--- Assertion imports
-#ifdef DEBUG
-import TcType ( isBoxyTy, isFlexi )
-#endif
\end{code}
%************************************************************************
; res <- tc_infer (mkTyVarTy box)
; res_ty <- readFilledBox box -- Guaranteed filled-in by now
; return (res, res_ty) }
-\end{code}
+\end{code}
%************************************************************************
-> Arity -- Expected # of args
-> BoxyRhoType -- res_ty
-> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
- -> TcM (ExprCoFn, a)
+ -> TcM (HsWrapper, a)
-- Attempt to decompse res_ty to have enough top-level arrows to
-- match the number of patterns in the match group
--
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
- = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ res_ty' ->
+ = 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) }
loop 0 args_so_far res_ty
= do { res <- thing_inside (reverse args_so_far) res_ty
- ; return (idCoercion, res) }
+ ; return (idHsWrapper, res) }
loop n args_so_far (FunTy arg_ty res_ty)
= do { (co_fn, res) <- loop (n-1) (arg_ty:args_so_far) res_ty
else loop n args_so_far (FunTy arg_ty' res_ty') }
loop n args_so_far (TyVarTy tv)
- | not (isImmutableTyVar 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 (idCoercion, res) } }
+ ; return (idHsWrapper, res) } }
where
mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
mk_res_ty [] = panic "TcUnify.mk_res_ty1"
= loop (n_req - 1) (arg:args_so_far) fun
loop n_req args_so_far (TyVarTy tv)
- | not (isImmutableTyVar tv)
+ | isTyConableTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> loop n_req args_so_far ty
= return (fun_ty, arg_ty)
loop (TyVarTy tv)
- | not (isImmutableTyVar tv)
+ | isTyConableTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> loop ty
go (TyVarTy tv) b_ty
| tv `elemVarSet` tmpl_tvs -- Template type variable in the template
- , not (intersectsVarSet boxy_tvs (tyVarsOfType orig_boxy_ty))
+ , boxy_tvs `disjointVarSet` tyVarsOfType orig_boxy_ty
, typeKind b_ty `isSubKind` tyVarKind tv -- See Note [Matching kinds]
= extendTvSubst subst tv boxy_ty'
| otherwise
\begin{code}
-----------------
-tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
+tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
-- (tcSub act exp) checks that
-- act <= exp
tcSubExp 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 foarall a. a->a with forall a. a->a"
- -- So instead I'm adding it when moving from tc_sub to u_tys
- tc_sub Nothing actual_ty actual_ty False expected_ty expected_ty
-
-tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
+ -- messages, such as "can't match forall a. a->a with forall a. a->a"
+ -- Example is tcfail165:
+ -- do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
+ -- putMVar var (show :: forall a. Show a => a -> String)
+ -- Here the info does not flow from the 'var' arg of putMVar to its 'show' arg
+ -- but after zonking it looks as if it does!
+ --
+ -- 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
+
+tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
tcFunResTy fun actual_ty expected_ty
- = tc_sub (Just fun) actual_ty actual_ty False expected_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
-----------------
-tc_sub :: Maybe Name -- Just fun => we're looking at a function result type
+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
-> BoxySigmaType -- actual_ty, before expanding synonyms
-> BoxySigmaType -- ..and after
-> InBox -- True <=> expected_ty is inside a box
-> BoxySigmaType -- expected_ty, before
-> BoxySigmaType -- ..and after
- -> TcM ExprCoFn
+ -> TcM HsWrapper
-- The acual_ty is never inside a box
-- IMPORTANT pre-condition: if the args contain foralls, the bound type
-- variables are visible non-monadically
-- 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 mb_fun act_sty act_ty exp_ib exp_sty exp_ty
- = tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty
+tc_sub sub_ctxt 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
-- This indirection is just here to make
-- it easy to insert a debug trace!
-tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty
- | Just exp_ty' <- tcView exp_ty = tc_sub mb_fun act_sty act_ty exp_ib exp_sty exp_ty'
-tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty
- | Just act_ty' <- tcView act_ty = tc_sub mb_fun 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 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
-----------------------------------
-- 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 mb_fun act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
- = do { addErrCtxtM (subCtxt mb_fun act_sty exp_sty) $
+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 idCoercion }
+ ; return idHsWrapper }
-----------------------------------
-- Skolemisation case (rule SKOL)
-- g :: Ord b => b->b
-- Consider f g !
-tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty
- | not exp_ib, -- SKOL does not apply if exp_ty is inside a box
- isSigmaTy exp_ty
- = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty ->
- tc_sub mb_fun act_sty act_ty False body_exp_ty body_exp_ty
+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
+ 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
; return (gen_fn <.> co_fn) }
where
act_tvs = tyVarsOfType act_ty
-- expected_ty: Int -> Int
-- co_fn e = e Int dOrdInt
-tc_sub1 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty
+tc_sub1 sub_ctxt 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.)
; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty,
ppr tyvars <+> ppr theta <+> ppr tau,
ppr tau'])
- ; co_fn <- tc_sub mb_fun tau' tau' exp_ib exp_sty expected_ty
+ ; co_fn2 <- tc_sub sub_ctxt tau' tau' exp_ib exp_sty expected_ty
-- Deal with the dictionaries
- ; dicts <- newDicts InstSigOrigin (substTheta subst' theta)
- ; extendLIEs dicts
- ; let inst_fn = CoApps (CoTyApps CoHole inst_tys)
- (map instToId dicts)
- ; return (co_fn <.> inst_fn) }
+ -- 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 mb_fun _ (FunTy act_arg act_res) exp_ib _ (FunTy exp_arg exp_res)
- = tc_sub_funs mb_fun act_arg act_res exp_ib exp_arg exp_res
+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
-- Function case (rule F2)
-tc_sub1 mb_fun act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
+tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
| isBoxyTyVar exp_tv
- = do { cts <- readMetaTyVar exp_tv
+ = addSubCtxt sub_ctxt act_sty exp_sty $
+ do { cts <- readMetaTyVar exp_tv
; case cts of
- Indirect ty -> tc_sub mb_fun act_sty act_ty True exp_sty ty
+ 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 mb_fun act_arg act_res True arg_ty res_ty } }
+ ; tc_sub_funs 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 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty
- = do { addErrCtxtM (subCtxt mb_fun act_sty exp_sty) $
- u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty
- ; return idCoercion }
+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
+-----------------------------------
+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 True False act_sty actual_ty exp_ib exp_sty expected_ty
+ ; return idHsWrapper }
-----------------------------------
-tc_sub_funs mb_fun act_arg act_res exp_ib exp_arg exp_res
+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 mb_fun act_res act_res exp_ib exp_res exp_res
+ ; co_fn_res <- tc_sub SubDone act_res act_res exp_ib exp_res exp_res
; wrapFunResCoercion [exp_arg] co_fn_res }
-----------------------------------
wrapFunResCoercion
:: [TcType] -- Type of args
- -> ExprCoFn -- HsExpr a -> HsExpr b
- -> TcM ExprCoFn -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
+ -> HsWrapper -- HsExpr a -> HsExpr b
+ -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
wrapFunResCoercion arg_tys co_fn_res
- | isIdCoercion co_fn_res = return idCoercion
+ | isIdHsWrapper co_fn_res = return idHsWrapper
| null arg_tys = return co_fn_res
| otherwise
- = do { us <- newUniqueSupply
- ; let arg_ids = zipWith (mkSysLocal FSLIT("sub")) (uniqsFromSupply us) arg_tys
- ; return (CoLams arg_ids (co_fn_res <.> (CoApps CoHole arg_ids))) }
+ = do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys
+ ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) }
\end{code}
-> TcTyVarSet -- Extra tyvars that the universally
-- quantified tyvars of expected_ty
-- must not be unified
- -> (BoxyRhoType -> TcM result) -- spec_ty
- -> TcM (ExprCoFn, result)
+ -> ([TcTyVar] -> BoxyRhoType -> TcM result)
+ -> TcM (HsWrapper, result)
-- The expression has type: spec_ty -> expected_ty
tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
-- 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
- ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
+ ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
- ; span <- getSrcSpanM
- ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
+ -- Get loation from monad, not from expected_ty
+ ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
; return ((forall_tvs, theta, rho_ty), skol_info) })
#ifdef DEBUG
; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
text "expected_ty" <+> ppr expected_ty,
- text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
- text "free_tvs" <+> ppr free_tvs,
- text "forall_tvs" <+> ppr forall_tvs])
+ text "inst ty" <+> ppr tvs' <+> ppr theta' <+> ppr rho',
+ text "free_tvs" <+> ppr free_tvs])
#endif
-- Type-check the arg and unify with poly type
- ; (result, lie) <- getLIE (thing_inside rho_ty)
+ ; (result, lie) <- getLIE (thing_inside tvs' rho')
-- Check that the "forall_tvs" havn't been constrained
-- The interesting bit here is that we must include the free variables
-- Conclusion: include the free vars of the expected_ty in the
-- list of "free vars" for the signature check.
- ; dicts <- newDicts (SigOrigin skol_info) theta
- ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
+ ; loc <- getInstLoc (SigOrigin skol_info)
+ ; dicts <- newDictBndrs loc theta'
+ ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
- ; checkSigTyVarsWrt free_tvs forall_tvs
+ ; checkSigTyVarsWrt free_tvs tvs'
; traceTc (text "tcGen:done")
; let
- -- This HsLet binds any Insts which came out of the simplification.
- -- It's a bit out of place here, but using AbsBind involves inventing
- -- a couple of new names which seems worse.
- dict_ids = map instToId dicts
- co_fn = CoTyLams forall_tvs $ CoLams dict_ids $ CoLet inst_binds CoHole
+ -- 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) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
- sig_msg = ptext SLIT("expected type of an expression")
\end{code}
-- Acutal and expected types
unifyTheta theta1 theta2
= do { checkTc (equalLength theta1 theta2)
- (ptext SLIT("Contexts differ in length"))
+ (vcat [ptext SLIT("Contexts differ in length"),
+ nest 2 $ parens $ ptext SLIT("Use -fglasgow-exts to allow this")])
; uList unifyPred theta1 theta2 }
---------------
:: InBox -> TcType -- ty1 is the *expected* type
-> InBox -> TcType -- ty2 is the *actual* type
-> TcM ()
-uTysOuter nb1 ty1 nb2 ty2 = u_tys True nb1 ty1 ty1 nb2 ty2 ty2
-uTys nb1 ty1 nb2 ty2 = u_tys False nb1 ty1 ty1 nb2 ty2 ty2
+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 }
--------------
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
-- "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
+ | isSigmaTy ty1 || isSigmaTy ty2
+ = do { checkM (equalLength tvs1 tvs2)
+ (unifyMisMatch outer False orig_ty1 orig_ty2)
+
+ ; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
+ -- Get location from monad, not from tvs1
+ ; let tys = mkTyVarTys tvs
+ in_scope = mkInScopeSet (mkVarSet tvs)
+ phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
+ phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
+ (theta1,tau1) = tcSplitPhiTy phi1
+ (theta2,tau2) = tcSplitPhiTy phi2
+
+ ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
+ { checkM (equalLength theta1 theta2)
+ (unifyMisMatch outer False orig_ty1 orig_ty2)
+
+ ; uPreds False nb1 theta1 nb2 theta2
+ ; 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)
+ (bleatEscapedTvs free_tvs tvs tvs)
+
+ -- If both sides are inside a box, we are in a "box-meets-box"
+ -- situation, and we should not have a polytype at all.
+ -- If we get here we have two boxes, already filled with
+ -- 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)
+ }}
+ where
+ (tvs1, body1) = tcSplitForAllTys ty1
+ (tvs2, body2) = tcSplitForAllTys ty2
+
-- Predicates
- go outer (PredTy p1) (PredTy p2) = uPred outer nb1 p1 nb2 p2
+ go outer (PredTy p1) (PredTy p2) = uPred False nb1 p1 nb2 p2
-- Type constructors must match
go _ (TyConApp con1 tys1) (TyConApp con2 tys2)
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
= do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
- go _ ty1@(ForAllTy _ _) ty2@(ForAllTy _ _)
- | length tvs1 == length tvs2
- = do { tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
- ; let tys = mkTyVarTys tvs
- in_scope = mkInScopeSet (mkVarSet tvs)
- subst1 = mkTvSubst in_scope (zipTyEnv tvs1 tys)
- subst2 = mkTvSubst in_scope (zipTyEnv tvs2 tys)
- ; uTys nb1 (substTy subst1 body1) nb2 (substTy subst2 body2)
-
- -- If both sides are inside a box, we are in a "box-meets-box"
- -- situation, and we should not have a polytype at all.
- -- If we get here we have two boxes, already filled with
- -- 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)
- }
- where
- (tvs1, body1) = tcSplitForAllTys ty1
- (tvs2, body2) = tcSplitForAllTys ty2
-- Anything else fails
go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
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
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 ps1 nb2 ps2 = panic "uPreds"
\end{code}
Note [Tycon app]
| otherwise = brackets (equals <+> ppr ty2)
; traceTc (text "uVar" <+> ppr swapped <+>
sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ),
- nest 2 (ptext SLIT(" :=: ")),
+ nest 2 (ptext SLIT(" <-> ")),
ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion])
; details <- lookupTcTyVar tv1
; case details of
k1_sub_k2 = k1 `isSubKind` k2
k2_sub_k1 = k2 `isSubKind` k1
- nicer_to_update_tv1 = isSystemName (varName tv1)
+ nicer_to_update_tv1 = isSystemName (Var.varName tv1)
-- Try to update sys-y type variables in preference to ones
-- gotten (say) by instantiating a polymorphic function with
-- a user-written type sig
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)
; case mb_tys' of
Just tys' -> return (TyConApp tc tys')
-- Retain the synonym (the common case)
- Nothing -> go (expectJust "checkTauTvUpdate"
+ 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
}
Rather, we should bind t to () (= non_var_ty2).
\begin{code}
-stripBoxyType :: BoxyType -> TcM TcType
--- Strip all boxes from the input type, returning a non-boxy type.
--- It's fine for there to be a polytype inside a box (c.f. unBox)
--- All of the boxes should have been filled in by now;
--- hence we return a TcType
-stripBoxyType ty = zonkType strip_tv ty
- where
- strip_tv tv = ASSERT( not (isBoxyTyVar tv) ) return (TyVarTy tv)
- -- strip_tv will be called for *Flexi* meta-tyvars
- -- There should not be any Boxy ones; hence the ASSERT
+refineBox :: TcType -> TcM TcType
+-- Unbox the outer box of a boxy type (if any)
+refineBox ty@(TyVarTy box_tv)
+ | isMetaTyVar box_tv
+ = do { cts <- readMetaTyVar box_tv
+ ; case cts of
+ Flexi -> return ty
+ Indirect ty -> return ty }
+refineBox other_ty = return other_ty
+
+refineBoxToTau :: TcType -> TcM TcType
+-- Unbox the outer box of a boxy type, filling with a monotype if it is empty
+-- Like refineBox except for the "fill with monotype" part.
+refineBoxToTau ty@(TyVarTy box_tv)
+ | isMetaTyVar box_tv
+ , MetaTv BoxTv ref <- tcTyVarDetails box_tv
+ = do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> fillBoxWithTau box_tv ref
+ Indirect ty -> return ty }
+refineBoxToTau other_ty = return other_ty
zapToMonotype :: BoxySigmaType -> TcM TcTauType
-- Subtle... we must zap the boxy res_ty
unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') }
unBoxPred (IParam ip ty) = do { ty' <- unBox ty; return (IParam ip ty') }
+unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') }
\end{code}
----------------
-- 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.
-subCtxt mb_fun actual_res_ty expected_res_ty tidy_env
- = do { exp_ty' <- zonkTcType expected_res_ty
- ; act_ty' <- zonkTcType actual_res_ty
- ; let
- (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
- (env2, act_ty'') = tidyOpenType env1 act_ty'
- (exp_args, _) = tcSplitFunTys exp_ty''
- (act_args, _) = tcSplitFunTys act_ty''
+addSubCtxt SubDone actual_res_ty expected_res_ty thing_inside
+ = thing_inside
+addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside
+ = addErrCtxtM mk_err thing_inside
+ where
+ mk_err tidy_env
+ = do { exp_ty' <- zonkTcType expected_res_ty
+ ; act_ty' <- zonkTcType actual_res_ty
+ ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
+ (env2, act_ty'') = tidyOpenType env1 act_ty'
+ (exp_args, _) = tcSplitFunTys exp_ty''
+ (act_args, _) = tcSplitFunTys act_ty''
- len_act_args = length act_args
- len_exp_args = length exp_args
+ len_act_args = length act_args
+ len_exp_args = length exp_args
- message = case mb_fun of
- Just 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) }
+ 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''
+ ; return (env2, message) }
- where
wrongArgsCtxt too_many_or_few fun
= ptext SLIT("Probable cause:") <+> quotes (ppr fun)
<+> ptext SLIT("is applied to") <+> text too_many_or_few
<+> ptext SLIT("arguments")
------------------
+unifyForAllCtxt tvs phi1 phi2 env
+ = returnM (env2, msg)
+ where
+ (env', tvs') = tidyOpenTyVars env tvs -- NB: not tidyTyVarBndrs
+ (env1, phi1') = tidyOpenType env' phi1
+ (env2, phi2') = tidyOpenType env1 phi2
+ 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
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
unifyKind :: TcKind -- Expected
-> TcKind -- Actual
-> TcM ()
-unifyKind LiftedTypeKind LiftedTypeKind = returnM ()
-unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
-
-unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
-unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM ()
- -- Respect sub-kinding
+unifyKind (TyConApp kc1 []) (TyConApp kc2 [])
+ | isSubKindCon kc2 kc1 = returnM ()
-unifyKind (FunKind a1 r1) (FunKind a2 r2)
- = do { unifyKind a2 a1; unifyKind r1 r2 }
+unifyKind (FunTy a1 r1) (FunTy a2 r2)
+ = do { unifyKind a2 a1; unifyKind r1 r2 }
-- Notice the flip in the argument,
-- so that the sub-kinding works right
-
-unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
-unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
+unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2
+unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1
unifyKind k1 k2 = unifyKindMisMatch k1 k2
unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
uKVar swapped kv1 k2
= do { mb_k1 <- readKindVar kv1
; case mb_k1 of
- Nothing -> uUnboundKVar swapped kv1 k2
- Just k1 | swapped -> unifyKind k2 k1
- | otherwise -> unifyKind k1 k2 }
+ Flexi -> uUnboundKVar swapped kv1 k2
+ Indirect k1 | swapped -> unifyKind k2 k1
+ | otherwise -> unifyKind k1 k2 }
----------------
uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
-uUnboundKVar swapped kv1 k2@(KindVar kv2)
+uUnboundKVar swapped kv1 k2@(TyVarTy kv2)
| kv1 == kv2 = returnM ()
| otherwise -- Distinct kind variables
= do { mb_k2 <- readKindVar kv2
; case mb_k2 of
- Just k2 -> uUnboundKVar swapped kv1 k2
- Nothing -> writeKindVar kv1 k2 }
+ Indirect k2 -> uUnboundKVar swapped kv1 k2
+ Flexi -> writeKindVar kv1 k2 }
uUnboundKVar swapped kv1 non_var_k2
= do { k2' <- zonkTcKind non_var_k2
kindOccurCheck kv1 k2 -- k2 is zonked
= checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
where
- not_in (KindVar kv2) = kv1 /= kv2
- not_in (FunKind a2 r2) = not_in a2 && not_in r2
- not_in other = True
+ not_in (TyVarTy kv2) = kv1 /= kv2
+ not_in (FunTy a2 r2) = not_in a2 && not_in r2
+ not_in other = True
kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
-- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
kindSimpleKind orig_swapped orig_kind
= go orig_swapped orig_kind
where
- go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
- ; k2' <- go sw k2
- ; return (FunKind k1' k2') }
- go True OpenTypeKind = return liftedTypeKind
- go True ArgTypeKind = return liftedTypeKind
- go sw LiftedTypeKind = return liftedTypeKind
- go sw UnliftedTypeKind = return unliftedTypeKind
- go sw k@(KindVar _) = return k -- KindVars are always simple
+ go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1
+ ; k2' <- go sw k2
+ ; return (mkArrowKind k1' k2') }
+ go True k
+ | isOpenTypeKind k = return liftedTypeKind
+ | isArgTypeKind k = return liftedTypeKind
+ go sw k
+ | isLiftedTypeKind k = return liftedTypeKind
+ | isUnliftedTypeKind k = return unliftedTypeKind
+ go sw k@(TyVarTy _) = return k -- KindVars are always simple
go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
<+> ppr orig_swapped <+> ppr orig_kind)
-- I think this can't actually happen
unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
-- Like unifyFunTy, but does not fail; instead just returns Nothing
-unifyFunKind (KindVar kvar)
- = readKindVar kvar `thenM` \ maybe_kind ->
+unifyFunKind (TyVarTy kvar)
+ = readKindVar kvar `thenM` \ maybe_kind ->
case maybe_kind of
- Just fun_kind -> unifyFunKind fun_kind
- Nothing -> do { arg_kind <- newKindVar
- ; res_kind <- newKindVar
- ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
- ; returnM (Just (arg_kind,res_kind)) }
+ Indirect fun_kind -> unifyFunKind fun_kind
+ Flexi ->
+ do { arg_kind <- newKindVar
+ ; res_kind <- newKindVar
+ ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
+ ; returnM (Just (arg_kind,res_kind)) }
-unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
-unifyFunKind other = returnM Nothing
+unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
+unifyFunKind other = returnM Nothing
\end{code}
%************************************************************************