<div dir="ltr"><div>Hi,</div><div><br>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.</div><div><br></div><div>I have 2 questions:</div><div><br></div><div>1. When is it safe to use uniqAway?</div><div><br></div><div>2. Is my conclusion reasonable given this trace: (full trace here [3])?</div><div><br></div><div>I. We start out with (line 123):</div><div><br></div><div>CallStack (from ImplicitParams):</div><div>  pprSTrace, called at compiler/coreSyn/CoreLint.hs:659:12 in ghc:CoreLint</div><div>  e: EqConstr</div><div>       @ (s_Xpw a_Xpz)</div><div>       @ (s_Xpw b_Xpy)</div><div>       @ s_Xpw</div><div>       @ b_Xpy</div><div>       @ a_Xpz</div><div>       @~ (<s_Xpw a_Xpz>_N :: s_Xpw a_Xpz ~# s_Xpw a_Xpz)</div><div>       @~ (<s_Xpw b_Xpy>_N :: s_Xpw b_Xpy ~# s_Xpw b_Xpy)</div><div>       dt_aq3</div><div>  fun: EqConstr</div><div>  args: [TYPE: s_Xpw a_Xpz, TYPE: s_Xpw b_Xpy, TYPE: s_Xpw,</div><div>         TYPE: b_Xpy, TYPE: a_Xpz, CO: <s_Xpw a_Xpz>_N, CO: <s_Xpw b_Xpy>_N,</div><div>         dt_aq3]</div><div>  fun_ty: forall a_apr b_aps (s_Xpw :: * -> *) b_Xpy a_Xpz.</div><div>          (a_apr ~# s_Xpw a_Xpz, b_aps ~# s_Xpw b_Xpy) =></div><div>          EqTypes a_Xpz b_Xpy -> EqTypes a_apr b_aps</div><div><span class="" style="white-space:pre">             </span>  </div><div>II. Then we create s_Xpz with uniqAway (line 499) which has the same unique as a_Xpz above</div><div><br></div><div>CallStack (from ImplicitParams):</div><div>  pprSTrace, called at compiler/types/TyCoRep.hs:1947:5 in ghc:TyCoRep</div><div>  old_var: s_Xpy</div><div>  new_var: s_Xpz</div><div><br></div><div>III. Which causes trouble when we want to substitute s_Xpw for s_Xpz and we substitute a_Xpz as well (line 733):</div><div><br></div><div>CallStack (from ImplicitParams):</div><div>  pprSTrace, called at compiler/coreSyn/CoreLint.hs:813:11 in ghc:CoreLint</div><div>  substTyWith [tv] [arg_ty] body_ty forall b_XpB a_XpD.</div><div>                                    (s_Xpw s_Xpw ~# s_Xpw a_XpD, s_Xpw b_Xpy ~# s_Xpw b_XpB) =></div><div>                                    EqTypes a_XpD b_XpB -> EqTypes (s_Xpw s_Xpw) (s_Xpw b_Xpy)</div><div><span class="" style="white-space:pre">                                                                   </span></div><div><span class="" style="white-space:pre"><br></span></div><div><span class="" style="white-space:pre">The uniqAway comes from substTyVarBndrCallback which blames to nokinds patch.</span></div><div><span class="" style="white-space:pre"><br></span></div><div><span class="" style="white-space:pre">Thanks,</span></div><div><span class="" style="white-space:pre">Bartosz</span></div><div><span class="" style="white-space:pre">                                                                   </span></div><div>[1] <a href="https://phabricator.haskell.org/P77">https://phabricator.haskell.org/P77</a></div><div>[2] <a href="https://phabricator.haskell.org/P76">https://phabricator.haskell.org/P76</a></div><div>[3] <a href="https://phabricator.haskell.org/P78">https://phabricator.haskell.org/P78</a></div></div>