Add left-to-right impredicative instantiation

People keep complaining, with some justification, that

	runST $ foo

doesn't work.  So I've finally caved in.  The difficulty with the above
is that we need to decide how to instantiate ($)'s type arguments based
on the first argument (runST), and then use that info to check the second
argumnent.  There is a left-to-right flow of information.

It's not hard to implement this, and it's clearly useful.  The main
change is in TcExpr.tcArgs, with some knock-on effects elsewhere.

I was finally provoked into this by Trac #981, which turned out, after some
head-scratching, to be another instance of the same problem.

(There was some bug-fixing too; a type like ((?x::Int) => ...) is a polytype
even though it has no leading for-alls, but the new TcUnify code was not
treating it right.)

Test for this is tc222

diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index 18bef23..fa0e419 100644 (file)
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -228,10 +228,12 @@ tcExpr in_expr@(SectionR lop@(L loc op) arg2) res_ty
   where
     doc = ptext SLIT("The section") <+> quotes (ppr in_expr)
                <+> ptext SLIT("takes one argument")
   where
     doc = ptext SLIT("The section") <+> quotes (ppr in_expr)
                <+> ptext SLIT("takes one argument")

-    tc_args arg1_ty' [arg1_ty, arg2_ty] 
-       = do { boxyUnify arg1_ty' arg1_ty
-            ; tcArg lop (arg2, arg2_ty, 2) }
-    tc_args arg1_ty' other = panic "tcExpr SectionR"
+    tc_args arg1_ty' qtvs qtys [arg1_ty, arg2_ty] 
+       = do { boxyUnify arg1_ty' (substTyWith qtvs qtys arg1_ty)
+            ; arg2' <- tcArg lop 2 arg2 qtvs qtys arg2_ty 
+            ; qtys' <- mapM refineBox qtys     -- c.f. tcArgs 
+            ; return (qtys', arg2') }
+    tc_args arg1_ty' _ _ _ = panic "tcExpr SectionR"

 \end{code}
 
 \begin{code}
 \end{code}
 
 \begin{code}

@@ -321,12 +323,15 @@ tcExpr expr@(RecordCon (L loc con_name) _ rbinds) res_ty
        ; checkMissingFields data_con rbinds
 
        ; let arity = dataConSourceArity data_con
        ; checkMissingFields data_con rbinds
 
        ; let arity = dataConSourceArity data_con

-             check_fields arg_tys 
-                 = do  { rbinds' <- tcRecordBinds data_con arg_tys rbinds
-                       ; mapM unBox arg_tys 
-                       ; return rbinds' }
-               -- The unBox ensures that all the boxes in arg_tys are indeed
+             check_fields qtvs qtys arg_tys 
+                 = do  { let arg_tys' = substTys (zipOpenTvSubst qtvs qtys) arg_tys
+                       ; rbinds' <- tcRecordBinds data_con arg_tys' rbinds
+                       ; qtys' <- mapM refineBoxToTau qtys
+                       ; return (qtys', rbinds') }
+               -- The refineBoxToTau ensures that all the boxes in arg_tys are indeed

                -- filled, which is the invariant expected by tcIdApp
                -- filled, which is the invariant expected by tcIdApp

+               -- How could this not be the case?  Consider a record construction
+               -- that does not mention all the fields.

 
        ; (con_expr, rbinds') <- tcIdApp con_name arity check_fields res_ty
 
 
        ; (con_expr, rbinds') <- tcIdApp con_name arity check_fields res_ty
 

@@ -571,9 +576,9 @@ tcExpr other _ = pprPanic "tcMonoExpr" (ppr other)
 ---------------------------
 tcApp :: HsExpr Name                           -- Function
       -> Arity                                 -- Number of args reqd
 ---------------------------
 tcApp :: HsExpr Name                           -- Function
       -> Arity                                 -- Number of args reqd

-      -> ([BoxySigmaType] -> TcM arg_results)  -- Argument type-checker
+      -> ArgChecker results

       -> BoxyRhoType                           -- Result type
       -> BoxyRhoType                           -- Result type

-      -> TcM (HsExpr TcId, arg_results)                
+      -> TcM (HsExpr TcId, results)            

 
 -- (tcFun fun n_args arg_checker res_ty)
 -- The argument type checker, arg_checker, will be passed exactly n_args types
 
 -- (tcFun fun n_args arg_checker res_ty)
 -- The argument type checker, arg_checker, will be passed exactly n_args types

@@ -582,19 +587,18 @@ tcApp (HsVar fun_name) n_args arg_checker res_ty
   = tcIdApp fun_name n_args arg_checker res_ty
 
 tcApp fun n_args arg_checker res_ty    -- The vanilla case (rula APP)
   = tcIdApp fun_name n_args arg_checker res_ty
 
 tcApp fun n_args arg_checker res_ty    -- The vanilla case (rula APP)

-  = do { arg_boxes <- newBoxyTyVars (replicate n_args argTypeKind)
-       ; fun'      <- tcExpr fun (mkFunTys (mkTyVarTys arg_boxes) res_ty)
-       ; arg_tys'  <- mapM readFilledBox arg_boxes
-       ; args'     <- arg_checker arg_tys'
+  = do { arg_boxes  <- newBoxyTyVars (replicate n_args argTypeKind)
+       ; fun'       <- tcExpr fun (mkFunTys (mkTyVarTys arg_boxes) res_ty)
+       ; arg_tys'   <- mapM readFilledBox arg_boxes
+       ; (_, args') <- arg_checker [] [] arg_tys'      -- Yuk

        ; return (fun', args') }
 
 ---------------------------
 tcIdApp :: Name                                        -- Function
         -> Arity                               -- Number of args reqd
        ; return (fun', args') }
 
 ---------------------------
 tcIdApp :: Name                                        -- Function
         -> Arity                               -- Number of args reqd

-        -> ([BoxySigmaType] -> TcM arg_results)        -- Argument type-checker
-               -- The arg-checker guarantees to fill all boxes in the arg types
+        -> ArgChecker results  -- The arg-checker guarantees to fill all boxes in the arg types

         -> BoxyRhoType                         -- Result type
         -> BoxyRhoType                         -- Result type

-        -> TcM (HsExpr TcId, arg_results)              
+        -> TcM (HsExpr TcId, results)          

 
 -- Call        (f e1 ... en) :: res_ty
 -- Type                f :: forall a b c. theta => fa_1 -> ... -> fa_k -> fres
 
 -- Call        (f e1 ... en) :: res_ty
 -- Type                f :: forall a b c. theta => fa_1 -> ... -> fa_k -> fres

@@ -627,23 +631,16 @@ tcIdApp fun_name n_args arg_checker res_ty
        ; let extra_arg_tys' = mkTyVarTys extra_arg_boxes
              res_ty'        = mkFunTys extra_arg_tys' res_ty
        ; qtys' <- preSubType qtvs tau_qtvs fun_res_ty res_ty'
        ; let extra_arg_tys' = mkTyVarTys extra_arg_boxes
              res_ty'        = mkFunTys extra_arg_tys' res_ty
        ; 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

 
        -- Typecheck the arguments!
        -- Doing so will fill arg_qtvs and extra_arg_tys'
 
        -- Typecheck the arguments!
        -- Doing so will fill arg_qtvs and extra_arg_tys'

-       ; args' <- arg_checker (fun_arg_tys' ++ extra_arg_tys')
+       ; (qtys'', args') <- arg_checker qtvs qtys' (fun_arg_tys ++ extra_arg_tys')

 
        -- Strip boxes from the qtvs that have been filled in by the arg checking
 
        -- 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'
-       ; qtys'' <- zipWithM strip qtvs qtys'

        ; extra_arg_tys'' <- mapM readFilledBox extra_arg_boxes
 
        -- Result subsumption
        ; extra_arg_tys'' <- mapM readFilledBox extra_arg_boxes
 
        -- Result subsumption

+       -- This fills in res_qtvs

        ; let res_subst = zipOpenTvSubst qtvs qtys''
              fun_res_ty'' = substTy res_subst fun_res_ty
              res_ty'' = mkFunTys extra_arg_tys'' res_ty
        ; let res_subst = zipOpenTvSubst qtvs qtys''
              fun_res_ty'' = substTy res_subst fun_res_ty
              res_ty'' = mkFunTys extra_arg_tys'' res_ty

@@ -653,7 +650,7 @@ tcIdApp fun_name n_args arg_checker res_ty
        -- By applying the coercion just to the *function* we can make
        -- tcFun work nicely for OpApp and Sections too
        ; fun' <- instFun orig fun res_subst tv_theta_prs
        -- By applying the coercion just to the *function* we can make
        -- tcFun work nicely for OpApp and Sections too
        ; fun' <- instFun orig fun res_subst tv_theta_prs

-       ; co_fn' <- wrapFunResCoercion fun_arg_tys' co_fn
+       ; co_fn' <- wrapFunResCoercion (substTys res_subst fun_arg_tys) co_fn

        ; return (mkHsWrap co_fn' fun', args') }
 \end{code}
 
        ; return (mkHsWrap co_fn' fun', args') }
 \end{code}
 

@@ -818,19 +815,45 @@ This gets a bit less sharing, but
        a) it's better for RULEs involving overloaded functions
        b) perhaps fewer separated lambdas
 
        a) it's better for RULEs involving overloaded functions
        b) perhaps fewer separated lambdas
 

+Note [Left to right]
+~~~~~~~~~~~~~~~~~~~~
+tcArgs implements a left-to-right order, which goes beyond what is described in the
+impredicative type inference paper.  In particular, it allows
+       runST $ foo
+where runST :: (forall s. ST s a) -> a
+When typechecking the application of ($)::(a->b) -> a -> b, we first check that
+runST has type (a->b), thereby filling in a=forall s. ST s a.  Then we un-box this type
+before checking foo.  The left-to-right order really helps here.
+

 \begin{code}
 tcArgs :: LHsExpr Name                         -- The function (for error messages)
 \begin{code}
 tcArgs :: LHsExpr Name                         -- The function (for error messages)

-       -> [LHsExpr Name] -> [TcSigmaType]      -- Actual arguments and expected arg types
-       -> TcM [LHsExpr TcId]                   -- Resulting args
+       -> [LHsExpr Name]                       -- Actual args
+       -> ArgChecker [LHsExpr TcId]

 
 

-tcArgs fun args expected_arg_tys
-  = mapM (tcArg fun) (zip3 args expected_arg_tys [1..])
+type ArgChecker results
+   = [TyVar] -> [TcSigmaType]          -- Current instantiation
+   -> [TcSigmaType]                    -- Expected arg types (**before** applying the instantiation)
+   -> TcM ([TcSigmaType], results)     -- Resulting instaniation and args

 
 

-tcArg :: LHsExpr Name                          -- The function (for error messages)
-       -> (LHsExpr Name, BoxySigmaType, Int)   -- Actual argument and expected arg type
-       -> TcM (LHsExpr TcId)                   -- Resulting argument
-tcArg fun (arg, ty, arg_no) = addErrCtxt (funAppCtxt fun arg arg_no) $
-                             tcPolyExprNC arg ty
+tcArgs fun args qtvs qtys arg_tys
+  = go 1 qtys args arg_tys
+  where
+    go n qtys [] [] = return (qtys, [])
+    go n qtys (arg:args) (arg_ty:arg_tys)
+       = do { arg' <- tcArg fun n arg qtvs qtys arg_ty
+            ; qtys' <- mapM refineBox qtys     -- Exploit new info
+            ; (qtys'', args') <- go (n+1) qtys' args arg_tys
+            ; return (qtys'', arg':args') }
+
+tcArg :: LHsExpr Name                          -- The function
+      -> Int                                   --   and arg number (for error messages)
+      -> LHsExpr Name
+      -> [TyVar] -> [TcSigmaType]              -- Instantiate the arg type like this
+      -> BoxySigmaType
+      -> TcM (LHsExpr TcId)                    -- Resulting argument
+tcArg fun arg_no arg qtvs qtys ty
+  = addErrCtxt (funAppCtxt fun arg arg_no) $
+    tcPolyExprNC arg (substTyWith qtvs qtys ty)

 \end{code}
 
 
 \end{code}
 
 

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 0845853..b4e89b0 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -62,7 +62,6 @@ module TcMType (
 import TypeRep
 import TcType
 import Type
 import TypeRep
 import TcType
 import Type

-import Type

 import Coercion
 import Class
 import TyCon
 import Coercion
 import Class
 import TyCon

@@ -360,7 +359,7 @@ data LookupTyVarResult      -- The result of a lookupTcTyVar call
 
 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 lookupTcTyVar tyvar 
 
 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 lookupTcTyVar tyvar 

-  = ASSERT( isTcTyVar tyvar )
+  = ASSERT2( isTcTyVar tyvar, ppr tyvar )

     case details of
       SkolemTv _   -> return (DoneTv details)
       MetaTv _ ref -> do { meta_details <- readMutVar ref
     case details of
       SkolemTv _   -> return (DoneTv details)
       MetaTv _ ref -> do { meta_details <- readMutVar ref

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 1868ad0..de9c341 100644 (file)
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -19,7 +19,7 @@ module TcUnify (
 
   --------------------------------
   -- Holes
 
   --------------------------------
   -- Holes

-  tcInfer, subFunTys, unBox, stripBoxyType, withBox, 
+  tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, 

   boxyUnify, boxyUnifyList, zapToMonotype,
   boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
   wrapFunResCoercion
   boxyUnify, boxyUnifyList, zapToMonotype,
   boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
   wrapFunResCoercion

@@ -607,7 +607,8 @@ tc_sub :: SubCtxt           -- How to add an error-context
 -- 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
 -- 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_sub1 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!
 
        -- This indirection is just here to make 
        -- it easy to insert a debug trace!
 

@@ -637,9 +638,11 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
 -- Consider  f g !
 
 tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
 -- Consider  f g !
 
 tc_sub1 sub_ctxt 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 ->
+  | 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
                             tc_sub sub_ctxt act_sty act_ty False body_exp_ty body_exp_ty
        ; return (gen_fn <.> co_fn) }
   where

@@ -713,11 +716,14 @@ tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_t
 
 -- Everything else: defer to boxy matching
 tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
 
 -- 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
+
+-----------------------------------
+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 }
 
   = 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 act_arg act_res exp_ib exp_arg exp_res
   = do { uTys False act_arg exp_ib exp_arg
 -----------------------------------
 tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
   = do { uTys False act_arg exp_ib exp_arg

@@ -942,8 +948,45 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_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
     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)
+                  subst1   = mkTvSubst in_scope (zipTyEnv tvs1 tys)
+                  subst2   = mkTvSubst in_scope (zipTyEnv tvs2 tys)
+                  (theta1,tau1) = tcSplitPhiTy (substTy subst1 body1)
+                  (theta2,tau2) = tcSplitPhiTy (substTy subst2 body2)
+
+            ; checkM (equalLength theta1 theta2)
+                     (unifyMisMatch outer False orig_ty1 orig_ty2)
+            
+            ; uPreds False nb1 theta1 nb2 theta2
+            ; uTys nb1 tau1 nb2 tau2
+
+               -- 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
        -- 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)
 
        -- Type constructors must match
     go _ (TyConApp con1 tys1) (TyConApp con2 tys2)

@@ -969,27 +1012,6 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
       | Just (s1,t1) <- tcSplitAppTy_maybe ty1
       = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
 
       | 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
-                       -- Get location from monad, not from tvs1
-            ; 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
 
        -- Anything else fails
     go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2

@@ -1000,6 +1022,10 @@ uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
 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)
 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]
 \end{code}
 
 Note [Tycon app]

@@ -1380,16 +1406,27 @@ But we should not reject the program, because A t = ().
 Rather, we should bind t to () (= non_var_ty2).
 
 \begin{code}
 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
 
 zapToMonotype :: BoxySigmaType -> TcM TcTauType
 -- Subtle... we must zap the boxy res_ty