[Git][ghc/ghc][wip/T23329] Fix type variable substitution in gen_Newtype_fam_insts
Ryan Scott (@RyanGlScott)
gitlab at gitlab.haskell.org
Wed May 3 00:30:46 UTC 2023
Ryan Scott pushed to branch wip/T23329 at Glasgow Haskell Compiler / GHC
Commits:
134d4e65 by Ryan Scott at 2023-05-02T20:23:14-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
@@ -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')
where
- ty' = mkTyVarTy (updateTyVarKind (substTyUnchecked subst) tc_tv)
+ ty' = mkTyVarTy (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/134d4e6583a3c6b0659eeeddd1ab969d47eab42c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/134d4e6583a3c6b0659eeeddd1ab969d47eab42c
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/20230502/e2eb7508/attachment-0001.html>
More information about the ghc-commits
mailing list