[GHC] #13959: substTyVar's definition is highly dubious
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Currently, we have: {{{#!hs substTyVar :: TCvSubst -> TyVar -> Type substTyVar (TCvSubst _ tenv _) tv = ASSERT( isTyVar tv ) case lookupVarEnv tenv tv of Just ty -> ty Nothing -> TyVarTy tv }}} But as Richard pointed out to me, the `Nothing` case is flat-out wrong. If `tv` isn't in the substitution, we need to check if any of the variables in `tv`'s kind are in the substitution, and if so, apply the substitution to them. Fixing this might seem straightforward enough: {{{#!diff diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 5ac63e5..4f7d650 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -2191,11 +2191,11 @@ subst_ty subst ty go (CoercionTy co) = CoercionTy $! (subst_co subst co) substTyVar :: TCvSubst -> TyVar -> Type -substTyVar (TCvSubst _ tenv _) tv +substTyVar subst@(TCvSubst _ tenv _) tv = ASSERT( isTyVar tv ) case lookupVarEnv tenv tv of Just ty -> ty - Nothing -> TyVarTy tv + Nothing -> TyVarTy (updateTyVarKind (substTyUnchecked subst) tv) substTyVars :: TCvSubst -> [TyVar] -> [Type] substTyVars subst = map $ substTyVar subst }}} But note that I'm using `substTyUnchecked`, not `substTy`, since if you try using the latter, GHC will pretty quickly fall over on a `./validate --slow` build, as `substTy`'s assertions are violated all over the place. I'm fairly certain I know why the assertions would be tripping up, however. To build most of the in-scope sets used for `substTyVar`'s substitutions, the `mkVarSet :: [Var] -> VarSet` function is used. But `mkVarSet` only grabs the `Unique`s of the type variables themselves, not the variables in the kind of each type variable. This means the in-scope sets will frequently be too narrow to encompass the kind variables, which absolutely must be in the set if we want to change `substTyVar` as described above. I'm not sure what the solution is here. Perhaps we should be using a variant of `mkVarSet` called `mkTyVarSet` that grabs the `Unique`s of the kind variables as well? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Thanks for digging into this further. My question is: where do the arguments to `mkVarSet` come from? Why don't they already have the kind variables in the lists? (They probably should!) My hunch is that the assertion failures you're seeing are genuine -- that is, they suggest real latent bugs. So, I propose this solution: keep digging! :) More concretely, point us to a small sampling (1 might be a suitable small number) of places where this `mkVarSet` call happens, and see if you can describe the context for where that list of variables comes from. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Well looking at the definition of `mkVarSet`, it's no surprise that things are going awry: {{{#!hs mkVarSet :: [Var] -> VarSet mkVarSet = mkUniqSet mkUniqSet :: Uniquable a => [a] -> UniqSet a mkUniqSet = foldl' addOneToUniqSet emptyUniqSet }}} It's just grabbing the `Unique` of each type variable, and nothing more. Experimentally, when I tried a debugging build of GHC with the modified version of `substTyVar`, it fell over trying to compile `Data.Type.Equality`. I don't have the full assertion failure at the moment, but I recall that there were indeed more `tenvFVs` than what were contained in the `in_scope` set. [http://git.haskell.org/ghc.git/blob/1ee49cb11c7ad1af20c117a5395df96ded9a729f... Here's] a sample call to `mkVarSet` that's propagated through to `substTyVars`. This is used in the logic for `GeneralizedNewtypeDeriving`, where we need to take all the type variables mentioned in the instance head in preparation for the substitution that substitutes the class tyvars with the types used when deriving the instance. ...Although now that I think about it, this probably isn't a very good example of the thing we're worried about in this ticket, since that substitution is formed by simply zipping the class tyvars with their instantiated types in the instance, so there's no need to ever substitute in the kind of a tyvar... I think. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Here's a much more detailed stack trace when compiling `Data.Type.Equality`: {{{ $ inplace/bin/ghc-stage2 -fforce-recomp -O2 -DDEBUG -dcore-lint Bug.hs [1 of 1] Compiling Data.Type.Equality ( Bug.hs, Bug.o ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20170712 for x86_64-unknown-linux): ASSERT failed! in_scope InScope {k1_X49O a_X49V b_X49X} tenv [X49T :-> k1_X49O, X49V :-> a_X49V, X49X :-> b_X49X] tenvFVs [X49M :-> k2_X49M, X49O :-> k1_X49O, X49V :-> a_X49V, X49X :-> b_X49X] cenv [] cenvFVs [] tys [*] cos [] Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1188:22 in ghc:Outputable assertPprPanic, called at compiler/types/TyCoRep.hs:2089:56 in ghc:TyCoRep checkValidSubst, called at compiler/types/TyCoRep.hs:2122:29 in ghc:TyCoRep substTy, called at compiler/types/TyCoRep.hs:2198:44 in ghc:TyCoRep Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1186:5 in ghc:Outputable assertPprPanic, called at compiler/types/TyCoRep.hs:2089:56 in ghc:TyCoRep checkValidSubst, called at compiler/types/TyCoRep.hs:2122:29 in ghc:TyCoRep substTy, called at compiler/types/TyCoRep.hs:2198:44 in ghc:TyCoRep CallStack (from -prof): Panic.panic (compiler/utils/Panic.hs:(182,1)-(186,68)) Outputable.pprDebugAndThen (compiler/utils/Outputable.hs:(1191,1)-(1194,43)) ErrUtils.prettyPrintGhcErrors.\ (compiler/main/ErrUtils.hs:(658,23)-(666,44)) GhcMonad.gcatch.\.\ (compiler/main/GhcMonad.hs:117:46-63) Panic.throwGhcException (compiler/utils/Panic.hs:171:1-35) Panic.panicDoc (compiler/utils/Panic.hs:192:1-61) Outputable.pprPanic (compiler/utils/Outputable.hs:1137:1-49) Outputable.assertPprPanic (compiler/utils/Outputable.hs:(1185,1)-(1188,35)) TyCoRep.checkValidSubst (compiler/types/TyCoRep.hs:(2088,1)-(2113,57)) TyCoRep.substTy (compiler/types/TyCoRep.hs:(2120,1)-(2123,45)) Var.updateTyVarKind (compiler/basicTypes/Var.hs:456:1-64) TyCoRep.substTyVar (compiler/types/TyCoRep.hs:(2194,1)-(2198,61)) TyCoRep.subst_ty.go (compiler/types/TyCoRep.hs:(2176,5)-(2191,60)) TyCoRep.subst_ty (compiler/types/TyCoRep.hs:(2173,1)-(2191,60)) TyCoRep.subst_co.go_ty (compiler/types/TyCoRep.hs:2240:5-26) TyCoRep.subst_co.go (compiler/types/TyCoRep.hs:(2243,5)-(2264,66)) TyCoRep.subst_co (compiler/types/TyCoRep.hs:(2236,1)-(2270,36)) TyCoRep.substCoUnchecked (compiler/types/TyCoRep.hs:(2223,1)-(2225,33)) TyCoRep.substCoWithUnchecked (compiler/types/TyCoRep.hs:(2045,1)-(2047,41)) Coercion.mkInstCo (compiler/types/Coercion.hs:(950,1)-(952,31)) CoreOpt.pushCoTyArg.co2 (compiler/coreSyn/CoreOpt.hs:1012:5-62) CoreOpt.pushCoTyArg (compiler/coreSyn/CoreOpt.hs:(990,1)-(1012,62)) Simplify.simplCast.addCoerce (compiler/simplCore/Simplify.hs:(1427,8)-(1461,53)) Simplify.simplCast (compiler/simplCore/Simplify.hs:(1421,1)-(1461,53)) Simplify.rebuildCall (compiler/simplCore/Simplify.hs:(1761,1)-(1853,47)) Simplify.completeCall (compiler/simplCore/Simplify.hs:(1718,1)-(1749,60)) Simplify.simplIdF (compiler/simplCore/Simplify.hs:(1680,1)-(1712,53)) Simplify.simplExprC (compiler/simplCore/Simplify.hs:(1035,1)-(1041,42)) Simplify.simplExpr (compiler/simplCore/Simplify.hs:(1018,1)-(1026,45)) Simplify.simplLam (compiler/simplCore/Simplify.hs:(1501,1)-(1538,37)) Simplify.simplExprF1 (compiler/simplCore/Simplify.hs:(1064,1)-(1140,52)) Simplify.simplExprF (compiler/simplCore/Simplify.hs:(1049,1)-(1059,26)) Simplify.simplLazyBind (compiler/simplCore/Simplify.hs:(381,1)-(432,68)) Simplify.simplBind (compiler/simplCore/Simplify.hs:(362,1)-(368,58)) Simplify.simplRecOrTopPair.trace_bind (compiler/simplCore/Simplify.hs:(330,5)-(334,56)) Simplify.simplRecOrTopPair (compiler/simplCore/Simplify.hs:(321,1)-(334,56)) Simplify.simplTopBinds.simpl_bind (compiler/simplCore/Simplify.hs:(268,5)-(272,65)) Simplify.simplTopBinds.simpl_binds (compiler/simplCore/Simplify.hs:(264,5)-(266,64)) Simplify.simplTopBinds (compiler/simplCore/Simplify.hs:(248,1)-(272,65)) SimplCore.SimplTopBinds (compiler/simplCore/SimplCore.hs:758:29-64) SimplMonad.initSmpl (compiler/simplCore/SimplMonad.hs:(72,1)-(78,36)) SimplCore.simplifyPgmIO.do_iteration (compiler/simplCore/SimplCore.hs:(691,5)-(798,48)) SimplCore.simplifyPgmIO (compiler/simplCore/SimplCore.hs:(658,1)-(800,47)) IOEnv.liftIO (compiler/utils/IOEnv.hs:188:5-33) CoreMonad.liftIO (compiler/simplCore/CoreMonad.hs:615:5-37) CoreMonad.liftIOWithCount (compiler/simplCore/CoreMonad.hs:619:1-87) SimplCore.simplifyPgm (compiler/simplCore/SimplCore.hs:(644,1)-(649,48)) SimplCore.Simplify (compiler/simplCore/SimplCore.hs:456:40-55) SimplCore.doCorePass (compiler/simplCore/SimplCore.hs:(455,1)-(500,50)) SimplCore.runCorePasses.do_pass (compiler/simplCore/SimplCore.hs:(442,5)-(450,28)) SimplCore.runCorePasses (compiler/simplCore/SimplCore.hs:(439,1)-(452,24)) IOEnv.thenM.\ (compiler/utils/IOEnv.hs:(83,37)-(84,60)) IOEnv.thenM (compiler/utils/IOEnv.hs:(83,1)-(84,61)) CoreMonad.>>=.\ (compiler/simplCore/CoreMonad.hs:(524,30)-(528,38)) CoreMonad.>>= (compiler/simplCore/CoreMonad.hs:(524,5)-(528,38)) IOEnv.runIOEnv (compiler/utils/IOEnv.hs:127:1-30) CoreMonad.runCoreM (compiler/simplCore/CoreMonad.hs:(565,1)-(581,63)) SimplCore.core2core (compiler/simplCore/SimplCore.hs:(75,1)-(99,54)) HscTypes.liftIO.\ (compiler/main/HscTypes.hs:245:31-55) HscTypes.liftIO (compiler/main/HscTypes.hs:245:5-55) HscMain.Core2Core (compiler/main/HscMain.hs:1173:7-42) HscMain.hscSimplify' (compiler/main/HscMain.hs:(1170,1)-(1173,42)) HscMain.finish (compiler/main/HscMain.hs:(702,1)-(740,70)) HscTypes.>>=.\ (compiler/main/HscTypes.hs:(240,33)-(242,56)) HscTypes.>>= (compiler/main/HscTypes.hs:(240,5)-(242,56)) HscTypes.runHsc (compiler/main/HscTypes.hs:(251,1)-(254,12)) HscMain.hscIncrementalCompile (compiler/main/HscMain.hs:(644,1)-(690,60)) DriverPipeline.compileOne' (compiler/main/DriverPipeline.hs:(134,1)-(289,55)) GhcMake.upsweep_mod.compile_it_discard_iface (compiler/main/GhcMake.hs:(1436,13)-(1438,61)) GhcMake.upsweep_mod (compiler/main/GhcMake.hs:(1376,1)-(1532,49)) GhcMonad.liftIO (compiler/main/GhcMonad.hs:110:3-30) GhcMake.upsweep.upsweep' (compiler/main/GhcMake.hs:(1245,3)-(1344,91)) GhcMake.upsweep (compiler/main/GhcMake.hs:(1237,1)-(1344,91)) GhcMake.load'.upsweep_fn (compiler/main/GhcMake.hs:(389,9)-(390,41)) GhcMake.load' (compiler/main/GhcMake.hs:(242,1)-(490,38)) GhcMake.load (compiler/main/GhcMake.hs:(234,1)-(236,44)) Main.doMake (ghc/Main.hs:(695,1)-(720,13)) GhcMonad.gcatch.\ (compiler/main/GhcMonad.hs:117:19-63) GhcMonad.gcatch (compiler/main/GhcMonad.hs:(116,3)-(117,63)) ErrUtils.prettyPrintGhcErrors (compiler/main/ErrUtils.hs:(657,1)-(666,44)) Main.main' (ghc/Main.hs:(154,1)-(258,33)) GhcMonad.gmask.\.\.g_restore.\ (compiler/main/GhcMonad.hs:121:65-80) GhcMonad.gmask.\.\.g_restore (compiler/main/GhcMonad.hs:121:33-80) GhcMonad.gmask.\.\ (compiler/main/GhcMonad.hs:(120,30)-(123,53)) Exception.gmask.\ (compiler/utils/Exception.hs:64:27-29) Exception.gmask (compiler/utils/Exception.hs:64:3-30) GhcMonad.gmask.\ (compiler/main/GhcMonad.hs:(119,19)-(123,53)) GhcMonad.gmask (compiler/main/GhcMonad.hs:(118,3)-(123,53)) Exception.gfinally (compiler/utils/Exception.hs:(56,3)-(60,14)) GhcMonad.>>=.\ (compiler/main/GhcMonad.hs:107:26-57) GhcMonad.>>= (compiler/main/GhcMonad.hs:107:3-57) Panic.withSignalHandlers (compiler/utils/Panic.hs:(240,1)-(298,37)) GHC.runGhc (compiler/main/GHC.hs:(440,1)-(445,26)) Exception.gcatch (compiler/utils/Exception.hs:63:3-37) Exception.ghandle (compiler/utils/Exception.hs:73:1-21) GHC.defaultErrorHandler (compiler/main/GHC.hs:(380,1)-(412,7)) Main.main (ghc/Main.hs:(90,1)-(150,64)) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): comment:3 is easy to diagnose: note that the stack includes `substCoWithUnchecked`, but the "uncheckedness" doesn't propagate. Not sure what the best way to fix this is, but the underlying problem is not ours. comment:2 is as you describe: the `inst_tvs` here do ''not'' need to contain the kinds. But the `InScopeSet` surely does! Use `closeOverKinds`. This is a latent bug, as I expected. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): * comment:2: Sorry, I shouldn't have used this example, since it's not actually tripping up the `ASSERT`. In fact, it does close over the kinds of the type variables, which you can see by looking at the [http://git.haskell.org/ghc.git/blob/f656fba19d0cefe05643ddea35d080ea332a6584... definition of zipTvSubst]: {{{#!hs zipTvSubst :: [TyVar] -> [Type] -> TCvSubst zipTvSubst tvs tys | debugIsOn , not (all isTyVar tvs) || neLength tvs tys = pprTrace "zipTvSubst" (ppr tvs $$ ppr tys) emptyTCvSubst | otherwise = mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv where tenv = zipTyEnv tvs tys }}} It uses `tyCoVarsOfTypes` to get the tyvars for the in-scope set, so they will include the necessary kind variables. Phew. * comment:3. Aha! What I should have done is split `substTyVar` into a checked version and an unchecked version, and use the unchecked version in `subst_ty` (`subst_ty` is already using `substTyVarBndrUnchecked` [http://git.haskell.org/ghc.git/blob/f656fba19d0cefe05643ddea35d080ea332a6584... here], so this doesn't make things any less palatable than before). I'll post an update after I've ran `./validate` with this change. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3732 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D3732 Comment: Happily, it passes `./validate`! I also ran `./validate --slow`, and I couldn't observe any //additional// `ASSERT` failures from this change (there were some `ASSERT` failures related to the substitution invariant before and after this chance, but importantly, the number of them remain unchanged with this patch). Since I'm convinced this will just work, I've submitted Phab:D3732 to Phab. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3732 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I differ right at the start! If you look at the corresponding code for term variables you'll see (in `CoreSubst`): {{{ lookupIdSubst :: SDoc -> Subst -> Id -> CoreExpr lookupIdSubst doc (Subst in_scope ids _ _) v | not (isLocalId v) = Var v | Just e <- lookupVarEnv ids v = e | Just v' <- lookupInScope in_scope v = Var v' -- Vital! See Note [Extending the Subst] | otherwise = WARN( True, text "CoreSubst.lookupIdSubst" <+> doc <+> ppr v $$ ppr in_scope) Var v }}} We do ''not'' apply the substition to the type of the `Id` and update its type! Rather, we just look it up in the in-scope set: that should include all in-scope `Id`s; and moreover they are all full-substituted `OutIds`. A consequence is that all occurrences of the `Id` are common'd up to point to a single `Id` data structure, rather than having lots of copies of the `Id`. We should do the same for types. In `substTyVar`, if the var isn't in the `tenv` look in the in-scope set. It should be there. Of course, because we have not yet made all calls to `substTy` have the right in-scope set, we may not find it in the in-scope set. I suppose we can emit a warning, or just silently accept (as of course we are doing right now). Once we've fixed all the calls to `substTy` we should definitely make it a warning. So it's an easy fix. Did you say you'd found other lurking bugs as a result? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3732 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Who arranges for the members of the in-scope set to have substituted kinds? It's not uncommon to start a substitution with some in-scope set (derived from a call to `tyCoVarsOfTypes` or similar) and then build it from there. No one touches the in-scope set. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3732 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Who arranges for the members of the in-scope set to have substituted kinds?
Well, if the in-scope set comes from the context (as in the simplifier or other places) all the `Var`s in the in-scope set are `OutIds`; that is, fully substituted. It would be wrong to substitute again, because it's entirely OK to have a substitution that goes `a :-> [a]`, because the LHS is `InVars` and the RHS is `OutVaers`. (This is not true during unification of course, but that's entirely separate.) E.g. a substitution [a :-> Proxy k (b::k), k :-> *] really means "replace `a` by `Proxy k (b::k)`" and NOT "then apply the subsituton to the result to get `Proxy * (b::*)`. No no no. Substitutions apply exactly once. (In this example the `k` in `Proxy k (b::k)` is an `OutTyVar` whereas the `k` in `k :-> *` is an `InTyVar`.) What if we build the in-scope set by taking the free vars of the range of the substitution? Eg. {{{ Substitute [a :-> Proxy k (b::k)] in the type (a, b) }}} The in-scope set, from the range of the substitution, is {b,k}. Do we need to apply the substitution to {b}? No! The range of the substitution is `OutVars` so we must not apply the substitution to it. A more delicate point is this: what if we build (part of) the in-scope set by taking the free vars of the type being substituted (see `substTyAddInScope` and `Note [The substitution invariant]` in`TyCoRep`? That's an `InType`! eg {{{ Substitute [a :-> Int] in the type (a, b::k) }}} Now we get an in-scope set of `{b::k}`. But although `b` appears in an `InType`, it must be an `OutTyVar` precisely because it is not substituted. It must be bound somewhere outside, and it'd be wrong to substitute its kind at one of its occurrences and not at its binding site! So I think everything is fine. But I really wish I had a clearer way to explain WHY it is fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3732 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): After a long debate, Simon and I came up with the following claim: '''(*) Claim''': If a tyvar is not in the domain of a substitution, then no variables in its kind are in the domain of a substitution. If (*) is true, then the change Phab:D3732 should be a no-op: precisely no behavior should change. And we can check (*) on the fly, which we should. Why should (*) be true? Here's some rough reasoning: a tyvar `a` whose kind mentions `k` must be bound in `k`'s scope. If we are substituting `k` (to `Type`, say), then we'll need to substitute both in `a`'s binding site and `a`'s scope. When we subst in the binding site (with `substTyVarBndr`), the subst is extended mapping `a:k` to `a:Type`; `a` is thus in the domain of the subst when we get to substing in `a`'s scope. If we've forgotten to call `substTyVarBndr`, then we're in deep trouble, anyway. Thus, all tyvars whose kinds mention `k` will be added to the subst by the time we get to their scope. But thinking about (*) led us to ponder this strange scenario: `forall k. forall (b :: k). forall k. forall (a :: k). Proxy [a,b]`. Is that well- kinded? Surely not, because `a` and `b` have different kinds: `a`'s kind is the more local `k` while `b`'s kind is the less local `k`. However, Core Lint is going to have a hard time with this. When Lint looks at `[a,b]`, it will ask for `a`'s kind and get `k`. It will ask for `b`'s kind and get `k`. And the `k`s will be equal! Core Lint will accept. This is horrible. This bug may have been lurking in GHC for ages. The remedy: don't do this. Specifically, we introduce '''(+) Rule''': When a tyvar `a` is brought into scope, all vars (type and term) whose type mentions `a` fall out of scope. Under (+), `b` is not in scope in `[a,b]` and we have a straightforward scoping error. We can check this in Lint. We couldn't quite convince ourselves that (+) is actually always respected during transformations, etc., but by adding a rule in Lint, we can discover when it doesn't. An alternative to (+) is (-) Rule: It is illegal to shadow a variable. That is, if `a` is in scope, we cannot bind `a`. (-) implies (+) and is easy to check for. However, it may not be so easy to uphold; Simon claims several places in GHC knowingly violate (-), and avoiding this violation may hurt performance. I'm worried that any code that violates (-) will sometimes fall afoul of (+) (but only in very obscure scenarios). Simon claims that the violations of (-) but not (+) involve closed types and therefore are safe w.r.t. (+). So we've agreed to check for (+) for now and see how that goes. As a sidenote: comment:7 and comment:9 concern term-level substitutions. At the term level, we have a real interest in commoning up occurrences (so that all occurrences of an Id `x` actually point to the same heap object) because of `IdInfo`. In types, on the other hand, we have an interest in avoiding forcing a `TCvSubst`'s `InScopeSet`, and so we don't use the same "look up in in-scope set" approach. So, essentially, comment:7 and comment:9 are red herrings. == Bottom line == We have these tasks: 1. Check for (*) in `substTyVar`. This is instead of the kind substitution discussed earlier in this ticket. Document (*). 2. Update Core Lint to check (+). Document (+) in a nice Note. 3. (Optional) If we blindly set `no_kind_change` to `False` in `substTyVarBndrCallback`, then substitutions ''will'' common up type variables by looking up type variables in the substitution. There's a chance this will have a performance benefit. Try and investigate. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3732 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Just to add: Rule (+) means that the following program is illegal: {{{ forall (k:*). forall (a:k). forall (k:*->*). a }}} Note the shadowing: there are really two k's. It's illegal according to (+) because bringing the inner `k` into scope makes `a` (as well as the outer `k`) fall out of scope, because `a`'s kind mentions `k`. Why this rule? Because in the implementation we have kinds on every variable occurrence, and the kind on an occurrence should match that on the binder. So {{{ forall (a:*). (a:*) -> Int }}} is fine, but {{{ forall (a:*). T (a:*->*) }}} is not, because the kind on `a`'s occurrence doesn't match that at its binding site. And Rule (+) makes this illegal too: {{{ forall (k:*). forall (a:k). forall (k:*->*). (a:k) }}} because the kind at `a`'s occurrence is a different `k` to that at its binding site. Another way to say it is that `typeKind` (and `exprType`) yield sane results. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * differential: Phab:D3732 => Comment: Removing abandoned Diff. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => new -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Ryan, are you working on this? Or should I add it to my queue? Or does Simon want it? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:14 goldfire]:
Ryan, are you working on this?
No. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm not. Do add it to your queue, Richard. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: (none) => goldfire -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC