[Git][ghc/ghc][wip/T22331] 2 commits: Wibble

[Simon Peyton Jones (@simonpj)]

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


Commits:
d2adcb41 by Simon Peyton Jones at 2022-11-25T15:06:58+00:00
Wibble

- - - - -
66270efc by Simon Peyton Jones at 2022-11-25T17:58:10+00:00
Wibble

- - - - -


1 changed file:

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


Changes:

=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1566,11 +1566,15 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
     ty2 = mkTyConApp tc2 tys2
 
      -- See Note [Decomposing TyConApp equalities]
+     -- Note [Decomposing newtypes a bit more aggressively]
     can_decompose inerts
       =  isInjectiveTyCon tc1 (eqRelRole eq_rel)
       || (assert (eq_rel == ReprEq) $
           -- assert: isInjectiveTyCon is always True for Nominal except
-          -- for type synonyms/families, neither of which happen here
+          --   for type synonyms/families, neither of which happen here
+          -- Moreover isInjectiveTyCon is True for Representational
+          --   for algebraic data types.  So we are down to newtypes
+          --   and data families.
           ctEvFlavour ev == Wanted && noGivenIrreds inerts)
 
 {-
@@ -1750,7 +1754,7 @@ newtype in case of 'newtype instance'.
 
 As Note [Decomposing TyConApp equalities] describes, if N is injective
 at role r, we can do this decomposition?
-   [G/W] N ty1 ~r N ty2    to     [G/W]  ty1 ~r' ty2
+   [G/W] (N ty1) ~r (N ty2)    to     [G/W]  ty1 ~r' ty2
 
 For a Given with r=R, the answer is a solid NO: newtypes are not injective at
 representational role, and we must not decompose, or we lose soundness.
@@ -1831,9 +1835,15 @@ IO's argment is representational.  Hence:
      decompose [W] (N s1 .. sn) ~R (N t1 .. tn)
      if the roles of all N's arguments are representational
 
-If N's arguments really /are/ represntational this will not lose completeness.
-But the user might override a phantom role, and then we could (obscurely) get
-incompleteness.  Consider
+If N's arguments really /are/ representational this will not lose
+completeness.  Here "really are representational" means "if you expand
+all newtypes in N's RHS, we'd infer a representational role for each
+of N's type variables in that expansion".  See Note [Role inference]
+in GHC.Tc.TyCl.Utils.
+
+But the user might /override/ a phantom role with an explicit role
+application, and then we could (obscurely) get incompleteness.
+Consider
 
    module A( silly, T ) where
      newtype T a = MkT Int
@@ -1859,6 +1869,9 @@ obscure incompleteness (above).  But no one is reporting a problem from
 the lack of decompostion, so we'll just leave it for now.  This long
 Note is just to record the thinking for our future selves.
 
+Remmber: decomposing Wanteds is always /sound/. This Note is
+only about /completeness/.
+
 Note [Decomposing AppTy equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 For AppTy all the same questions arise as in



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/78053fe547cd25baa8ca49b76903021207540a2a...66270efc9eb95b2162035cd29992ee3550be7679

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/78053fe547cd25baa8ca49b76903021207540a2a...66270efc9eb95b2162035cd29992ee3550be7679
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/20221125/de5672b1/attachment-0001.html>