[Git][ghc/ghc][wip/T16762] Still freshen existentials, though.

[Richard Eisenberg]

Richard Eisenberg pushed to branch wip/T16762 at Glasgow Haskell Compiler / GHC


Commits:
7a777a49 by Richard Eisenberg at 2020-10-09T13:21:06-04:00
Still freshen existentials, though.

- - - - -


2 changed files:

- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Utils/Instantiate.hs


Changes:

=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -837,6 +837,15 @@ between alternatives.
 RIP GADT refinement: refinements have been replaced by the use of explicit
 equality constraints that are used in conjunction with implication constraints
 to express the local scope of GADT refinements.
+
+Note [Freshen existentials]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is essential that these existentials are freshened.
+Otherwise, if we have something like
+  case (a :: Ex, b :: Ex) of (MkEx ..., MkEx ...) -> ...
+we'll give both unpacked existential variables the
+same name, leading to shadowing.
+
 -}
 
 --      Running example:
@@ -887,6 +896,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
 
         ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv ex_tvs
                      -- Get location from monad, not from ex_tvs
+                     -- This freshens: See Note [Freshen existentials]
 
         ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
               -- pat_ty' is type of the actual constructor application
@@ -973,6 +983,8 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
         ; let all_arg_tys = ty : prov_theta ++ (map scaledThing arg_tys)
         ; checkExistentials ex_tvs all_arg_tys penv
         ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
+           -- This freshens: Note [Freshen existentials]
+
         ; let ty'         = substTy tenv ty
               arg_tys'    = substScaledTys tenv arg_tys
               pat_mult    = scaledMult pat_ty


=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -486,7 +486,7 @@ tcInstTypeBndrs id
 
 tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type signature with skolem constants.
--- We could give them fresh names, but no need to do so
+-- This freshens the names, but no need to do so
 tcSkolDFunType dfun
   = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
        ; return (map snd tv_prs, theta, tau) }
@@ -518,20 +518,34 @@ tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
 
 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- See Note [Skolemising type variables]
+-- This version freshens the names and creates "super skolems";
+-- see comments around superSkolemTv.
 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
 
 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- See Note [Skolemising type variables]
+-- This version freshens the names and creates "super skolems";
+-- see comments around superSkolemTv.
 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
 
-tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar]
+tcInstSkolTyVarsPushLevel :: Bool  -- True <=> make "super skolem" AND
+                                   --          freshen names
+                          -> TCvSubst -> [TyVar]
                           -> TcM (TCvSubst, [TcTyVar])
 -- Skolemise one level deeper, hence pushTcLevel
 -- See Note [Skolemising type variables]
-tcInstSkolTyVarsPushLevel overlappable subst tvs
+tcInstSkolTyVarsPushLevel overlappable_and_freshen subst tvs
   = do { tc_lvl <- getTcLevel
        ; let pushed_lvl = pushTcLevel tc_lvl
-       ; return (tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs) }
+       ; if overlappable_and_freshen
+         then freshenTyCoVarsX (mk_skol pushed_lvl) subst tvs
+         else return (tcInstSkolTyVarsAt pushed_lvl overlappable_and_freshen
+                                         subst tvs) }
+  where
+    mk_skol :: TcLevel -> Name -> Kind -> TcTyVar
+    mk_skol lvl nm ki = mkTcTyVar nm ki details
+      where
+        details = SkolemTv lvl overlappable_and_freshen
 
 tcInstSkolTyVarsAt :: TcLevel -> Bool
                    -> TCvSubst -> [TyVar]



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7a777a490038b2c6db8cdaa17ec4af18db5dc619

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7a777a490038b2c6db8cdaa17ec4af18db5dc619
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201009/02270c61/attachment-0001.html>