| I doubt there's a bug in uniqAway; it's more likely the in scope set | is not correct. I think Edward is probably right here. | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of | Edward Z. Yang | Sent: 06 January 2016 00:50 | To: Bartosz Nitka | Cc: ghc-devs Devs | Subject: Re: uniqAway and collisions | | Hello Bartosz, | | The principle between uniqAway is described in the "Secrets of the GHC | Inliner" paper | | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fresear | ch.microsoft.com%2fen- | us%2fum%2fpeople%2fsimonpj%2fPapers%2finlining%2f&data=01%7c01%7csimon | pj%40064d.mgd.microsoft.com%7c9562a48ea0714da096be08d316334bef%7c72f98 | 8bf86f141af91ab2d7cd011db47%7c1&sdata=D0h2%2btGYDNVaqU8wiKWvq3QA%2bLbz | 6q2BY%2f0IZA9nq%2bk%3d | | I doubt there's a bug in uniqAway; it's more likely the in scope set | is not correct. | | Edward | | Excerpts from Bartosz Nitka's message of 2016-01-05 09:39:54 -0800: | > Hi, | > | > I'm running into core lint issues [1] with my determinism patch [2] | > and they appear to come down to uniqAway coming up with a Unique | > that's already used in the expression. That creates a collision, | > making next substitution substitute more than it needs. | > | > I have 2 questions: | > | > 1. When is it safe to use uniqAway? | > | > 2. Is my conclusion reasonable given this trace: (full trace here | [3])? | > | > I. We start out with (line 123): | > | > CallStack (from ImplicitParams): | > pprSTrace, called at compiler/coreSyn/CoreLint.hs:659:12 in | ghc:CoreLint | > e: EqConstr | > @ (s_Xpw a_Xpz) | > @ (s_Xpw b_Xpy) | > @ s_Xpw | > @ b_Xpy | > @ a_Xpz | > @~ (_N :: s_Xpw a_Xpz ~# s_Xpw a_Xpz) | > @~ (_N :: s_Xpw b_Xpy ~# s_Xpw b_Xpy) | > dt_aq3 | > fun: EqConstr | > args: [TYPE: s_Xpw a_Xpz, TYPE: s_Xpw b_Xpy, TYPE: s_Xpw, | > TYPE: b_Xpy, TYPE: a_Xpz, CO: _N, CO: _N, | > dt_aq3] | > fun_ty: forall a_apr b_aps (s_Xpw :: * -> *) b_Xpy a_Xpz. | > (a_apr ~# s_Xpw a_Xpz, b_aps ~# s_Xpw b_Xpy) => | > EqTypes a_Xpz b_Xpy -> EqTypes a_apr b_aps | > | > II. Then we create s_Xpz with uniqAway (line 499) which has the same | > unique as a_Xpz above | > | > CallStack (from ImplicitParams): | > pprSTrace, called at compiler/types/TyCoRep.hs:1947:5 in | ghc:TyCoRep | > old_var: s_Xpy | > new_var: s_Xpz | > | > III. Which causes trouble when we want to substitute s_Xpw for s_Xpz | > and we substitute a_Xpz as well (line 733): | > | > CallStack (from ImplicitParams): | > pprSTrace, called at compiler/coreSyn/CoreLint.hs:813:11 in | ghc:CoreLint | > substTyWith [tv] [arg_ty] body_ty forall b_XpB a_XpD. | > (s_Xpw s_Xpw ~# s_Xpw a_XpD, | s_Xpw | > b_Xpy ~# s_Xpw b_XpB) => | > EqTypes a_XpD b_XpB -> EqTypes | > (s_Xpw | > s_Xpw) (s_Xpw b_Xpy) | > | > The uniqAway comes from substTyVarBndrCallback which blames to | nokinds | > patch. | > | > Thanks, | > Bartosz | > [1] https://phabricator.haskell.org/P77 | > [2] https://phabricator.haskell.org/P76 | > [3] https://phabricator.haskell.org/P78 | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.h | askell.org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c9562a48ea0714da | 096be08d316334bef%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=GEAnP46 | gF85287E%2bovF9vH6KmZqqeWGKNjeKvfMXcjA%3d

Bartosz Well, I’m glad I wrote that Note. I think you are right on: it looks to me like an outright bug, correctly identified by the Note, that just so happens not to occur in actual code. I’ve elaborated in this new ticket: https://ghc.haskell.org/trac/ghc/ticket/11371 Would you like to work on this? Simon From: Bartosz Nitka [mailto:niteria@gmail.com] Sent: 06 January 2016 14:57 To: Simon Peyton Jones Cc: Edward Z. Yang ; ghc-devs Devs Subject: Re: uniqAway and collisions Hello, Thank you for the paper, it helped with my understanding of how it's supposed to work. Simon, could my issue be related to your comment here: [1]? -- Note [Generating the in-scope set for a substitution] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- If we want to substitute [a -> ty1, b -> ty2] I used to -- think it was enough to generate an in-scope set that includes -- fv(ty1,ty2). But that's not enough; we really should also take the -- free vars of the type we are substituting into! Example: -- (forall b. (a,b,x)) [a -> List b] -- Then if we use the in-scope set {b}, there is a danger we will rename -- the forall'd variable to 'x' by mistake, getting this: -- (forall x. (List b, x, x) -- Urk! This means looking at all the calls to mkOpenTvSubst.... Currently the InScope set only contains the free variables of the arguments when linting type application [2][3][4] and doesn't contain the free variables of the body that it's substituting in. The definition of substTyWith is: substTyWith :: [TyVar] -> [Type] -> Type -> Type substTyWith tvs tys = ASSERT( length tvs == length tys ) substTy (zipOpenTCvSubst tvs tys) When I changed it to include the free variables of the body my core lint error went away: substTyWith :: [TyVar] -> [Type] -> Type -> Type substTyWith tvs tys ty = ASSERT( length tvs == length tys ) substTy (extendTCvInScopeList (zipOpenTCvSubst tvs tys) (tyCoVarsOfTypeList ty)) ty It seems unlikely to me that this is the issue, since this code is very old, but I don't have a better explanation for this and a second pair of eyes would help. Thank you, Bartosz [1] https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/T... [2] https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/coreSyn... [3] https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/T... [4] https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/T... 2016-01-06 8:42 GMT+00:00 Simon Peyton Jones mailto:simonpj@microsoft.com>: | I doubt there's a bug in uniqAway; it's more likely the in scope set | is not correct. I think Edward is probably right here.