[Git][ghc/ghc][wip/T23329] Fix type variable substitution in gen_Newtype_fam_insts

Ryan Scott (@RyanGlScott) gitlab at gitlab.haskell.org
Thu May 4 02:06:48 UTC 2023



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


Commits:
78a7d47b by Ryan Scott at 2023-05-03T22:05:13-04:00
Fix type variable substitution in gen_Newtype_fam_insts

Previously, `gen_Newtype_fam_insts` was substituting the type variable binders
of a type family instance using `substTyVars`, which failed to take type
variable dependencies into account. There is similar code in
`GHC.Tc.TyCl.Class.tcATDefault` that _does_ perform this substitution properly,
so this patch:

1. Factors out this code into a top-level `substATBndrs` function, and
2. Uses `substATBndrs` in `gen_Newtype_fam_insts`.

Fixes #23329.

- - - - -


5 changed files:

- compiler/GHC/Tc/Deriv/Generate.hs
- compiler/GHC/Tc/TyCl/Class.hs
- + testsuite/tests/deriving/should_compile/T23329.hs
- + testsuite/tests/deriving/should_compile/T23329_M.hs
- testsuite/tests/deriving/should_compile/all.T


Changes:

=====================================
compiler/GHC/Tc/Deriv/Generate.hs
=====================================
@@ -46,6 +46,7 @@ import GHC.Prelude
 
 import GHC.Hs
 
+import GHC.Tc.TyCl.Class ( substATBndrs )
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Instantiate( newFamInst )
 import GHC.Tc.Utils.Env
@@ -2100,8 +2101,8 @@ gen_Newtype_fam_insts loc' cls inst_tvs inst_tys rhs_ty
         newFamInst SynFamilyInst axiom
       where
         fam_tvs     = tyConTyVars fam_tc
-        rep_lhs_tys = substTyVars lhs_subst fam_tvs
-        rep_rhs_tys = substTyVars rhs_subst fam_tvs
+        (_, rep_lhs_tys) = substATBndrs lhs_subst fam_tvs
+        (_, rep_rhs_tys) = substATBndrs rhs_subst fam_tvs
         rep_rhs_ty  = mkTyConApp fam_tc rep_rhs_tys
         rep_tcvs    = tyCoVarsOfTypesList rep_lhs_tys
         (rep_tvs, rep_cvs) = partition isTyVar rep_tcvs


=====================================
compiler/GHC/Tc/TyCl/Class.hs
=====================================
@@ -22,6 +22,7 @@ module GHC.Tc.TyCl.Class
    , instDeclCtxt2
    , instDeclCtxt3
    , tcATDefault
+   , substATBndrs
    )
 where
 
@@ -42,7 +43,7 @@ import GHC.Tc.Utils.TcType
 import GHC.Tc.Utils.Monad
 import GHC.Tc.TyCl.Build( TcMethInfo )
 
-import GHC.Core.Type     ( piResultTys )
+import GHC.Core.Type     ( extendTvSubstWithClone, piResultTys )
 import GHC.Core.Predicate
 import GHC.Core.Multiplicity
 import GHC.Core.Class
@@ -58,7 +59,7 @@ import GHC.Types.Name
 import GHC.Types.Name.Env
 import GHC.Types.Name.Set
 import GHC.Types.Var
-import GHC.Types.Var.Env
+import GHC.Types.Var.Env ( lookupVarEnv )
 import GHC.Types.SourceFile (HscSource(..))
 import GHC.Types.SrcLoc
 import GHC.Types.Basic
@@ -501,8 +502,7 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
    --            instance C [x]
    -- Then we want to generate the decl:   type F [x] b = ()
   | Just (rhs_ty, _loc) <- defs
-  = do { let (subst', pat_tys') = mapAccumL subst_tv inst_subst
-                                            (tyConTyVars fam_tc)
+  = do { let (subst', pat_tys') = substATBndrs inst_subst (tyConTyVars fam_tc)
              rhs'     = substTyUnchecked subst' rhs_ty
              tcv' = tyCoVarsOfTypesList pat_tys'
              (tv', cv') = partition isTyVar tcv'
@@ -525,14 +525,73 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
   | otherwise  -- defs = Nothing
   = do { warnMissingAT (tyConName fam_tc)
        ; return [] }
+
+-- | Apply a substitution to the type variable binders of an associated type
+-- family. This is used to compute default instances for associated type
+-- families (see 'tcATDefault') as well as @newtype at -derived associated type
+-- family instances (see @gen_Newtype_fam_insts@ in "GHC.Tc.Deriv.Generate").
+--
+-- As a concrete example, consider the following class and associated type
+-- family:
+--
+-- @
+--   class C k (a :: k) where
+--     type F k a (b :: k) :: Type
+--     type F j p q = (Proxy @j p, Proxy @j (q :: j))
+-- @
+--
+-- If a user defines this instance:
+--
+-- @
+-- instance C (Type -> Type) Maybe where {}
+-- @
+--
+-- Then in order to typecheck the default @F@ instance, we must apply the
+-- substitution @[k :-> (Type -> Type), a :-> Maybe]@ to @F@'s binders, which
+-- are @[k, a, (b :: k)]@. The result should look like this:
+--
+-- @
+--   type F (Type -> Type) Maybe (b :: Type -> Type) =
+--     (Proxy @(Type -> Type) Maybe, Proxy @(Type -> Type) (b :: Type -> Type))
+-- @
+--
+-- Making this work requires some care. There are two cases:
+--
+-- 1. If we encounter a type variable in the domain of the substitution (e.g.,
+--    @k@ or @a@), then we apply the substitution directly.
+--
+-- 2. Otherwise, we substitute into the type variable's kind (e.g., turn
+--    @b :: k@ to @b :: Type -> Type@). We then return an extended substitution
+--    where the old @b@ (of kind @k@) maps to the new @b@ (of kind @Type -> Type@).
+--
+--    This step is important to do in case there are later occurrences of @b@,
+--    which we must ensure have the correct kind. Otherwise, we might end up
+--    with @Proxy \@(Type -> Type) (b :: k)@ on the right-hand side of the
+--    default instance, which would be completely wrong.
+--
+-- Contrast 'substATBndrs' function with similar substitution functions:
+--
+-- * 'substTyVars' does not substitute into the kinds of each type variable,
+--   nor does it extend the substitution. 'substTyVars' is meant for occurrences
+--   of type variables, whereas 'substATBndr's is meant for binders.
+--
+-- * 'substTyVarBndrs' does substitute into kinds and extends the substitution,
+--   but it does not apply the substitution to the variables themselves. As
+--   such, 'substTyVarBndrs' returns a list of 'TyVar's rather than a list of
+--   'Type's.
+substATBndrs :: Subst -> [TyVar] -> (Subst, [Type])
+substATBndrs = mapAccumL substATBndr
   where
-    subst_tv subst tc_tv
+    substATBndr :: Subst -> TyVar -> (Subst, Type)
+    substATBndr subst tc_tv
+        -- Case (1) in the Haddocks
       | Just ty <- lookupVarEnv (getTvSubstEnv subst) tc_tv
       = (subst, ty)
+        -- Case (2) in the Haddocks
       | otherwise
-      = (extendTvSubst subst tc_tv ty', ty')
+      = (extendTvSubstWithClone subst tc_tv tc_tv', mkTyVarTy tc_tv')
       where
-        ty' = mkTyVarTy (updateTyVarKind (substTyUnchecked subst) tc_tv)
+        tc_tv' = updateTyVarKind (substTy subst) tc_tv
 
 warnMissingAT :: Name -> TcM ()
 warnMissingAT name


=====================================
testsuite/tests/deriving/should_compile/T23329.hs
=====================================
@@ -0,0 +1,9 @@
+module T23329 where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy(Proxy))
+
+import T23329_M
+
+foo :: ()
+foo = myMethod @Type @MyMaybe @() () Proxy Proxy


=====================================
testsuite/tests/deriving/should_compile/T23329_M.hs
=====================================
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T23329_M where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy)
+
+class MyClass (f :: k -> Type) where
+  type MyTypeFamily f (i :: k) :: Type
+  myMethod :: MyTypeFamily f i -> Proxy f -> Proxy i -> ()
+
+instance MyClass Maybe where
+  type MyTypeFamily Maybe i = ()
+  myMethod = undefined
+
+newtype MyMaybe a = MyMaybe (Maybe a)
+  deriving MyClass


=====================================
testsuite/tests/deriving/should_compile/all.T
=====================================
@@ -141,3 +141,4 @@ test('T20994', normal, compile, [''])
 test('T22167', normal, compile, [''])
 test('T22696a', normal, compile, [''])
 test('T22696c', normal, compile, [''])
+test('T23329', normal, multimod_compile, ['T23329', '-v0'])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/78a7d47bd0523483d5008a131e190d92fa8cd4d8

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/78a7d47bd0523483d5008a131e190d92fa8cd4d8
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/20230503/c17b3e00/attachment-0001.html>


More information about the ghc-commits mailing list