Two more error message indendations
[ghc-hetmet.git] / compiler / typecheck / TcUnify.lhs
index 23cc9e2..e8fb134 100644 (file)
@@ -13,7 +13,7 @@ module TcUnify (
   unifyType, unifyTypeList, unifyTheta,
   unifyKind, unifyKinds, unifyFunKind, 
   checkExpectedKind, 
-  boxySubMatchType, boxyMatchTypes,
+  preSubType, boxyMatchTypes,
 
   --------------------------------
   -- Holes
@@ -29,31 +29,34 @@ 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, 
+                         tcInstSkolTyVars, tcInstTyVar,
                          zonkTcKind, zonkType, zonkTcType,  zonkTcTyVarsAndFV, 
                          readKindVar, writeKindVar )
 import TcSimplify      ( tcSimplifyCheck )
 import TcEnv           ( tcGetGlobalTyVars, findGlobals )
 import TcIface         ( checkWiredInTyCon )
 import TcRnMonad         -- TcType, amongst others
-import TcType          ( TcKind, TcType, TcTyVar, TcTauType,
+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,
-                         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, mkArrowKind, defaultKind,
+                         openTypeKind, liftedTypeKind, unliftedTypeKind, 
+                         mkArrowKind, defaultKind,
                          isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
                          isSubKind, pprKind, splitKindFunTys )
 import TysPrim         ( alphaTy, betaTy )
@@ -62,8 +65,7 @@ import TyCon          ( TyCon, tyConArity, tyConTyVars, isSynTyCon )
 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 )
@@ -165,7 +167,7 @@ subFunTys error_herald n_pats res_ty thing_inside
     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)
@@ -182,9 +184,9 @@ subFunTys error_herald n_pats res_ty thing_inside
                -- 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'
@@ -333,16 +335,108 @@ 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
+  = 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; 
@@ -351,57 +445,10 @@ 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
+-- 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 )
@@ -411,8 +458,9 @@ boxyMatchTypes tmpl_tvs tmpl_tys 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
@@ -433,8 +481,13 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
        | 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
@@ -451,14 +504,22 @@ 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'
+       | 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
@@ -477,8 +538,8 @@ boxyLub orig_ty1 orig_ty2
       = 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
@@ -488,6 +549,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.
 
 %************************************************************************
 %*                                                                     *
@@ -562,8 +636,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):
@@ -572,13 +646,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) }
 
 -----------------------------------
@@ -995,10 +1087,14 @@ uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2
   =    -- 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
@@ -1024,10 +1120,26 @@ uMetaVar :: Bool
 -- 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 }
 
 ----------------
@@ -1079,13 +1191,18 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
     update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
     update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
 
-    box_meets_box | k1_sub_k2 = fill_with k1
-                 | k2_sub_k1 = fill_with k2
+    box_meets_box | k1_sub_k2 = if k2_sub_k1 && nicer_to_update_tv1
+                               then fill_from tv2
+                               else fill_from tv1
+                 | k2_sub_k1 = fill_from tv2
                  | otherwise = kind_err
 
-    fill_with kind = do { tau_ty <- newFlexiTyVarTy kind
-                       ; updateMeta tv1 ref1 tau_ty
-                       ; updateMeta tv2 ref2 tau_ty }
+       -- Update *both* tyvars with a TauTv whose name and kind
+       -- are gotten from tv (avoid losing nice names is poss)
+    fill_from tv = do { tv' <- tcInstTyVar tv
+                     ; let tau_ty = mkTyVarTy tv'
+                     ; updateMeta tv1 ref1 tau_ty
+                     ; updateMeta tv2 ref2 tau_ty }
 
     kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
               unifyKindMisMatch k1 k2
@@ -1181,9 +1298,7 @@ checkTauTvUpdate orig_tv orig_ty
             ; case cts of
                  Indirect ty -> go ty 
                  Flexi -> case box of
-                               BoxTv -> do { tau <- newFlexiTyVarTy (tyVarKind tv)
-                                           ; writeMutVar ref (Indirect tau)
-                                           ; return tau }
+                               BoxTv -> fillBoxWithTau tv ref
                                other -> return (TyVarTy tv)
             }
 
@@ -1201,6 +1316,19 @@ checkTauTvUpdate orig_tv orig_ty
                                        (tcView (TyConApp tc tys)))
                                -- Try again, expanding the synonym
             }
+
+fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
+-- (fillBoxWithTau tv ref) fills ref with a freshly allocated 
+--  tau-type meta-variable, whose print-name is the same as tv
+-- Choosing the same name is good: when we instantiate a function
+-- we allocate boxy tyvars with the same print-name as the quantified
+-- tyvar; and then we often fill the box with a tau-tyvar, and again
+-- we want to choose the same name.
+fillBoxWithTau tv ref 
+  = do { tv' <- tcInstTyVar tv         -- Do not gratuitously forget
+       ; let tau = mkTyVarTy tv'       -- name of the type variable
+       ; writeMutVar ref (Indirect tau)
+       ; return tau }
 \end{code}
 
 Note [Type synonyms and the occur check]
@@ -1251,7 +1379,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
 --
@@ -1271,13 +1399,11 @@ unBox (TyVarTy tv)
   , MetaTv BoxTv ref <- tcTyVarDetails tv      -- NB: non-TcTyVars are possible
   = do { cts <- readMutVar ref                 --     under nested quantifiers
        ; case cts of
+           Flexi       -> fillBoxWithTau tv ref
            Indirect ty -> do { non_boxy_ty <- unBox ty
                              ; if isTauTy non_boxy_ty 
                                then return non_boxy_ty
                                else notMonoType non_boxy_ty }
-           Flexi -> do { tau <- newFlexiTyVarTy (tyVarKind tv)
-                       ; writeMutVar ref (Indirect tau)
-                       ; return tau }
        }
   | otherwise  -- Skolems, and meta-tau-variables
   = return (TyVarTy tv)
@@ -1490,6 +1616,7 @@ kindSimpleKind orig_swapped orig_kind
     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 swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
                                  <+> ppr orig_swapped <+> ppr orig_kind)