[Git][ghc/ghc][wip/t22519] Add stuff to Note

[Richard Eisenberg (@rae)]

Richard Eisenberg pushed to branch wip/t22519 at Glasgow Haskell Compiler / GHC


Commits:
efe7c324 by Richard Eisenberg at 2023-01-02T14:02:25-05:00
Add stuff to Note

- - - - -


2 changed files:

- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Rewrite.hs


Changes:

=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1368,8 +1368,39 @@ which in turn gives us
   [W] a ~R# b
 which is easier to satisfy.
 
-Bottom line: unwrap newtypes before decomposing them!
-c.f. #9123 comment:52,53 for a compelling example.
+We thus must unwrap newtypes before decomposing them. But even this is
+challenging. Here are two cases to consider:
+
+Case 1:
+
+  newtype Age = MkAge Int
+  [G] c
+  [W] w1 :: IO Age ~R# IO Int
+
+Case 2:
+
+  newtype A = MkA [A]
+  [W] A ~R# [A]
+
+For Case 1, recall that IO is an abstract newtype. Then read
+Note [Decomposing newtype equalities]. According to that Note,
+we should not decompose w1, as we have an Irred Given. Yet we still
+want to solve the wanted! So we unwrap the newtypes we can, deeply.
+This is done in the rewriter: GHC.Tc.Solver.Rewrite.rewrite_newtype_app.
+
+Yet for Case 2, deep rewriting would be a disaster: we would loop. Instead,
+here, we just want to unwrap newtypes at the top level, allowing us to
+succeed via Note [Eager reflexivity check].
+
+To satisfy both cases, we unwrap *both* in can_eq_nc' and in the rewriter.
+The former unwraps outer newtypes (when the data constructor is in scope).
+The latter unwraps deeply -- but it won't be invoked in Case 2, when we
+can recognize an equality between the types [A] and [A] before rewriting
+deeply.
+
+This is delicate, but I think we're doomed to do *something* delicate,
+as we're really trying to solve for equirecursive type equality. Bottom
+line for users: recursive newtypes are dangerous.
 
 Note [Eager reflexivity check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -497,6 +497,7 @@ rewrite_one ty@(TyConApp tc tys)
        -- NB: try rewrite_newtype_app even when tc isn't a newtype;
        -- the allows the possibility of having a newtype buried under
        -- a synonym. Needed for e.g. T12067.
+       -- See Note [Unwrap newtypes first] in GHC.Tc.Solver.Canonincal.
          then rewrite_newtype_app ty
 
        -- For * a normal data type application



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/efe7c324435dfabf1ec64088fc9d10e0f1c0a0db
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/20230102/b8d25a43/attachment-0001.html>