Fix two obscure bugs in rule matching

This patch fixes Trac #14777, a compiler crash.

There were actually two bugs.

1. In Rules.matchN, I was (consciously) not rename the template binders
   of the rule. Sadly, in rare cases an accidental coincidence of
   uniques could mean that a term variable was mapped to a type
   variable, utterly bogusly.  See "Historical note" in
   Note [Cloning the template binders] in Rules.

   This was hard to find, but easy to fix.

2. The fix to (1) showed up a bug in Unify.hs.  The test in
   Unify.tvBindFlag was previously using the domain of the RnEnv2
   to detect locally-bound variables (e.g. when unifying under
   a forall).  That's fine when teh RnEnv2 starts empty, as it
   does in most entry points.  But the tcMatchTyKisX entry point,
   used from the rule matcher, passes in a non-empty RnEnv2 (by
   design).  Now the domain of the RnEnv doesn't idenfity those
   locally-bound variables any more :-(.

   Solution: extend UmEnv with a new field um_skols, to capture
   the skolems directly.  Simple, easy, works.

2 files changed, 154 insertions, 120 deletions

diff --git a/compiler/specialise/Rules.hs b/compiler/specialise/Rules.hs
index b6025955ac..8b15c819b6 100644
--- a/compiler/specialise/Rules.hs
+++ b/compiler/specialise/Rules.hs
@@ -40,7 +40,7 @@ import CoreUtils        ( exprType, eqExpr, mkTick, mkTicks,
                           stripTicksTopT, stripTicksTopE,
                           isJoinBind )
 import PprCore          ( pprRules )
-import Type             ( Type, substTy, mkTCvSubst )
+import Type             ( Type, Kind, substTy, mkTCvSubst )
 import TcType           ( tcSplitTyConApp_maybe )
 import TysWiredIn       ( anyTypeOfKind )
 import Coercion
@@ -518,7 +518,7 @@ matchRule _ in_scope is_active _ args rough_args
   | ruleCantMatch tpl_tops rough_args = Nothing
   | otherwise
   = case matchN in_scope rule_name tpl_vars tpl_args args of
-        Nothing                        -> Nothing
+        Nothing                       -> Nothing
         Just (bind_wrapper, tpl_vals) -> Just (bind_wrapper $
                                                rule_fn `mkApps` tpl_vals)
   where
@@ -536,58 +536,82 @@ matchN  :: InScopeEnv
 
 matchN (in_scope, id_unf) rule_name tmpl_vars tmpl_es target_es
   = do  { subst <- go init_menv emptyRuleSubst tmpl_es target_es
-        ; let (_, matched_es) = mapAccumL lookup_tmpl subst tmpl_vars
+        ; let (_, matched_es) = mapAccumL lookup_tmpl subst $
+                                tmpl_vars `zip` tmpl_vars1
         ; return (rs_binds subst, matched_es) }
   where
-    init_rn_env = mkRnEnv2 (extendInScopeSetList in_scope tmpl_vars)
-                  -- See Note [Template binders]
+    (init_rn_env, tmpl_vars1) = mapAccumL rnBndrL (mkRnEnv2 in_scope) tmpl_vars
+                  -- See Note [Cloning the template binders]
 
-    init_menv = RV { rv_tmpls = mkVarSet tmpl_vars, rv_lcl = init_rn_env
-                   , rv_fltR = mkEmptySubst (rnInScopeSet init_rn_env)
-                   , rv_unf = id_unf }
+    init_menv = RV { rv_tmpls = mkVarSet tmpl_vars1
+                   , rv_lcl   = init_rn_env
+                   , rv_fltR  = mkEmptySubst (rnInScopeSet init_rn_env)
+                   , rv_unf   = id_unf }
 
     go _    subst []     _      = Just subst
     go _    _     _      []     = Nothing       -- Fail if too few actual args
     go menv subst (t:ts) (e:es) = do { subst1 <- match menv subst t e
                                      ; go menv subst1 ts es }
 
-    lookup_tmpl :: RuleSubst -> Var -> (RuleSubst, CoreExpr)
-    lookup_tmpl rs@(RS { rs_tv_subst = tv_subst, rs_id_subst = id_subst }) tmpl_var
-        | isId tmpl_var
-        = case lookupVarEnv id_subst tmpl_var of
+    lookup_tmpl :: RuleSubst -> (InVar,OutVar) -> (RuleSubst, CoreExpr)
+                   -- Need to return a RuleSubst solely for the benefit of mk_fake_ty
+    lookup_tmpl rs@(RS { rs_tv_subst = tv_subst, rs_id_subst = id_subst })
+                (tmpl_var, tmpl_var1)
+        | isId tmpl_var1
+        = case lookupVarEnv id_subst tmpl_var1 of
              Just e -> (rs, e)
-             Nothing | Just refl_co <- isReflCoVar_maybe tmpl_var
-                     , let co_expr = Coercion refl_co
-                     -> (rs { rs_id_subst = extendVarEnv id_subst tmpl_var co_expr }, co_expr)
+             Nothing | Just refl_co <- isReflCoVar_maybe tmpl_var1
+                     , let co_expr   = Coercion refl_co
+                           id_subst' = extendVarEnv id_subst tmpl_var1 co_expr
+                           rs'       = rs { rs_id_subst = id_subst' }
+                     -> (rs', co_expr) -- See Note [Unbound RULE binders]
                      | otherwise
                      -> unbound tmpl_var
         | otherwise
-        = case lookupVarEnv tv_subst tmpl_var of
+        = case lookupVarEnv tv_subst tmpl_var1 of
              Just ty -> (rs, Type ty)
-             Nothing -> (rs { rs_tv_subst = extendVarEnv tv_subst tmpl_var fake_ty }, Type fake_ty)
-                        -- See Note [Unbound RULE binders]
+             Nothing -> (rs', Type fake_ty) -- See Note [Unbound RULE binders]
         where
-          fake_ty = anyTypeOfKind kind
-          cv_subst = to_co_env id_subst
-          kind = Type.substTy (mkTCvSubst in_scope (tv_subst, cv_subst))
-                              (tyVarKind tmpl_var)
-
-          to_co_env env = nonDetFoldUFM_Directly to_co emptyVarEnv env
-            -- It's OK to use nonDetFoldUFM_Directly because we forget the
-            -- order immediately by creating a new env
-          to_co uniq expr env
-            | Just co <- exprToCoercion_maybe expr
-            = extendVarEnv_Directly env uniq co
-
-            | otherwise
-            = env
-
-    unbound var = pprPanic "Template variable unbound in rewrite rule" $
-                  vcat [ text "Variable:" <+> ppr var <+> dcolon <+> ppr (varType var)
-                       , text "Rule" <+> pprRuleName rule_name
-                       , text "Rule bndrs:" <+> ppr tmpl_vars
-                       , text "LHS args:" <+> ppr tmpl_es
-                       , text "Actual args:" <+> ppr target_es ]
+          rs'     = rs { rs_tv_subst = extendVarEnv tv_subst tmpl_var1 fake_ty }
+          fake_ty = mk_fake_ty in_scope rs tmpl_var1
+                    -- This call is the sole reason we accumulate
+                    -- RuleSubst in lookup_tmpl
+
+    unbound tmpl_var
+       = pprPanic "Template variable unbound in rewrite rule" $
+         vcat [ text "Variable:" <+> ppr tmpl_var <+> dcolon <+> ppr (varType tmpl_var)
+              , text "Rule" <+> pprRuleName rule_name
+              , text "Rule bndrs:" <+> ppr tmpl_vars
+              , text "LHS args:" <+> ppr tmpl_es
+              , text "Actual args:" <+> ppr target_es ]
+
+
+mk_fake_ty :: InScopeSet -> RuleSubst -> TyVar -> Kind
+-- Roughly:
+--    mk_fake_ty subst tv = Any @(subst (tyVarKind tv))
+-- That is: apply the substitution to the kind of the given tyvar,
+-- and make an 'any' type of that kind.
+-- Tiresomely, the RuleSubst is not well adapted to substTy, leading to
+-- horrible impedence matching.
+--
+-- Happily, this function is seldom called
+mk_fake_ty in_scope (RS { rs_tv_subst = tv_subst, rs_id_subst = id_subst }) tmpl_var1
+  = anyTypeOfKind kind
+  where
+    kind = Type.substTy (mkTCvSubst in_scope (tv_subst, cv_subst))
+                        (tyVarKind tmpl_var1)
+
+    cv_subst = to_co_env id_subst
+
+    to_co_env :: IdSubstEnv -> CvSubstEnv
+    to_co_env env = nonDetFoldUFM_Directly to_co emptyVarEnv env
+      -- It's OK to use nonDetFoldUFM_Directly because we forget the
+      -- order immediately by creating a new env
+
+    to_co uniq expr env
+      = case exprToCoercion_maybe expr of
+          Just co -> extendVarEnv_Directly env uniq co
+          Nothing -> env
 
 {- Note [Unbound RULE binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -632,8 +656,8 @@ bound on the LHS:
   in Trac #13410, and also in test T10602.
 
 
-Note [Template binders]
-~~~~~~~~~~~~~~~~~~~~~~~
+Note [Cloning the template binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider the following match (example 1):
         Template:  forall x.  f x
         Target:               f (x+1)
@@ -644,21 +668,19 @@ Likewise this one (example 2):
         Template:  forall x. f (\x.x)
         Target:              f (\y.y)
 
-We achieve this simply by:
-  * Adding forall'd template binders to the in-scope set
+We achieve this simply by using rnBndrL to clone the template
+binders if they are already in scope.
 
-This works even if the template binder are already in scope
-(in the target) because
-
-  * The RuleSubst rs_tv_subst, rs_id_subst maps LHS template vars to
-    the target world.  It is not applied recursively.
-
-  * Having the template vars in the in-scope set ensures that in
-    example 2 above, the (\x.x) is cloned to (\x'. x').
-
-In the past we used rnBndrL to clone the template variables if
-they were already in scope.  But (a) that's not necessary and (b)
-it complicate the fancy footwork for Note [Unbound template type variables]
+------ Historical note -------
+At one point I tried simply adding the template binders to the
+in-scope set /without/ cloning them, but that failed in a horribly
+obscure way in Trac #14777.  Problem was that during matching we look
+up target-term variables in the in-scope set (see Note [Lookup
+in-scope]).  If a target-term variable happens to name-clash with a
+template variable, that lookup will find the template variable, which
+is /uttterly/ bogus.  In Trac #14777, this transformed a term variable
+into a type variable, and then crashed when we wanted its idInfo.
+------ End of historical note -------
 
 
 ************************************************************************
@@ -674,11 +696,12 @@ it complicate the fancy footwork for Note [Unbound template type variables]
 --   from nested matches; see the Let case of match, below
 --
 data RuleMatchEnv
-  = RV { rv_tmpls :: VarSet          -- Template variables
-       , rv_lcl   :: RnEnv2          -- Renamings for *local bindings*
+  = RV { rv_lcl   :: RnEnv2          -- Renamings for *local bindings*
                                      --   (lambda/case)
+       , rv_tmpls :: VarSet          -- Template variables
+                                     --   (after applying envL of rv_lcl)
        , rv_fltR  :: Subst           -- Renamings for floated let-bindings
-                                     --   domain disjoint from envR of rv_lcl
+                                     --   (domain disjoint from envR of rv_lcl)
                                      -- See Note [Matching lets]
        , rv_unf :: IdUnfoldingFun
        }
@@ -708,7 +731,6 @@ emptyRuleSubst = RS { rs_tv_subst = emptyVarEnv, rs_id_subst = emptyVarEnv
 --      For a start, in general eta expansion wastes work.
 --      SLPJ July 99
 
-
 match :: RuleMatchEnv
       -> RuleSubst
       -> CoreExpr               -- Template
@@ -739,7 +761,8 @@ match _ _ e@Tick{} _
 -- succeed in matching what looks like the template variable 'a' against 3.
 
 -- The Var case follows closely what happens in Unify.match
-match renv subst (Var v1)    e2 = match_var renv subst v1 e2
+match renv subst (Var v1) e2
+  = match_var renv subst v1 e2
 
 match renv subst e1 (Var v2)      -- Note [Expanding variables]
   | not (inRnEnvR rn_env v2) -- Note [Do not expand locally-bound variables]
@@ -1111,19 +1134,19 @@ SpecConstr sees this fragment:
           Data.Maybe.Nothing -> lvl_smf;
           Data.Maybe.Just n_acT [Just S(L)] ->
             case n_acT of wild1_ams [Just A] { GHC.Base.I# y_amr [Just L] ->
-            \$wfoo_smW (GHC.Prim.-# ds_Xmb y_amr) wild_Xf
+              $wfoo_smW (GHC.Prim.-# ds_Xmb y_amr) wild_Xf
             }};
 
 and correctly generates the rule
 
         RULES: "SC:$wfoo1" [0] __forall {y_amr [Just L] :: GHC.Prim.Int#
                                           sc_snn :: GHC.Prim.Int#}
-          \$wfoo_smW sc_snn (Data.Maybe.Just @ GHC.Base.Int (GHC.Base.I# y_amr))
-          = \$s\$wfoo_sno y_amr sc_snn ;]
+          $wfoo_smW sc_snn (Data.Maybe.Just @ GHC.Base.Int (GHC.Base.I# y_amr))
+          = $s$wfoo_sno y_amr sc_snn ;]
 
 BUT we must ensure that this rule matches in the original function!
-Note that the call to \$wfoo is
-            \$wfoo_smW (GHC.Prim.-# ds_Xmb y_amr) wild_Xf
+Note that the call to $wfoo is
+            $wfoo_smW (GHC.Prim.-# ds_Xmb y_amr) wild_Xf
 
 During matching we expand wild_Xf to (Just n_acT).  But then we must also
 expand n_acT to (I# y_amr).  And we can only do that if we look up n_acT
diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index 916654443b..34f2fac56b 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -517,6 +517,7 @@ tc_unify_tys bind_fn unif inj_check match_kis rn_env tv_env cv_env tys1 tys2
        ; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
   where
     env = UMEnv { um_bind_fun = bind_fn
+                , um_skols    = emptyVarSet
                 , um_unif     = unif
                 , um_inj_tf   = inj_check
                 , um_rn_env   = rn_env }
@@ -951,8 +952,8 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco
            CoVarCo cv
              | not (um_unif env)
              , not (cv `elemVarEnv` c_subst)
-             , BindMe <- tvBindFlagL env cv
-             -> do { checkRnEnvRCo env co2
+             , BindMe <- tvBindFlag env cv
+             -> do { checkRnEnv env (tyCoVarsOfCo co2)
                    ; let (co_l, co_r) = decomposeFunCo kco
                       -- cv :: t1 ~ t2
                       -- co2 :: s1 ~ s2
@@ -992,15 +993,18 @@ unify_tys env orig_xs orig_ys
 
 ---------------------------------
 uVar :: UMEnv
-     -> TyVar           -- Variable to be unified
+     -> InTyVar         -- Variable to be unified
      -> Type            -- with this Type
      -> Coercion        -- :: kind tv ~N kind ty
      -> UM ()
 
 uVar env tv1 ty kco
- = do { -- Check to see whether tv1 is refined by the substitution
-        subst <- getTvSubstEnv
-      ; case (lookupVarEnv subst tv1) of
+ = do { -- Apply the ambient renaming
+        let tv1' = umRnOccL env tv1
+
+        -- Check to see whether tv1 is refined by the substitution
+      ; subst <- getTvSubstEnv
+      ; case (lookupVarEnv subst tv1') of
           Just ty' | um_unif env                -- Unifying, so call
                    -> unify_ty env ty' ty kco   -- back into unify
                    | otherwise
@@ -1009,10 +1013,10 @@ uVar env tv1 ty kco
                       -- type, not the template type. So, just check for
                       -- normal type equality.
                       guard ((ty' `mkCastTy` kco) `eqType` ty)
-          Nothing  -> uUnrefined env tv1 ty ty kco } -- No, continue
+          Nothing  -> uUnrefined env tv1' ty ty kco } -- No, continue
 
 uUnrefined :: UMEnv
-           -> TyVar             -- variable to be unified
+           -> OutTyVar          -- variable to be unified
            -> Type              -- with this Type
            -> Type              -- (version w/ expanded synonyms)
            -> Coercion          -- :: kind tv ~N kind ty
@@ -1020,16 +1024,15 @@ uUnrefined :: UMEnv
 
 -- We know that tv1 isn't refined
 
-uUnrefined env tv1 ty2 ty2' kco
+uUnrefined env tv1' ty2 ty2' kco
   | Just ty2'' <- coreView ty2'
-  = uUnrefined env tv1 ty2 ty2'' kco    -- Unwrap synonyms
+  = uUnrefined env tv1' ty2 ty2'' kco    -- Unwrap synonyms
                 -- This is essential, in case we have
                 --      type Foo a = a
                 -- and then unify a ~ Foo a
 
   | TyVarTy tv2 <- ty2'
-  = do { let tv1' = umRnOccL env tv1
-             tv2' = umRnOccR env tv2
+  = do { let tv2' = umRnOccR env tv2
        ; unless (tv1' == tv2' && um_unif env) $ do
            -- If we are unifying a ~ a, just return immediately
            -- Do not extend the substitution
@@ -1038,16 +1041,16 @@ uUnrefined env tv1 ty2 ty2' kco
           -- Check to see whether tv2 is refined
        { subst <- getTvSubstEnv
        ; case lookupVarEnv subst tv2 of
-         {  Just ty' | um_unif env -> uUnrefined env tv1 ty' ty' kco
+         {  Just ty' | um_unif env -> uUnrefined env tv1' ty' ty' kco
          ;  _ ->
 
     do {   -- So both are unrefined
            -- Bind one or the other, depending on which is bindable
-       ; let b1  = tvBindFlagL env tv1
-             b2  = tvBindFlagR env tv2
-             ty1 = mkTyVarTy tv1
+       ; let b1  = tvBindFlag env tv1'
+             b2  = tvBindFlag env tv2'
+             ty1 = mkTyVarTy tv1'
        ; case (b1, b2) of
-           (BindMe, _) -> bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco)
+           (BindMe, _) -> bindTv env tv1' (ty2 `mkCastTy` mkSymCo kco)
            (_, BindMe) | um_unif env
                        -> bindTv (umSwapRn env) tv2 (ty1 `mkCastTy` kco)
 
@@ -1058,12 +1061,12 @@ uUnrefined env tv1 ty2 ty2' kco
            _ -> maybeApart -- See Note [Unification with skolems]
   }}}}
 
-uUnrefined env tv1 ty2 _ kco -- ty2 is not a type variable
-  = case tvBindFlagL env tv1 of
+uUnrefined env tv1' ty2 _ kco -- ty2 is not a type variable
+  = case tvBindFlag env tv1' of
       Skolem -> maybeApart  -- See Note [Unification with skolems]
-      BindMe -> bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco)
+      BindMe -> bindTv env tv1' (ty2 `mkCastTy` mkSymCo kco)
 
-bindTv :: UMEnv -> TyVar -> Type -> UM ()
+bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
 -- OK, so we want to extend the substitution with tv := ty
 -- But first, we must do a couple of checks
 bindTv env tv1 ty2
@@ -1072,7 +1075,7 @@ bindTv env tv1 ty2
         -- Make sure tys mentions no local variables
         -- E.g.  (forall a. b) ~ (forall a. [a])
         -- We should not unify b := [a]!
-        ; checkRnEnvR env free_tvs2
+        ; checkRnEnv env free_tvs2
 
         -- Occurs check, see Note [Fine-grained unification]
         -- Make sure you include 'kco' (which ty2 does) Trac #14846
@@ -1113,12 +1116,27 @@ data BindFlag
 ************************************************************************
 -}
 
-data UMEnv = UMEnv { um_bind_fun :: TyVar -> BindFlag
-                                       -- User-supplied BindFlag function
-                   , um_unif     :: AmIUnifying
-                   , um_inj_tf   :: Bool         -- Checking for injectivity?
-                          -- See (end of) Note [Specification of unification]
-                   , um_rn_env   :: RnEnv2 }
+data UMEnv
+  = UMEnv { um_unif :: AmIUnifying
+
+          , um_inj_tf :: Bool
+            -- Checking for injectivity?
+            -- See (end of) Note [Specification of unification]
+
+          , um_rn_env :: RnEnv2
+            -- Renaming InTyVars to OutTyVars; this eliminates
+            -- shadowing, and lines up matching foralls on the left
+            -- and right
+
+          , um_skols :: TyVarSet
+            -- OutTyVars bound by a forall in this unification;
+            -- Do not bind these in the substitution!
+            -- See the function tvBindFlag
+
+          , um_bind_fun :: TyVar -> BindFlag
+            -- User-supplied BindFlag function,
+            -- for variables not in um_skols
+          }
 
 data UMState = UMState
                    { um_tv_env   :: TvSubstEnv
@@ -1163,15 +1181,10 @@ initUM subst_env cv_subst_env um
     state = UMState { um_tv_env = subst_env
                     , um_cv_env = cv_subst_env }
 
-tvBindFlagL :: UMEnv -> TyVar -> BindFlag
-tvBindFlagL env tv
-  | inRnEnvL (um_rn_env env) tv = Skolem
-  | otherwise                   = um_bind_fun env tv
-
-tvBindFlagR :: UMEnv -> TyVar -> BindFlag
-tvBindFlagR env tv
-  | inRnEnvR (um_rn_env env) tv = Skolem
-  | otherwise                   = um_bind_fun env tv
+tvBindFlag :: UMEnv -> OutTyVar -> BindFlag
+tvBindFlag env tv
+  | tv `elemVarSet` um_skols env = Skolem
+  | otherwise                    = um_bind_fun env tv
 
 getTvSubstEnv :: UM TvSubstEnv
 getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
@@ -1195,18 +1208,22 @@ extendCvEnv cv co = UM $ \state ->
 
 umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
 umRnBndr2 env v1 v2
-  = env { um_rn_env = rnBndr2 (um_rn_env env) v1 v2 }
-
-checkRnEnv :: (RnEnv2 -> VarEnv Var) -> UMEnv -> VarSet -> UM ()
-checkRnEnv get_set env varset = UM $ \ state ->
-  let env_vars = get_set (um_rn_env env) in
-  if isEmptyVarEnv env_vars || (getUniqSet varset `disjointVarEnv` env_vars)
-     -- NB: That isEmptyVarSet is a critical optimization; it
-     -- means we don't have to calculate the free vars of
-     -- the type, often saving quite a bit of allocation.
-  then Unifiable  (state, ())
-  else MaybeApart (state, ())   -- ToDo: why MaybeApart
-                                -- I think SurelyApart would be right
+  = env { um_rn_env = rn_env', um_skols = um_skols env `extendVarSet` v' }
+  where
+    (rn_env', v') = rnBndr2_var (um_rn_env env) v1 v2
+
+checkRnEnv :: UMEnv -> VarSet -> UM ()
+checkRnEnv env varset
+  | isEmptyVarSet skol_vars           = return ()
+  | varset `disjointVarSet` skol_vars = return ()
+  | otherwise                         = maybeApart
+               -- ToDo: why MaybeApart?
+               -- I think SurelyApart would be right
+  where
+    skol_vars = um_skols env
+    -- NB: That isEmptyVarSet guard is a critical optimization;
+    -- it means we don't have to calculate the free vars of
+    -- the type, often saving quite a bit of allocation.
 
 -- | Converts any SurelyApart to a MaybeApart
 don'tBeSoSure :: UM () -> UM ()
@@ -1215,12 +1232,6 @@ don'tBeSoSure um = UM $ \ state ->
     SurelyApart -> MaybeApart (state, ())
     other       -> other
 
-checkRnEnvR :: UMEnv -> VarSet -> UM ()
-checkRnEnvR env fvs = checkRnEnv rnEnvR env fvs
-
-checkRnEnvRCo :: UMEnv -> Coercion -> UM ()
-checkRnEnvRCo env co = checkRnEnv rnEnvR env (tyCoVarsOfCo co)
-
 umRnOccL :: UMEnv -> TyVar -> TyVar
 umRnOccL env v = rnOccL (um_rn_env env) v