uniqAway and collisions

[Edward Z. Yang]

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
>        @~ (<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