[Git][ghc/ghc][master] Check visibility of nested foralls in can_eq_nc (#18863)

[Marge Bot (@marge-bot)]

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
469ff08b by Vladislav Zavialov at 2023-06-15T03:12:57-04:00
Check visibility of nested foralls in can_eq_nc (#18863)

Prior to this change, `can_eq_nc` checked the visibility of the
outermost layer of foralls:

	forall a. forall b. forall c. phi1
	forall x. forall y. forall z. phi2
	        ^^
	     up to here

Then it delegated the rest of the work to `can_eq_nc_forall`, which
split off all foralls:

	forall a. forall b. forall c. phi1
	forall x. forall y. forall z. phi2
	                            ^^
	                         up to here

This meant that some visibility flags were completely ignored.
We fix this oversight by moving the check to `can_eq_nc_forall`.

- - - - -


6 changed files:

- compiler/GHC/Tc/Solver/Equality.hs
- + testsuite/tests/saks/should_fail/T18863c.hs
- + testsuite/tests/saks/should_fail/T18863c.stderr
- + testsuite/tests/saks/should_fail/T18863d.hs
- + testsuite/tests/saks/should_fail/T18863d.stderr
- testsuite/tests/saks/should_fail/all.T


Changes:

=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -388,9 +388,8 @@ can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
   = canTyConApp ev eq_rel both_generative tc1 tys1 tc2 tys2
 
 can_eq_nc _rewritten _rdr_env _envs ev eq_rel
-           s1@(ForAllTy (Bndr _ vis1) _) _
-           s2@(ForAllTy (Bndr _ vis2) _) _
-  | vis1 `eqForAllVis` vis2 -- Note [ForAllTy and type equality]
+           s1 at ForAllTy{} _
+           s2 at ForAllTy{} _
   = can_eq_nc_forall ev eq_rel s1 s2
 
 -- See Note [Canonicalising type applications] about why we require rewritten types
@@ -481,11 +480,12 @@ can_eq_nc_forall ev eq_rel s1 s2
  = do { let free_tvs       = tyCoVarsOfTypes [s1,s2]
             (bndrs1, phi1) = tcSplitForAllTyVarBinders s1
             (bndrs2, phi2) = tcSplitForAllTyVarBinders s2
-      ; if not (equalLength bndrs1 bndrs2)
+            flags1 = binderFlags bndrs1
+            flags2 = binderFlags bndrs2
+      ; if not (all2 eqForAllVis flags1 flags2) -- Note [ForAllTy and type equality]
         then do { traceTcS "Forall failure" $
                      vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
-                          , ppr (binderFlags bndrs1)
-                          , ppr (binderFlags bndrs2) ]
+                          , ppr flags1, ppr flags2 ]
                 ; canEqHardFailure ev s1 s2 }
         else
    do { traceTcS "Creating implication for polytype equality" $ ppr ev


=====================================
testsuite/tests/saks/should_fail/T18863c.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module T18863c where
+
+import Data.Kind
+
+type D :: forall j -> forall i -> (i -> j) -> Type
+data D :: forall j -> forall i.   (i -> j) -> Type


=====================================
testsuite/tests/saks/should_fail/T18863c.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T18863c.hs:10:1: error: [GHC-83865]
+    • Couldn't match expected kind: forall j -> forall i. (i -> j) -> *
+                  with actual kind: forall j i -> (i -> j) -> *
+    • In the data type declaration for ‘D’


=====================================
testsuite/tests/saks/should_fail/T18863d.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module T18863d where
+
+import Data.Kind
+
+type D :: forall j -> forall i.   (i -> j) -> Type
+data D :: forall j -> forall i -> (i -> j) -> Type


=====================================
testsuite/tests/saks/should_fail/T18863d.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T18863d.hs:10:1: error: [GHC-83865]
+    • Couldn't match expected kind: forall j i -> (i -> j) -> *
+                  with actual kind: forall j -> forall i. (i -> j) -> *
+    • In the data type declaration for ‘D’


=====================================
testsuite/tests/saks/should_fail/all.T
=====================================
@@ -33,4 +33,6 @@ test('T16826', normal, compile_fail, [''])
 test('T16756b', normal, compile_fail, [''])
 test('T18863a', normal, compile_fail, [''])
 test('T18863b', normal, compile_fail, [''])
+test('T18863c', normal, compile_fail, [''])
+test('T18863d', normal, compile_fail, [''])
 test('T20916', normal, compile_fail, [''])



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/469ff08b4c56491f42236a5d59fe3e85ee901657
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/20230615/58f097c1/attachment-0001.html>