Do pre-subsumption in the main subsumption check
authorsimonpj@microsoft.com <unknown>
Fri, 4 Aug 2006 21:49:42 +0000 (21:49 +0000)
committersimonpj@microsoft.com <unknown>
Fri, 4 Aug 2006 21:49:42 +0000 (21:49 +0000)
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.

compiler/rename/RnExpr.lhs
compiler/typecheck/TcExpr.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcPat.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs

index e968590..c14909e 100644 (file)
@@ -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
index 36cda5a..e897420 100644 (file)
@@ -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
 
index 6a2041e..fe51df1 100644 (file)
@@ -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}
 
 
index 4c56b08..3c1c3ba 100644 (file)
@@ -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)) }
index b60936d..5ad9a10 100644 (file)
@@ -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
index 1a61822..c13da2c 100644 (file)
@@ -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
 --