[Git][ghc/ghc][wip/T24984] Wiblbe

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T24984 at Glasgow Haskell Compiler / GHC


Commits:
62ea54a5 by Simon Peyton Jones at 2024-07-26T11:14:31+01:00
Wiblbe

- - - - -


1 changed file:

- compiler/GHC/Tc/Solver/InertSet.hs


Changes:

=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -1057,7 +1057,17 @@ Proving termination of the extended substitution T is suprisingly tricky.
   So we must kick out the inert item, even though (fs>=fw). (KK2b) does this
   by looking for lhs_w under type family applications in rhs_s
 
-Tricky examples in: #19042, #17672
+Tricky examples in: #19042, #17672, #24984. The last (#24984) is particular subtle:
+
+  Inert:   [W] g1: F a0 ~ F a1
+           [W] g2: F a2 ~ F a1
+           [W] g3: F a3 ~ F a1
+
+Now we add [W] g4: F a1 ~ F a7.  Should we kick out g1,g2,g3?  No!  The
+substitution doesn't need to be idempotent, merely terminating.  And in #24984
+it turned out that we kept adding one new constraint and kicking out all the
+previous inert ones (and that rewriting led to exponentially big constraints due
+to lack of contraint sharing.)  So we only want to look /under/ type family applications.
 
 The proof is hard. We start by ignoring flavours. Suppose that:
 * We are adding [lhs_w -fw-> rhs_w] to a well-formed, terminating substitution S.



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/62ea54a56fb6a672397374bfa2361743cd6a2c15

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/62ea54a56fb6a672397374bfa2361743cd6a2c15
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240726/44ac3bed/attachment-0001.html>