diff options
| -rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 20 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Types/Constraint.hs | 3 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T22310.hs | 23 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
4 files changed, 41 insertions, 6 deletions
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 6622c67a4b..332d59244a 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/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 } diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 586a6a68aa..ea2a5f7189 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/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.) diff --git a/testsuite/tests/typecheck/should_compile/T22310.hs b/testsuite/tests/typecheck/should_compile/T22310.hs new file mode 100644 index 0000000000..9605a674be --- /dev/null +++ b/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! diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 802eb9097d..c1b10ff6c8 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/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, ['']) |