Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 7b2d1e6d by Simon Peyton Jones at 2025-05-11T03:24:47-04:00 Refine `noGivenNewtypeReprEqs` to account for quantified constraints This little MR fixes #26020. We are on the edge of completeness for newtype equalities (that doesn't change) but this MR makes GHC a bit more consistent -- and fixes the bug reported. - - - - - 6 changed files: - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - + testsuite/tests/typecheck/should_compile/T26020.hs - + testsuite/tests/typecheck/should_compile/T26020a.hs - + testsuite/tests/typecheck/should_compile/T26020a_help.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -1098,7 +1098,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: them. This is done in can_eq_nc. Of course, we can't unwrap if the data constructor isn't in scope. See Note [Unwrap newtypes first]. -* Incompleteness example (EX2): see #24887 +* Incompleteness example (EX2): prioritise Nominal equalities. See #24887 data family D a data instance D Int = MkD1 (D Char) data instance D Bool = MkD2 (D Char) @@ -1116,7 +1116,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: CONCLUSION: prioritise nominal equalites in the work list. See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet. -* Incompleteness example (EX3): available Givens +* Incompleteness example (EX3): check available Givens newtype Nt a = Mk Bool -- NB: a is not used in the RHS, type role Nt representational -- but the user gives it an R role anyway @@ -1134,36 +1134,41 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: equalities that could later solve it. But what precisely does it mean to say "any Given equalities that could - later solve it"? - - In #22924 we had - [G] f a ~R# a [W] Const (f a) a ~R# Const a a - where Const is an abstract newtype. If we decomposed the newtype, we - could solve. Not-decomposing on the grounds that (f a ~R# a) might turn - into (Const (f a) a ~R# Const a a) seems a bit silly. - - In #22331 we had - [G] N a ~R# N b [W] N b ~R# N a - (where N is abstract so we can't unwrap). Here we really /don't/ want to - decompose, because the /only/ way to solve the Wanted is from that Given - (with a Sym). - - In #22519 we had - [G] a <= b [W] IO Age ~R# IO Int - - (where IO is abstract so we can't unwrap, and newtype Age = Int; and (<=) - is a type-level comparison on Nats). Here we /must/ decompose, despite the - existence of an Irred Given, or we will simply be stuck. (Side note: We - flirted with deep-rewriting of newtypes (see discussion on #22519 and - !9623) but that turned out not to solve #22924, and also makes type - inference loop more often on recursive newtypes.) + later solve it"? It's tricky! + + * In #22924 we had + [G] f a ~R# a [W] Const (f a) a ~R# Const a a + where Const is an abstract newtype. If we decomposed the newtype, we + could solve. Not-decomposing on the grounds that (f a ~R# a) might turn + into (Const (f a) a ~R# Const a a) seems a bit silly. + + * In #22331 we had + [G] N a ~R# N b [W] N b ~R# N a + (where N is abstract so we can't unwrap). Here we really /don't/ want to + decompose, because the /only/ way to solve the Wanted is from that Given + (with a Sym). + + * In #22519 we had + [G] a <= b [W] IO Age ~R# IO Int + + (where IO is abstract so we can't unwrap, and newtype Age = Int; and (<=) + is a type-level comparison on Nats). Here we /must/ decompose, despite the + existence of an Irred Given, or we will simply be stuck. (Side note: We + flirted with deep-rewriting of newtypes (see discussion on #22519 and + !9623) but that turned out not to solve #22924, and also makes type + inference loop more often on recursive newtypes.) + + * In #26020 we had a /quantified/ constraint + forall x. Coercible (N t1) (N t2) + and (roughly) [W] N t1 ~R# N t2 + That quantified constraint can solve the Wanted, so don't decompose! The currently-implemented compromise is this: - - we decompose [W] N s ~R# N t unless there is a [G] N s' ~ N t' - - that is, a Given Irred equality with both sides headed with N. - See the call to noGivenNewtypeReprEqs in canTyConApp. + We decompose [W] N s ~R# N t unless there is + - an Irred [G] N s' ~ N t' + - a quantified [G] forall ... => N s' ~ N t' + that is, a Given equality with both sides headed with N. + See the call to `noGivenNewtypeReprEqs` in `canTyConApp`. This is not perfect. In principle a Given like [G] (a b) ~ (c d), or even just [G] c, could later turn into N s ~ N t. But since the free @@ -1174,7 +1179,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: un-expanded equality superclasses; but only in some very obscure recursive-superclass situations. - Yet another approach (!) is desribed in + Yet another approach (!) is described in Note [Decomposing newtypes a bit more aggressively]. Remember: decomposing Wanteds is always /sound/. This Note is ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -70,7 +70,7 @@ import GHC.Core.Predicate import qualified GHC.Core.TyCo.Rep as Rep import GHC.Core.TyCon import GHC.Core.Class( classTyCon ) -import GHC.Builtin.Names( eqPrimTyConKey, heqTyConKey, eqTyConKey ) +import GHC.Builtin.Names( eqPrimTyConKey, heqTyConKey, eqTyConKey, coercibleTyConKey ) import GHC.Utils.Misc ( partitionWith ) import GHC.Utils.Outputable import GHC.Utils.Panic @@ -1862,21 +1862,34 @@ isOuterTyVar tclvl tv | otherwise = False -- Coercion variables; doesn't much matter noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool --- True <=> there is no Irred looking like (N tys1 ~ N tys2) --- See Note [Decomposing newtype equalities] (EX2) in GHC.Tc.Solver.Equality --- This is the only call site. -noGivenNewtypeReprEqs tc inerts - = not (anyBag might_help (inert_irreds (inert_cans inerts))) +-- True <=> there is no Given looking like (N tys1 ~ N tys2) +-- See Note [Decomposing newtype equalities] (EX3) in GHC.Tc.Solver.Equality +noGivenNewtypeReprEqs tc (IS { inert_cans = inerts }) + | IC { inert_irreds = irreds, inert_insts = quant_cts } <- inerts + = not (anyBag might_help_irred irreds || any might_help_qc quant_cts) + -- Look in both inert_irreds /and/ inert_insts (#26020) where - might_help irred - = case classifyPredType (ctEvPred (irredCtEvidence irred)) of - EqPred ReprEq t1 t2 - | Just (tc1,_) <- tcSplitTyConApp_maybe t1 - , tc == tc1 - , Just (tc2,_) <- tcSplitTyConApp_maybe t2 - , tc == tc2 - -> True - _ -> False + might_help_irred (IrredCt { ir_ev = ev }) + | EqPred ReprEq t1 t2 <- classifyPredType (ctEvPred ev) + = headed_by_tc t1 t2 + | otherwise + = False + + might_help_qc (QCI { qci_body = pred }) + | ClassPred cls [_, t1, t2] <- classifyPredType pred + , cls `hasKey` coercibleTyConKey + = headed_by_tc t1 t2 + | otherwise + = False + + headed_by_tc t1 t2 + | Just (tc1,_) <- tcSplitTyConApp_maybe t1 + , tc == tc1 + , Just (tc2,_) <- tcSplitTyConApp_maybe t2 + , tc == tc2 + = True + | otherwise + = False -- | Is it (potentially) loopy to use the first @ct1@ to solve @ct2@? -- ===================================== testsuite/tests/typecheck/should_compile/T26020.hs ===================================== @@ -0,0 +1,17 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE QuantifiedConstraints #-} + +module T26020 where + +import Data.Kind +import Data.Coerce + +class C r where + data T r :: Type -> Type + +-- type family F r +-- data T r i = MkR r (F i) + +coT :: (forall x. Coercible (T r i) (T r o)) + => T r i -> T r o +coT = coerce ===================================== testsuite/tests/typecheck/should_compile/T26020a.hs ===================================== @@ -0,0 +1,9 @@ +{-# LANGUAGE QuantifiedConstraints #-} +module T26020a where + +import T26020a_help( N ) -- Not the MkN constructor +import Data.Coerce + +coT :: (forall x. Coercible (N i) (N o)) + => N i -> N o +coT = coerce ===================================== testsuite/tests/typecheck/should_compile/T26020a_help.hs ===================================== @@ -0,0 +1,7 @@ +{-# LANGUAGE TypeFamilies #-} + +module T26020a_help where + +type family F a +newtype N a = MkN (F a) + ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -938,3 +938,5 @@ test('T25266a', normal, compile_fail, ['']) test('T25266b', normal, compile, ['']) test('T25597', normal, compile, ['']) test('T25960', normal, compile, ['']) +test('T26020', normal, compile, ['']) +test('T26020a', [extra_files(['T26020a_help.hs'])], multimod_compile, ['T26020a', '-v0']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7b2d1e6d0319dabe5a19b130744f6b5a... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7b2d1e6d0319dabe5a19b130744f6b5a... You're receiving this email because of your account on gitlab.haskell.org.