[Git][ghc/ghc][wip/T22235] Broaden the in-scope sets for liftEnvSubst and composeTCvSubst

[Ryan Scott (@RyanGlScott)]

Ryan Scott pushed to branch wip/T22235 at Glasgow Haskell Compiler / GHC


Commits:
2f8d1e2d by Ryan Scott at 2022-10-23T19:29:46-04:00
Broaden the in-scope sets for liftEnvSubst and composeTCvSubst

This patch fixes two distinct (but closely related) buglets that were uncovered
in #22235:

* `liftEnvSubst` used an empty in-scope set, which was not wide enough to cover
  the variables in the range of the substitution. This patch fixes this by
  populating the in-scope set from the free variables in the range of the
  substitution.
* `composeTCvSubst` applied the first substitution argument to the range of the
  second substitution argument, but the first substitution's in-scope set was
  not wide enough to cover the range of the second substutition. We similarly
  fix this issue in this patch by widening the first substitution's in-scope set
  before applying it.

Fixes #22235.

- - - - -


4 changed files:

- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/TyCo/Subst.hs
- + testsuite/tests/gadt/T22235.hs
- testsuite/tests/gadt/all.T


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -2234,13 +2234,18 @@ liftEnvSubstRight = liftEnvSubst pSnd
 
 liftEnvSubst :: (forall a. Pair a -> a) -> Subst -> LiftCoEnv -> Subst
 liftEnvSubst selector subst lc_env
-  = composeTCvSubst (Subst emptyInScopeSet emptyIdSubstEnv tenv cenv) subst
+  = composeTCvSubst (Subst in_scope emptyIdSubstEnv tenv cenv) subst
   where
     pairs            = nonDetUFMToList lc_env
                        -- It's OK to use nonDetUFMToList here because we
                        -- immediately forget the ordering by creating
                        -- a VarEnv
     (tpairs, cpairs) = partitionWith ty_or_co pairs
+    -- Make sure the in-scope set is wide enough to cover the range of the
+    -- substitution (#22235).
+    in_scope         = mkInScopeSet $
+                       tyCoVarsOfTypes (map snd tpairs) `unionVarSet`
+                       tyCoVarsOfCos (map snd cpairs)
     tenv             = mkVarEnv_Directly tpairs
     cenv             = mkVarEnv_Directly cpairs
 


=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -245,8 +245,14 @@ composeTCvSubst subst1@(Subst is1 ids1 tenv1 cenv1) (Subst is2 _ tenv2 cenv2)
   = Subst is3 ids1 tenv3 cenv3
   where
     is3 = is1 `unionInScope` is2
-    tenv3 = tenv1 `plusVarEnv` mapVarEnv (substTy subst1) tenv2
-    cenv3 = cenv1 `plusVarEnv` mapVarEnv (substCo subst1) cenv2
+    tenv3 = tenv1 `plusVarEnv` mapVarEnv (substTy extended_subst1) tenv2
+    cenv3 = cenv1 `plusVarEnv` mapVarEnv (substCo extended_subst1) cenv2
+    -- Make sure the in-scope set in the first substitution is wide enough to
+    -- cover the free variables in the range of the second substitution before
+    -- applying it (#22235).
+    extended_subst1 =
+      subst1 `extendSubstInScopeSet` tyCoVarsOfTypes (nonDetEltsUFM tenv2)
+             `extendSubstInScopeSet` tyCoVarsOfCos (nonDetEltsUFM cenv2)
 
 emptySubst :: Subst
 emptySubst = Subst emptyInScopeSet emptyVarEnv emptyVarEnv emptyVarEnv


=====================================
testsuite/tests/gadt/T22235.hs
=====================================
@@ -0,0 +1,23 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+module T22235 (f) where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..))
+
+f :: ST x -> ST y -> x :~: y
+f st1 at SMkT st2 at SMkT = method st1 st2
+
+type T :: Type -> Type
+data T a where
+  MkT :: T Int
+
+type ST :: T a -> Type
+data ST (t :: T a) where
+  SMkT :: ST MkT
+
+class C f where
+  method :: f a -> f b -> a :~: b
+
+instance C ST where
+  method SMkT SMkT = Refl


=====================================
testsuite/tests/gadt/all.T
=====================================
@@ -125,3 +125,4 @@ test('T20278', normal, compile, [''])
 test('SynDataRec', normal, compile, [''])
 test('T20485', normal, compile, [''])
 test('T20485a', normal, compile, [''])
+test('T22235', normal, compile, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2f8d1e2dbc62080351b8ce98911a3ea4e3150b1d

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2f8d1e2dbc62080351b8ce98911a3ea4e3150b1d
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/20221023/4e781489/attachment-0001.html>