Commit af20907a authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Do pre-subsumption in the main subsumption check

This patch improves the subsumption check (in TcUnify.tc_sub) so that
it does pre-subsumption first.  The key code is in the case with
guard (isSigmaTy actual_ty); note the new call to preSubType.

Shorn of details, the question is this.  Should this hold?

	forall a. a->a   <=   Int -> (forall b. Int)

Really, it should; just instantiate 'a' to Int.  This is just what
the pre-subsumption phase (which used in function applications),
will do.

I did a bit of refactoring to achieve this.

Fixes Trac #821.  Test tc205 tests.
parent 6493f9d3
......@@ -459,7 +459,7 @@ methodNamesCmd other = emptyFVs
-- The type checker will complain later
---------------------------------------------------
methodNamesMatch (MatchGroup ms ty)
methodNamesMatch (MatchGroup ms _)
= plusFVs (map do_one ms)
where
do_one (L _ (Match pats sig_ty grhss)) = methodNamesGRHSs grhss
......
......@@ -26,7 +26,7 @@ import HsSyn ( HsExpr(..), LHsExpr, ArithSeqInfo(..), recBindFields,
import TcHsSyn ( hsLitType )
import TcRnMonad
import TcUnify ( tcInfer, tcSubExp, tcFunResTy, tcGen, boxyUnify, subFunTys, zapToMonotype, stripBoxyType,
boxySplitListTy, boxySplitTyConApp, wrapFunResCoercion, boxySubMatchType,
boxySplitListTy, boxySplitTyConApp, wrapFunResCoercion, preSubType,,
unBox )
import BasicTypes ( Arity, isMarkedStrict )
import Inst ( newMethodFromName, newIPDict, instToId,
......@@ -648,26 +648,7 @@ tcIdApp fun_name n_args arg_checker res_ty
; extra_arg_boxes <- newBoxyTyVars (replicate n_missing_args argTypeKind)
; let extra_arg_tys' = mkTyVarTys extra_arg_boxes
res_ty' = mkFunTys extra_arg_tys' res_ty
subst = boxySubMatchType arg_qtvs fun_res_ty res_ty'
-- Only bind arg_qtvs, since only they will be
-- *definitely* be filled in by arg_checker
-- E.g. error :: forall a. String -> a
-- (error "foo") :: bx5
-- Don't make subst [a |-> bx5]
-- because then the result subsumption becomes
-- bx5 ~ bx5
-- and the unifer doesn't expect the
-- same box on both sides
inst_qtv tv | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty
| tv `elemVarSet` tau_qtvs = do { tv' <- tcInstBoxyTyVar tv
; return (mkTyVarTy tv') }
| otherwise = do { tv' <- tcInstTyVar tv
; return (mkTyVarTy tv') }
-- The 'otherwise' case handles type variables that are
-- mentioned only in the constraints, not in argument or
-- result types. We'll make them tau-types
; qtys' <- mapM inst_qtv qtvs
; qtys' <- preSubType qtvs tau_qtvs fun_res_ty res_ty'
; let arg_subst = zipOpenTvSubst qtvs qtys'
fun_arg_tys' = substTys arg_subst fun_arg_tys
......@@ -675,8 +656,12 @@ tcIdApp fun_name n_args arg_checker res_ty
-- Doing so will fill arg_qtvs and extra_arg_tys'
; args' <- arg_checker (fun_arg_tys' ++ extra_arg_tys')
-- Strip boxes from the qtvs that have been filled in by the arg checking
-- AND any variables that are mentioned in neither arg nor result
-- the latter are mentioned only in constraints; stripBoxyType will
-- fill them with a monotype
; let strip qtv qty' | qtv `elemVarSet` arg_qtvs = stripBoxyType qty'
| otherwise = return qty'
| otherwise = return qty'
; qtys'' <- zipWithM strip qtvs qtys'
; extra_arg_tys'' <- mapM readFilledBox extra_arg_boxes
......@@ -722,17 +707,13 @@ tcId orig fun_name res_ty
-- Split up the function type
; let (tv_theta_prs, fun_tau) = tcMultiSplitSigmaTy (idType fun_id)
qtvs = concatMap fst tv_theta_prs -- Quantified tyvars
tau_qtvs = exactTyVarsOfType fun_tau -- Mentiond in the tau part
inst_qtv tv | tv `elemVarSet` tau_qtvs = do { tv' <- tcInstBoxyTyVar tv
; return (mkTyVarTy tv') }
| otherwise = do { tv' <- tcInstTyVar tv
; return (mkTyVarTy tv') }
qtvs = concatMap fst tv_theta_prs -- Quantified tyvars
tau_qtvs = exactTyVarsOfType fun_tau -- Mentioned in the tau part
; qtv_tys <- preSubType qtvs tau_qtvs fun_tau res_ty
-- Do the subsumption check wrt the result type
; qtv_tys <- mapM inst_qtv qtvs
; let res_subst = zipTopTvSubst qtvs qtv_tys
fun_tau' = substTy res_subst fun_tau
; let res_subst = zipTopTvSubst qtvs qtv_tys
fun_tau' = substTy res_subst fun_tau
; co_fn <- tcFunResTy fun_name fun_tau' res_ty
......
......@@ -24,7 +24,7 @@ module TcMType (
--------------------------------
-- Instantiation
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar,
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
tcInstSigTyVars, zonkSigTyVar,
tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
tcSkolSigType, tcSkolSigTyVars,
......@@ -58,8 +58,7 @@ import TypeRep ( Type(..), PredType(..), -- Friend; can see representation
import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
MetaDetails(..), SkolemInfo(..), BoxInfo(..),
BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType,
UserTypeCtxt(..),
BoxyTyVar, BoxyType, UserTypeCtxt(..),
isMetaTyVar, isSigTyVar, metaTvRef,
tcCmpPred, isClassPred, tcGetTyVar,
tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
......@@ -327,12 +326,6 @@ readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
-- Instantiate with a BOXY type variable
tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
-- tcInstType instantiates the outer-level for-alls of a TcType with
-- fresh BOXY type variables, splits off the dictionary part,
-- and returns the pieces.
tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
\end{code}
......
......@@ -683,8 +683,7 @@ newLitInst orig lit res_ty -- Make a LitInst
= do { loc <- getInstLoc orig
; res_tau <- zapToMonotype res_ty
; new_uniq <- newUnique
; let
lit_nm = mkSystemVarName new_uniq FSLIT("lit")
; let lit_nm = mkSystemVarName new_uniq FSLIT("lit")
lit_inst = LitInst lit_nm lit res_tau loc
; extendLIE lit_inst
; return (HsVar (instToId lit_inst)) }
......
......@@ -170,7 +170,7 @@ import TyCon ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique )
import DataCon ( DataCon, dataConStupidTheta, dataConResTys )
import Class ( Class )
import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
import ForeignCall ( Safety, playSafe, DNType(..) )
import ForeignCall ( Safety, DNType(..) )
import Unify ( tcMatchTys )
import VarSet
......@@ -966,7 +966,7 @@ smart-app checking code --- see TcExpr.tcIdApp
\begin{code}
exactTyVarsOfType :: TcType -> TyVarSet
-- Find the free type variables (of any kind)
-- but *expand* type synonyms. See Note [Silly type synonym] belos.
-- but *expand* type synonyms. See Note [Silly type synonym] above.
exactTyVarsOfType ty
= go ty
where
......
......@@ -13,7 +13,7 @@ module TcUnify (
unifyType, unifyTypeList, unifyTheta,
unifyKind, unifyKinds, unifyFunKind,
checkExpectedKind,
boxySubMatchType, boxyMatchTypes,
preSubType, boxyMatchTypes,
--------------------------------
-- Holes
......@@ -29,8 +29,8 @@ import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) )
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,
......@@ -46,11 +46,13 @@ import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType,
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,
......@@ -334,16 +336,95 @@ withBox kind thing_inside
%************************************************************************
\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
= mapM inst_tv qtvs
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_ty emptyVarSet boxy_ty
where
go t_ty b_tvs b_ty
| Just t_ty' <- tcView t_ty = go t_ty' b_tvs b_ty
| Just b_ty' <- tcView b_ty = go t_ty b_tvs b_ty'
go (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 (ForAllTy tv t_ty) b_tvs b_ty = go t_ty b_tvs b_ty -- Rule S-SPEC
go t_ty b_tvs (ForAllTy tv b_ty) = go t_ty b_tvs' b_ty -- Rule S-SKOL
where b_tvs' = extendVarSet b_tvs tv
go (FunTy arg1 res1) b_tvs (FunTy arg2 res2) -- Rule S-FUN
= boxy_match tmpl_tvs arg1 b_tvs arg2 (go res1 b_tvs res2)
-- Match the args, and sub-match the results
go t_ty b_tvs b_ty = boxy_match tmpl_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;
......@@ -352,57 +433,12 @@ boxyMatchTypes
-- 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
--
-- 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 )
......@@ -452,7 +488,7 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
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'
where
boxy_ty' = case lookupTyVar subst tv of
......@@ -489,6 +525,19 @@ boxyLub orig_ty1 orig_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.
%************************************************************************
%* *
......@@ -563,8 +612,8 @@ tc_sub outer act_sty act_ty exp_sty exp_ty
; 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):
......@@ -573,13 +622,31 @@ tc_sub outer act_sty act_ty exp_sty exp_ty
-- 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) }
-----------------------------------
......@@ -1288,7 +1355,7 @@ unBox :: BoxyType -> TcM TcType
-- |- 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
--
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment