unifyType, unifyTypeList, unifyTheta,
unifyKind, unifyKinds, unifyFunKind,
checkExpectedKind,
- boxySubMatchType, boxyMatchTypes,
+ preSubType, boxyMatchTypes,
--------------------------------
-- Holes
import TypeRep ( Type(..), PredType(..) )
import TcMType ( lookupTcTyVar, LookupTyVarResult(..),
- tcInstSkolType, newKindVar, newMetaTyVar,
- tcInstBoxy, newBoxyTyVar, newBoxyTyVarTys, readFilledBox,
+ tcInstSkolType, tcInstBoxyTyVar, newKindVar, newMetaTyVar,
+ newBoxyTyVar, newBoxyTyVarTys, readFilledBox,
readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy,
tcInstSkolTyVars, tcInstTyVar,
zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
pprSkolTvBinding, isTauTy, isTauTyCon, isSigmaTy,
mkFunTy, mkFunTys, mkTyConApp, isMetaTyVar,
tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys,
- tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
+ tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
typeKind, mkForAllTys, mkAppTy, isBoxyTyVar,
+ exactTyVarsOfType,
tidyOpenType, tidyOpenTyVar, tidyOpenTyVars,
pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView,
- TvSubst, mkTvSubst, zipTyEnv, substTy, emptyTvSubst,
+ TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst,
+ substTy, substTheta,
lookupTyVar, extendTvSubst )
import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
openTypeKind, liftedTypeKind, unliftedTypeKind,
import TysWiredIn ( listTyCon )
import Id ( Id, mkSysLocal )
import Var ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails )
-import VarSet ( emptyVarSet, mkVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems,
- extendVarSet, intersectsVarSet )
+import VarSet
import VarEnv
import Name ( Name, isSystemName )
import ErrUtils ( Message )
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 res_ty
+ ; if isNothing mb_unit then bale_out args_so_far
else loop n args_so_far (FunTy arg_ty' res_ty') }
loop n args_so_far (TyVarTy tv)
-- Note argTypeKind: the args can have an unboxed type,
-- but not an unboxed tuple.
- loop n args_so_far res_ty = bale_out args_so_far res_ty
+ loop n args_so_far res_ty = bale_out args_so_far
- bale_out args_so_far res_ty
+ bale_out args_so_far
= do { env0 <- tcInitTidyEnv
; res_ty' <- zonkTcType res_ty
; let (env1, res_ty'') = tidyOpenType env0 res_ty'
%************************************************************************
\begin{code}
+preSubType :: [TcTyVar] -- Quantified type variables
+ -> TcTyVarSet -- Subset of quantified type variables
+ -- that can be instantiated with boxy types
+ -> TcType -- The rho-type part; quantified tyvars scopes over this
+ -> BoxySigmaType -- Matching type from the context
+ -> TcM [TcType] -- Types to instantiate the tyvars
+-- Perform pre-subsumption, and return suitable types
+-- to instantiate the quantified type varibles:
+-- info from the pre-subsumption, if there is any
+-- a boxy type variable otherwise
+--
+-- The 'btvs' are a subset of 'qtvs'. They are the ones we can
+-- instantiate to a boxy type variable, because they'll definitely be
+-- filled in later. This isn't always the case; sometimes we have type
+-- variables mentioned in the context of the type, but not the body;
+-- f :: forall a b. C a b => a -> a
+-- Then we may land up with an unconstrained 'b', so we want to
+-- instantiate it to a monotype (non-boxy) type variable
+
+preSubType qtvs btvs qty expected_ty
+ = do { tys <- mapM inst_tv qtvs
+ ; traceTc (text "preSubType" <+> (ppr qtvs $$ ppr btvs $$ ppr qty $$ ppr expected_ty $$ ppr pre_subst $$ ppr tys))
+ ; return tys }
+ where
+ pre_subst = boxySubMatchType (mkVarSet qtvs) qty expected_ty
+ inst_tv tv
+ | Just boxy_ty <- lookupTyVar pre_subst tv = return boxy_ty
+ | tv `elemVarSet` btvs = do { tv' <- tcInstBoxyTyVar tv
+ ; return (mkTyVarTy tv') }
+ | otherwise = do { tv' <- tcInstTyVar tv
+ ; return (mkTyVarTy tv') }
+
boxySubMatchType
:: TcTyVarSet -> TcType -- The "template"; the tyvars are skolems
-> BoxyRhoType -- Type to match (note a *Rho* type)
-> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
+-- boxySubMatchType implements the Pre-subsumption judgement, in Fig 5 of the paper
+-- "Boxy types: inference for higher rank types and impredicativity"
+
+boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
+ = go tmpl_tvs tmpl_ty emptyVarSet boxy_ty
+ where
+ go t_tvs t_ty b_tvs b_ty
+ | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
+ | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
+
+ go t_tvs (TyVarTy _) b_tvs b_ty = emptyTvSubst -- Rule S-ANY; no bindings
+ -- Rule S-ANY covers (a) type variables and (b) boxy types
+ -- in the template. Both look like a TyVarTy.
+ -- See Note [Sub-match] below
+
+ go t_tvs t_ty b_tvs b_ty
+ | isSigmaTy t_ty, (tvs, _, t_tau) <- tcSplitSigmaTy t_ty
+ = go (t_tvs `delVarSetList` tvs) t_tau b_tvs b_ty -- Rule S-SPEC
+ -- Under a forall on the left, if there is shadowing,
+ -- do not bind! Hence the delVarSetList.
+ | isSigmaTy b_ty, (tvs, _, b_tau) <- tcSplitSigmaTy b_ty
+ = go t_tvs t_ty (extendVarSetList b_tvs tvs) b_tau -- Rule S-SKOL
+ -- Add to the variables we must not bind to
+ -- NB: it's *important* to discard the theta part. Otherwise
+ -- consider (forall a. Eq a => a -> b) ~<~ (Int -> Int -> Bool)
+ -- and end up with a completely bogus binding (b |-> Bool), by lining
+ -- up the (Eq a) with the Int, whereas it should be (b |-> (Int->Bool)).
+ -- This pre-subsumption stuff can return too few bindings, but it
+ -- must *never* return bogus info.
+
+ go t_tvs (FunTy arg1 res1) b_tvs (FunTy arg2 res2) -- Rule S-FUN
+ = boxy_match t_tvs arg1 b_tvs arg2 (go t_tvs res1 b_tvs res2)
+ -- Match the args, and sub-match the results
+
+ go t_tvs t_ty b_tvs b_ty = boxy_match t_tvs t_ty b_tvs b_ty emptyTvSubst
+ -- Otherwise defer to boxy matching
+ -- This covers TyConApp, AppTy, PredTy
+\end{code}
+
+Note [Sub-match]
+~~~~~~~~~~~~~~~~
+Consider this
+ head :: [a] -> a
+ |- head xs : <rhobox>
+We will do a boxySubMatchType between a ~ <rhobox>
+But we *don't* want to match [a |-> <rhobox>] because
+ (a) The box should be filled in with a rho-type, but
+ but the returned substitution maps TyVars to boxy
+ *sigma* types
+ (b) In any case, the right final answer might be *either*
+ instantiate 'a' with a rho-type or a sigma type
+ head xs : Int vs head xs : forall b. b->b
+So the matcher MUST NOT make a choice here. In general, we only
+bind a template type variable in boxyMatchType, not in boxySubMatchType.
+
+
+\begin{code}
boxyMatchTypes
:: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems
-> [BoxySigmaType] -- Type to match
-> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
+-- boxyMatchTypes implements the Pre-matching judgement, in Fig 5 of the paper
+-- "Boxy types: inference for higher rank types and impredicativity"
+
-- Find a *boxy* substitution that makes the template look as much
-- like the BoxySigmaType as possible.
-- It's always ok to return an empty substitution;
-- NB1: This is a pure, non-monadic function.
-- It does no unification, and cannot fail
--
--- Note [Matching kinds]
--- The target type might legitimately not be a sub-kind of template.
--- For example, suppose the target is simply a box with an OpenTypeKind,
--- and the template is a type variable with LiftedTypeKind.
--- Then it's ok (because the target type will later be refined).
--- We simply don't bind the template type variable.
---
--- It might also be that the kind mis-match is an error. For example,
--- suppose we match the template (a -> Int) against (Int# -> Int),
--- where the template type variable 'a' has LiftedTypeKind. This
--- matching function does not fail; it simply doesn't bind the template.
--- Later stuff will fail.
---
-- Precondition: the arg lengths are equal
--- Precondition: none of the template type variables appear in the [BoxySigmaType]
--- Precondition: any nested quantifiers in either type differ from
--- the template type variables passed as arguments
+-- Precondition: none of the template type variables appear anywhere in the [BoxySigmaType]
--
--- Note [Sub-match]
--- ~~~~~~~~~~~~~~~~
--- Consider this
--- head :: [a] -> a
--- |- head xs : <rhobox>
--- We will do a boxySubMatchType between a ~ <rhobox>
--- But we *don't* want to match [a |-> <rhobox>] because
--- (a) The box should be filled in with a rho-type, but
--- but the returned substitution maps TyVars to boxy *sigma*
--- types
--- (b) In any case, the right final answer might be *either*
--- instantiate 'a' with a rho-type or a sigma type
--- head xs : Int vs head xs : forall b. b->b
--- So the matcher MUST NOT make a choice here. In general, we only
--- bind a template type variable in boxyMatchType, not in boxySubMatchType.
-boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
- = go tmpl_ty boxy_ty
- where
- go t_ty b_ty
- | Just t_ty' <- tcView t_ty = go t_ty' b_ty
- | Just b_ty' <- tcView b_ty = go t_ty b_ty'
-
- go (FunTy arg1 res1) (FunTy arg2 res2)
- = do_match arg1 arg2 (go res1 res2)
- -- Match the args, and sub-match the results
-
- go (TyVarTy _) b_ty = emptyTvSubst -- Do not bind! See Note [Sub-match]
-
- go t_ty b_ty = do_match t_ty b_ty emptyTvSubst -- Otherwise we are safe to bind
-
- do_match t_ty b_ty subst = boxy_match tmpl_tvs t_ty emptyVarSet b_ty subst
-
------------
boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
= ASSERT( length tmpl_tys == length boxy_tys )
boxy_match_s tmpl_tvs [] boxy_tvs [] subst
= subst
boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
- = boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys $
- boxy_match tmpl_tvs t_ty boxy_tvs b_ty subst
+ = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $
+ boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst
+
------------
boxy_match :: TcTyVarSet -> TcType -- Template
| Just t_ty' <- tcView t_ty = go t_ty' b_ty
| Just b_ty' <- tcView b_ty = go t_ty b_ty'
- go (ForAllTy _ ty1) (ForAllTy tv2 ty2)
- = boxy_match tmpl_tvs ty1 (boxy_tvs `extendVarSet` tv2) ty2 subst
+ go ty1 ty2 -- C.f. the isSigmaTy case for boxySubMatchType
+ | isSigmaTy ty1
+ , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
+ , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
+ , equalLength tvs1 tvs2
+ = boxy_match (tmpl_tvs `delVarSetList` tvs1) tau1
+ (boxy_tvs `extendVarSetList` tvs2) tau2 subst
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2 = go_s tys1 tys2
go (TyVarTy tv) b_ty
| tv `elemVarSet` tmpl_tvs -- Template type variable in the template
, not (intersectsVarSet boxy_tvs (tyVarsOfType orig_boxy_ty))
- , typeKind b_ty `isSubKind` tyVarKind tv
+ , typeKind b_ty `isSubKind` tyVarKind tv -- See Note [Matching kinds]
= extendTvSubst subst tv boxy_ty'
+ | otherwise
+ = subst -- Ignore others
where
boxy_ty' = case lookupTyVar subst tv of
Nothing -> orig_boxy_ty
Just ty -> ty `boxyLub` orig_boxy_ty
- go _ _ = subst -- Always safe
+ go _ _ = emptyTvSubst -- It's important to *fail* by returning the empty substitution
+ -- Example: Tree a ~ Maybe Int
+ -- We do not want to bind (a |-> Int) in pre-matching, because that can give very
+ -- misleading error messages. An even more confusing case is
+ -- a -> b ~ Maybe Int
+ -- Then we do not want to bind (b |-> Int)! It's always safe to discard bindings
+ -- from this pre-matching phase.
--------
go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst
= TyConApp tc1 (zipWith boxyLub ts1 ts2)
go (TyVarTy tv1) ty2 -- This is the whole point;
- | isTcTyVar tv1, isMetaTyVar tv1 -- choose ty2 if ty2 is a box
- = ty2
+ | isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box
+ = orig_ty2
-- Look inside type synonyms, but only if the naive version fails
go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
go ty1 ty2 = orig_ty1 -- Default
\end{code}
+Note [Matching kinds]
+~~~~~~~~~~~~~~~~~~~~~
+The target type might legitimately not be a sub-kind of template.
+For example, suppose the target is simply a box with an OpenTypeKind,
+and the template is a type variable with LiftedTypeKind.
+Then it's ok (because the target type will later be refined).
+We simply don't bind the template type variable.
+
+It might also be that the kind mis-match is an error. For example,
+suppose we match the template (a -> Int) against (Int# -> Int),
+where the template type variable 'a' has LiftedTypeKind. This
+matching function does not fail; it simply doesn't bind the template.
+Later stuff will fail.
%************************************************************************
%* *
; return (gen_fn <.> co_fn) }
where
act_tvs = tyVarsOfType act_ty
- -- It's really important to check for escape wrt the free vars of
- -- both expected_ty *and* actual_ty
+ -- It's really important to check for escape wrt
+ -- the free vars of both expected_ty *and* actual_ty
-----------------------------------
-- Specialisation case (rule ASPEC):
-- co_fn e = e Int dOrdInt
tc_sub outer act_sty actual_ty 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.)
+-- The idea is to *first* do pre-subsumption, and then full subsumption
+-- Example: forall a. a->a <= Int -> (forall b. Int)
+-- Pre-subsumpion finds a|->Int, and that works fine, whereas
+-- just running full subsumption would fail.
| isSigmaTy actual_ty
- = do { (tyvars, theta, tau) <- tcInstBoxy actual_ty
- ; dicts <- newDicts InstSigOrigin theta
+ = do { -- 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
+ tau_tvs = exactTyVarsOfType tau
+ ; inst_tys <- preSubType tyvars tau_tvs tau expected_ty
+ ; let subst' = zipOpenTvSubst tyvars inst_tys
+ tau' = substTy subst' tau
+
+ -- Perform a full subsumption check
+ ; co_fn <- tc_sub False tau' tau' exp_sty expected_ty
+
+ -- Deal with the dictionaries
+ ; dicts <- newDicts InstSigOrigin (substTheta subst' theta)
; extendLIEs dicts
- ; let inst_fn = CoApps (CoTyApps CoHole (mkTyVarTys tyvars))
+ ; let inst_fn = CoApps (CoTyApps CoHole inst_tys)
(map instToId dicts)
- ; co_fn <- tc_sub False tau tau exp_sty expected_ty
; return (co_fn <.> inst_fn) }
-----------------------------------
= -- Expand synonyms; ignore FTVs
uUnfilledVar False swapped tv1 details1 nb2 ps_ty2 ty2'
-uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2@(TyVarTy tv2)
- -- Same type variable => no-op
- | tv1 == tv2
- = returnM ()
+uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 (TyVarTy tv2)
+ | tv1 == tv2 -- Same type variable => no-op (but watch out for the boxy case)
+ = case details1 of
+ 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
-- Distinct type variables
| otherwise
-- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
-- ty2 is not a type variable
+uMetaVar swapped tv1 BoxTv ref1 nb2 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
+ --
+ -- It should not be the case that tv1 occurs in ty2
+ -- (i.e. no occurs check should be needed), but if perchance
+ -- it does, the unbox operation will fill it, and the DEBUG
+ -- checks for that.
+ do { final_ty <- unBox ps_ty2
+#ifdef DEBUG
+ ; meta_details <- readMutVar ref1
+ ; case meta_details of
+ Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
+ return () -- This really should *not* happen
+ Flexi -> return ()
+#endif
+ ; checkUpdateMeta swapped tv1 ref1 final_ty }
+
uMetaVar swapped tv1 info1 ref1 nb2 ps_ty2 non_var_ty2
- = do { final_ty <- case info1 of
- BoxTv -> unBox ps_ty2 -- No occurs check
- other -> checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check
+ = do { final_ty <- checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check
; checkUpdateMeta swapped tv1 ref1 final_ty }
----------------
-- |- s' ~ box(s)
-- with input s', and result s
--
--- It remove all boxes from the input type, returning a non-boxy type.
+-- It removes all boxes from the input type, returning a non-boxy type.
-- A filled box in the type can only contain a monotype; unBox fails if not
-- The type can have empty boxes, which unBox fills with a monotype
--
= do { ty' <- zonkTcType ty
; env0 <- tcInitTidyEnv
; let (env1, tidy_ty) = tidyOpenType env0 ty'
- msg = ptext SLIT("Cannot match a monotype with") <+> ppr tidy_ty
+ msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
; failWithTcM (env1, msg) }
occurCheck tyvar ty