RE: uniqAway and collisions
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:nite...@gmail.com]
Sent: 06 January 2016 14:57
To: Simon Peyton Jones <simo...@microsoft.com>
Cc: Edward Z. Yang <ezy...@mit.edu>; ghc-devs Devs <ghc-devs@haskell.org>
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/TyCoRep.hs;cac0795af33d622e4c6ebae6ae1f206969287088$1591-1601
[2]
https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/coreSyn/CoreLint.hs;cac0795af33d622e4c6ebae6ae1f206969287088$788
[3]
https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/TyCoRep.hs;cac0795af33d622e4c6ebae6ae1f206969287088$1756
[4]
https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/TyCoRep.hs;cac0795af33d622e4c6ebae6ae1f206969287088$1623
2016-01-06 8:42 GMT+00:00 Simon Peyton Jones
<simo...@microsoft.com<mailto:simo...@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.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
RE: uniqAway and collisions
| 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-boun...@haskell.org] On Behalf Of | Edward Z. Yang | Sent: 06 January 2016 00:50 | To: Bartosz Nitka <nite...@gmail.com> | Cc: ghc-devs Devs <ghc-devs@haskell.org> | 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=01%7c01%7csimon | pj%40064d.mgd.microsoft.com%7c9562a48ea0714da096be08d316334bef%7c72f98 | 8bf86f141af91ab2d7cd011db47%7c1=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=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c9562a48ea0714da | 096be08d316334bef%7c72f988bf86f141af91ab2d7cd011db47%7c1=GEAnP46 | gF85287E%2bovF9vH6KmZqqeWGKNjeKvfMXcjA%3d ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
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/TyCoRep.hs;cac0795af33d622e4c6ebae6ae1f206969287088$1591-1601
[2]
https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/coreSyn/CoreLint.hs;cac0795af33d622e4c6ebae6ae1f206969287088$788
[3]
https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/TyCoRep.hs;cac0795af33d622e4c6ebae6ae1f206969287088$1756
[4]
https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/TyCoRep.hs;cac0795af33d622e4c6ebae6ae1f206969287088$1623
2016-01-06 8:42 GMT+00:00 Simon Peyton Jones :
> | 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.
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
uniqAway and collisions
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 http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: uniqAway and collisions
Hello Bartosz, The principle between uniqAway is described in the "Secrets of the GHC Inliner" paper http://research.microsoft.com/en-us/um/people/simonpj/Papers/inlining/ 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 http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
