[Git][ghc/ghc][master] TyEq:N assertion: only for saturated applications

[Marge Bot (@marge-bot)]

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


Commits:
b17cfc9c by sheaf at 2022-10-19T10:50:37-04:00
TyEq:N assertion: only for saturated applications

The assertion that checked TyEq:N in canEqCanLHSFinish incorrectly
triggered in the case of an unsaturated newtype TyCon heading the RHS,
even though we can't unwrap such an application. Now, we only trigger
an assertion failure in case of a saturated application of a newtype
TyCon.

Fixes #22310

- - - - -


4 changed files:

- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Types/Constraint.hs
- + testsuite/tests/typecheck/should_compile/T22310.hs
- testsuite/tests/typecheck/should_compile/all.T


Changes:

=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -2032,6 +2032,14 @@ and the Id newtype is unwrapped. This is assured by requiring only rewritten
 types in canEqCanLHS *and* having the newtype-unwrapping check above
 the tyvar check in can_eq_nc.
 
+Note that this only applies to saturated applications of newtype TyCons, as
+we can't rewrite an unsaturated application. See for example T22310, where
+we ended up with:
+
+  newtype Compose f g a = ...
+
+  [W] t[tau] ~# Compose Foo Bar
+
 Note [Put touchable variables on the left]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Ticket #10009, a very nasty example:
@@ -2401,15 +2409,17 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
 
     lhs_ty = canEqLHSType lhs
 
-    -- This is about (TyEq:N): check that we don't have a newtype
-    -- whose constructor is in scope at the top-level of the RHS.
+    -- This is about (TyEq:N): check that we don't have a saturated application
+    -- of a newtype TyCon at the top level of the RHS, if the constructor
+    -- of the newtype is in scope.
     ty_eq_N_OK :: TcS Bool
     ty_eq_N_OK
       | ReprEq <- eq_rel
-      , Just tc <- tyConAppTyCon_maybe rhs
+      , Just (tc, tc_args) <- splitTyConApp_maybe rhs
       , Just con <- newTyConDataCon_maybe tc
-      -- #21010: only a problem if the newtype constructor is in scope
-      -- yet we didn't rewrite it away.
+      -- #22310: only a problem if the newtype TyCon is saturated.
+      , tc_args `lengthAtLeast` tyConArity tc
+      -- #21010: only a problem if the newtype constructor is in scope.
       = do { rdr_env <- getGlobalRdrEnvTcS
            ; let con_in_scope = isJust $ lookupGRE_Name rdr_env (dataConName con)
            ; return $ not con_in_scope }


=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -235,7 +235,8 @@ data Ct
        --   * (TyEq:F) rhs has no foralls
        --       (this avoids substituting a forall for the tyvar in other types)
        --   * (TyEq:K) tcTypeKind lhs `tcEqKind` tcTypeKind rhs; Note [Ct kind invariant]
-       --   * (TyEq:N) If the equality is representational, rhs has no top-level newtype
+       --   * (TyEq:N) If the equality is representational, rhs is not headed by a saturated
+       --     application of a newtype TyCon.
        --     See Note [No top-level newtypes on RHS of representational equalities]
        --     in GHC.Tc.Solver.Canonical. (Applies only when constructor of newtype is
        --     in scope.)


=====================================
testsuite/tests/typecheck/should_compile/T22310.hs
=====================================
@@ -0,0 +1,23 @@
+{-# LANGUAGE GADTs, ScopedTypeVariables, StandaloneKindSignatures #-}
+
+module T22310 where
+
+import Data.Coerce ( coerce )
+import Data.Kind   ( Type )
+
+type Some :: (Type -> Type) -> Type
+data Some t where
+  Some :: t ex -> Some t
+
+type NT :: Type -> Type
+newtype NT f = MkNT ()
+
+oops :: Some NT -> Some NT
+oops = coerce (\(Some @NT x) -> Some x)
+  -- After canonicalisation of Wanted constraints,
+  -- we end up with:
+  --
+  -- [W] t[tau:0] ~R# NT
+  --
+  -- Note the newtype TyCon on the RHS.
+  -- Does not violate TyEq:N, because it is unsaturated!


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -856,3 +856,4 @@ test('DeepSubsumption09', normal, compile, [''])
 test('T21951a', normal, compile, ['-Wredundant-strictness-flags'])
 test('T21951b', normal, compile, ['-Wredundant-strictness-flags'])
 test('T21550', normal, compile, [''])
+test('T22310', normal, compile, [''])



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

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