Relax TyEq:N: allow out-of-scope newtype DataCon

The 'bad_newtype' assertion in GHC.Tc.Solver.Canonical.canEqCanLHSFinish
failed to account for the possibility that the newtype constructor
might not be in scope, in which case we don't provide any guarantees
about canonicalising away a newtype on the RHS of a representational
equality.

Fixes #21010

5 files changed, 69 insertions, 8 deletions

diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index b7c702e5b9..347696f874 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -25,6 +25,7 @@ import GHC.Tc.Solver.InertSet
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.EvTerm
 import GHC.Core.Class
+import GHC.Core.DataCon ( dataConName )
 import GHC.Core.TyCon
 import GHC.Core.Multiplicity
 import GHC.Core.TyCo.Rep   -- cleverly decomposes types, good for completeness checking
@@ -1153,7 +1154,7 @@ can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
 
   | ReprEq <- eq_rel
   , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
-  = can_eq_newtype_nc ev IsSwapped  ty2 stuff2 ty1 ps_ty1
+  = can_eq_newtype_nc ev IsSwapped ty2 stuff2 ty1 ps_ty1
 
 -- Then, get rid of casts
 can_eq_nc' rewritten _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
@@ -2486,7 +2487,10 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
        ; massert (canEqLHSKind lhs `eqType` tcTypeKind rhs)
 
      -- by now, (TyEq:N) is already satisfied (if applicable)
-       ; massert (not bad_newtype)
+       ; assertPprM ty_eq_N_OK $
+           vcat [ text "CanEqCanLHSFinish: (TyEq:N) not satisfied"
+                , text "rhs:" <+> ppr rhs
+                ]
 
      -- guarantees (TyEq:OC), (TyEq:F)
      -- Must do the occurs check even on tyvar/tyvar
@@ -2547,12 +2551,20 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
 
     lhs_ty = canEqLHSType lhs
 
-    -- This is about (TyEq:N)
-    bad_newtype | ReprEq <- eq_rel
-                , Just tc <- tyConAppTyCon_maybe rhs
-                = isNewTyCon tc
-                | otherwise
-                = False
+    -- 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.
+    ty_eq_N_OK :: TcS Bool
+    ty_eq_N_OK
+      | ReprEq <- eq_rel
+      , Just tc <- tyConAppTyCon_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.
+      = do { rdr_env <- getGlobalRdrEnvTcS
+           ; let con_in_scope = isJust $ lookupGRE_Name rdr_env (dataConName con)
+           ; return $ not con_in_scope }
+      | otherwise
+      = return True
 
 -- | Solve a reflexive equality constraint
 canEqReflexive :: CtEvidence    -- ty ~ ty
diff --git a/testsuite/tests/typecheck/should_compile/T21010.hs b/testsuite/tests/typecheck/should_compile/T21010.hs
new file mode 100644
index 0000000000..249d0f12c0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21010.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T21010 ( CBind(..) ) where
+import T21010A ( WrapMono, Constrained(Dom), withMonoCoercible )
+
+class CBind m where
+  (>>-) :: (Dom m a, Dom m b) => m a -> (a -> m b) -> m b
+
+instance CBind (WrapMono ()) where
+  (>>-) = withMonoCoercible undefined
diff --git a/testsuite/tests/typecheck/should_compile/T21010A.hs b/testsuite/tests/typecheck/should_compile/T21010A.hs
new file mode 100644
index 0000000000..234e1c72d7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21010A.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T21010A ( WrapMono, Constrained(..), withMonoCoercible ) where
+import T21010B ( WrapMono(..), withMonoCoercible )
+
+import Data.Kind ( Type, Constraint )
+
+class Constrained (f :: Type -> Type) where
+  type Dom f (a :: Type) :: Constraint
+
+instance Constrained (WrapMono mono) where
+  type Dom (WrapMono mono) b = b ~ mono
diff --git a/testsuite/tests/typecheck/should_compile/T21010B.hs b/testsuite/tests/typecheck/should_compile/T21010B.hs
new file mode 100644
index 0000000000..2a19a7e7e7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21010B.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T21010B where
+import Data.Coerce ( Coercible)
+import Data.Kind   ( Constraint, Type )
+
+newtype WrapFunctor f (a :: Type) = WrapFunctor {runFunctor :: f a}
+
+type role WrapMono representational phantom
+newtype WrapMono mono b = WrapMono mono
+
+withMonoCoercible
+  :: (Coercible (WrapMono mono other) mono => r)
+  -> r
+withMonoCoercible = \x -> x
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index ef13910c41..39878e3ce6 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -810,3 +810,4 @@ test('StaticPtrTypeFamily', normal, compile, [''])
 test('T20946', normal, compile, [''])
 test('T20996', normal, compile, [''])
 test('T20732', normal, compile, [''])
+test('T21010', [extra_files(['T21010A.hs', 'T21010B.hs'])], multimod_compile, ['T21010.hs', '-v0'])