uniqAway and collisions

[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.

|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
|  Edward Z. Yang
|  Sent: 06 January 2016 00:50
|  To: Bartosz Nitka <niteria at gmail.com>
|  Cc: ghc-devs Devs <ghc-devs at 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&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
|  >        @~ (<s_Xpw a_Xpz>_N :: s_Xpw a_Xpz ~# s_Xpw a_Xpz)
|  >        @~ (<s_Xpw b_Xpy>_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: <s_Xpw a_Xpz>_N, CO: <s_Xpw
|  b_Xpy>_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 at 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