diff options
author | Richard Eisenberg <rae@richarde.dev> | 2022-12-05 10:14:02 -0500 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2023-01-26 20:06:53 -0500 |
commit | 3e827c3f74ef76d90d79ab6c4e71aa954a1a6b90 (patch) | |
tree | 3fd3c6b74e1c0e226f54ea688c0d633d29570e19 | |
parent | 5640cb1d84d3cce4ce0a9e90d29b2b20d2b38c2f (diff) | |
download | haskell-3e827c3f74ef76d90d79ab6c4e71aa954a1a6b90.tar.gz |
Do newtype unwrapping in the canonicaliser and rewriter
See Note [Unwrap newtypes first], which has the details.
Close #22519.
-rw-r--r-- | compiler/GHC/Core/Coercion.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Tc/Instance/Family.hs | 8 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 151 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 32 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 78 | ||||
-rw-r--r-- | compiler/GHC/Tc/Types.hs | 1 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T22519.hs | 21 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
8 files changed, 215 insertions, 79 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index c7ade006e5..bab53e323b 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -1791,7 +1791,7 @@ topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type) -- -- > topNormaliseNewType_maybe rec_nts ty = Just (co, ty') -- --- then (a) @co : ty ~ ty'@. +-- then (a) @co : ty ~R ty'@. -- (b) ty' is not a newtype. -- -- The function returns @Nothing@ for non-@newtypes@, diff --git a/compiler/GHC/Tc/Instance/Family.hs b/compiler/GHC/Tc/Instance/Family.hs index 8c81e860c5..a555c04a69 100644 --- a/compiler/GHC/Tc/Instance/Family.hs +++ b/compiler/GHC/Tc/Instance/Family.hs @@ -519,16 +519,16 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args = Nothing -- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes, --- potentially looking through newtype /instances/. +-- potentially looking through newtype /instances/ and type synonyms. -- -- It is only used by the type inference engine (specifically, when -- solving representational equality), and hence it is careful to unwrap -- only if the relevant data constructor is in scope. That's why -- it gets a GlobalRdrEnv argument. -- --- It is careful not to unwrap data/newtype instances if it can't --- continue unwrapping. Such care is necessary for proper error --- messages. +-- It is careful not to unwrap data/newtype instances nor synonyms +-- if it can't continue unwrapping. Such care is necessary for proper +-- error messages. -- -- It does not look through type families. -- It does not normalise arguments to a tycon. diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 02ce8115ad..ea2d95e80d 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -61,7 +61,6 @@ import GHC.Types.Basic import qualified Data.Semigroup as S import Data.Bifunctor ( bimap ) -import Data.Foldable ( traverse_ ) {- ************************************************************************ @@ -1085,7 +1084,7 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel -- Decompose type constructor applications -- NB: we have expanded type synonyms already -can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ +can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ | Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1 , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2 -- we want to catch e.g. Maybe Int ~ (Int -> Int) here for better @@ -1093,7 +1092,7 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ -- hence no direct match on TyConApp , not (isTypeFamilyTyCon tc1) , not (isTypeFamilyTyCon tc2) - = canTyConApp ev eq_rel tc1 tys1 tc2 tys2 + = canTyConApp rewritten ev eq_rel tc1 tys1 tc2 tys2 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel s1@(ForAllTy (Bndr _ vis1) _) _ @@ -1115,11 +1114,8 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _ ------------------- -- No similarity in type structure detected. Rewrite and try again. -can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2 - = do { (redn1@(Reduction _ xi1), rewriters1) <- rewrite ev ps_ty1 - ; (redn2@(Reduction _ xi2), rewriters2) <- rewrite ev ps_ty2 - ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2 - ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 } +can_eq_nc' False _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2 + = rewrite_and_try_again ev eq_rel ps_ty1 ps_ty2 ---------------------------- -- Look for a canonical LHS. See Note [Canonical LHS]. @@ -1157,6 +1153,16 @@ can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2 -- No need to call canEqFailure/canEqHardFailure because they -- rewrite, and the types involved here are already rewritten +-- Rewrite the two types and try again +rewrite_and_try_again :: CtEvidence -> EqRel -> TcType -> TcType -> TcS (StopOrContinue Ct) +rewrite_and_try_again ev eq_rel ty1 ty2 + = do { (redn1@(Reduction _ xi1), rewriters1) <- rewrite ev ty1 + ; (redn2@(Reduction _ xi2), rewriters2) <- rewrite ev ty2 + ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2 + ; rdr_env <- getGlobalRdrEnvTcS + ; envs <- getFamInstEnvs + ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 } + {- Note [Unsolved equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If we have an unsolved equality like @@ -1379,45 +1385,84 @@ zonk_eq_types = go combine_rev f (Right tys) (Left elt) = Left (f <$> elt <*> pure tys) combine_rev f (Right tys) (Right ty) = Right (f ty tys) -{- See Note [Unwrap newtypes first] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Unwrap newtypes first] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ See also Note [Decomposing newtype equalities] Consider newtype N m a = MkN (m a) -Then N will get a conservative, Nominal role for its second parameter 'a', +N will get a conservative, Nominal role for its second parameter 'a', because it appears as an argument to the unknown 'm'. Now consider [W] N Maybe a ~R# N Maybe b -If we decompose, we'll get +If we /decompose/, we'll get [W] a ~N# b -But if instead we unwrap we'll get +But if instead we /unwrap/ we'll get [W] Maybe a ~R# Maybe b which in turn gives us [W] a ~R# b which is easier to satisfy. -Bottom line: unwrap newtypes before decomposing them! -c.f. #9123 comment:52,53 for a compelling example. +Conclusion: we must unwrap newtypes before decomposing them. This happens +in `can_eq_newtype_nc` -Note [Newtypes can blow the stack] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have +But even this is challenging. Here are two cases to consider: - newtype X = MkX (Int -> X) - newtype Y = MkY (Int -> Y) +Case 1: + + newtype Age = MkAge Int + [G] c + [W] w1 :: IO Age ~R# IO Int -and now wish to prove +Case 2: - [W] X ~R Y + newtype A = MkA [A] + [W] A ~R# [A] -This Wanted will loop, expanding out the newtypes ever deeper looking -for a solid match or a solid discrepancy. Indeed, there is something -appropriate to this looping, because X and Y *do* have the same representation, -in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized -coercion will ever witness it. This loop won't actually cause GHC to hang, -though, because we check our depth when unwrapping newtypes. +For Case 1, recall that IO is an abstract newtype. Then read Note +[Decomposing newtype equalities]. According to that Note, we should not +decompose w1, because we have an Irred Given. Yet we still want to solve +the wanted! We can do so by unwrapping the (non-abstract) Age newtype +underneath the IO, giving + [W] w2 :: IO Int ~R# IO Int + w1 = (IO unwrap-Age ; w2) +where unwrap-Age :: Age ~R# Int. Now we case solve w2 by reflexivity; +see Note [Eager reflexivity check]. + +Conclusion: unwrap newtypes (deeply, inside types) in the rewriter: +specifically in GHC.Tc.Solver.Rewrite.rewrite_newtype_app. + +Yet for Case 2, deep rewriting would be a disaster: we would loop. + [W] A ~R# [A] ---> {unwrap} + [W] [A] ~R# [[A]] + ---> {decompose} + [W] A ~R# [A] + +In this case, we just want to unwrap newtypes /at the top level/, allowing us +to succeed via Note [Eager reflexivity check]: + [W] A ~R# [A] ---> {unwrap at top level only} + [W] [A] ~R# [A] + ---> {reflexivity} success + +Conclusion: to satisfy Case 1 and Case 2, we unwrap +* /both/ at top level, in can_eq_nc' +* /and/ deeply, in the rewriter, rewrite_newtype_app + +The former unwraps outer newtypes (when the data constructor is in scope). +The latter unwraps deeply -- but it won't be invoked in Case 2, when we can +recognize an equality between the types [A] and [A] before rewriting +deeply. + +This "before" business is delicate -- there is still a real risk of a loop +in the type checker with recursive newtypes -- but I think we're doomed to do +*something* delicate, as we're really trying to solve for equirecursive +type equality. Bottom line for users: recursive newtypes are dangerous. +See also Section 5.3.1 and 5.3.4 of +"Safe Zero-cost Coercions for Haskell" (JFP 2016). + +Another approach -- which we ultimately decided against -- is described in +Note [Decomposing newtypes a bit more aggressively]. Note [Eager reflexivity check] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1462,28 +1507,22 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2 = do { traceTcS "can_eq_newtype_nc" $ vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ] - -- check for blowing our stack: + -- Check for blowing our stack, and increase the depth -- See Note [Newtypes can blow the stack] - ; checkReductionDepth (ctEvLoc ev) ty1 + ; let loc = ctEvLoc ev + ev' = ev `setCtEvLoc` bumpCtLocDepth loc + ; checkReductionDepth loc ty1 -- Next, we record uses of newtype constructors, since coercing -- through newtypes is tantamount to using their constructors. - ; addUsedGREs gre_list - -- If a newtype constructor was imported, don't warn about not - -- importing it... - ; traverse_ keepAlive $ map greMangledName gre_list - -- ...and similarly, if a newtype constructor was defined in the same - -- module, don't warn about it being unused. - -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils. + ; recordUsedGREs gres ; let redn1 = mkReduction co1 ty1' - ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + ; new_ev <- rewriteEqEvidence emptyRewriterSet ev' swapped redn1 (mkReflRedn Representational ps_ty2) ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 } - where - gre_list = bagToList gres --------- -- ^ Decompose a type application. @@ -1559,7 +1598,8 @@ canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2 role = eqRelRole eq_rel ------------------------ -canTyConApp :: CtEvidence -> EqRel +canTyConApp :: Bool -- True <=> the types have been rewritten + -> CtEvidence -> EqRel -> TyCon -> [TcType] -> TyCon -> [TcType] -> TcS (StopOrContinue Ct) @@ -1567,13 +1607,17 @@ canTyConApp :: CtEvidence -> EqRel -- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities] -- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family -- But they can be data families. -canTyConApp ev eq_rel tc1 tys1 tc2 tys2 +canTyConApp rewritten ev eq_rel tc1 tys1 tc2 tys2 | tc1 == tc2 , tys1 `equalLength` tys2 = do { inerts <- getTcSInerts ; if can_decompose inerts then canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2 - else canEqFailure ev eq_rel ty1 ty2 } + else if rewritten + then canEqFailure ev eq_rel ty1 ty2 + else rewrite_and_try_again ev eq_rel ty1 ty2 } + -- Why rewrite and try again? See Case 1 + -- of Note [Unwrap newtypes first] -- See Note [Skolem abstract data] in GHC.Core.Tycon | tyConSkolem tc1 || tyConSkolem tc2 @@ -1851,8 +1895,12 @@ only about /completeness/. Note [Decomposing newtypes a bit more aggressively] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -c.f. https://github.com/ghc-proposals/ghc-proposals/pull/549, -issue #22441, and discussion on !9282. +IMPORTANT: the ideas in this Note are *not* implemented. Instead, the +current approach is detailed in Note [Unwrap newtypes first]. +For more details about the ideas in this Note see + * GHC propoosal: https://github.com/ghc-proposals/ghc-proposals/pull/549 + * issue #22441 + * discussion on !9282. Consider [G] c, [W] (IO Int) ~R (IO Age) where IO is abstract, and @@ -2091,8 +2139,8 @@ canEqHardFailure :: CtEvidence -- See Note [Make sure that insolubles are fully rewritten] canEqHardFailure ev ty1 ty2 = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2) - ; (redn1, rewriters1) <- rewrite ev ty1 - ; (redn2, rewriters2) <- rewrite ev ty2 + ; (redn1, rewriters1) <- rewriteForErrors ev ty1 + ; (redn2, rewriters2) <- rewriteForErrors ev ty2 ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2 ; continueWith (mkIrredCt ShapeMismatchReason new_ev) } @@ -3203,12 +3251,12 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio = do { let new_tm = evCoercion ( mkSymCo lhs_co `mkTransCo` maybeSymCo swapped (mkCoVarCo old_evar) `mkTransCo` rhs_co) - ; newGivenEvVar loc' (new_pred, new_tm) } + ; newGivenEvVar loc (new_pred, new_tm) } | CtWanted { ctev_dest = dest , ctev_rewriters = rewriters } <- old_ev , let rewriters' = rewriters S.<> new_rewriters - = do { (new_ev, hole_co) <- newWantedEq loc' rewriters' + = do { (new_ev, hole_co) <- newWantedEq loc rewriters' (ctEvRole old_ev) nlhs nrhs ; let co = maybeSymCo swapped $ lhs_co @@ -3228,12 +3276,7 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio #endif where new_pred = mkTcEqPredLikeEv old_ev nlhs nrhs - - -- equality is like a type class. Bumping the depth is necessary because - -- of recursive newtypes, where "reducing" a newtype can actually make - -- it bigger. See Note [Newtypes can blow the stack]. loc = ctEvLoc old_ev - loc' = bumpCtLocDepth loc {- ************************************************************************ diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index b5cf81ad9d..b9a9354eff 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -25,7 +25,7 @@ module GHC.Tc.Solver.Monad ( updWorkListTcS, pushLevelNoWorkList, - runTcPluginTcS, addUsedGRE, addUsedGREs, keepAlive, + runTcPluginTcS, recordUsedGREs, matchGlobalInst, TcM.ClsInstResult(..), QCInst(..), @@ -151,7 +151,7 @@ import GHC.Core.TyCon import GHC.Types.Error ( mkPlainError, noHints ) import GHC.Types.Name import GHC.Types.TyThing -import GHC.Types.Name.Reader ( GlobalRdrEnv, GlobalRdrElt ) +import GHC.Types.Name.Reader import GHC.Unit.Module ( HasModule, getModule, extractModule ) import qualified GHC.Rename.Env as TcM @@ -175,7 +175,8 @@ import Control.Monad import GHC.Utils.Monad import Data.IORef import GHC.Exts (oneShot) -import Data.List ( mapAccumL, partition, find ) +import Data.List ( mapAccumL, partition ) +import Data.Foldable #if defined(DEBUG) import GHC.Data.Graph.Directed @@ -1373,17 +1374,22 @@ tcLookupClass c = wrapTcS $ TcM.tcLookupClass c tcLookupId :: Name -> TcS Id tcLookupId n = wrapTcS $ TcM.tcLookupId n --- Setting names as used (used in the deriving of Coercible evidence) --- Too hackish to expose it to TcS? In that case somehow extract the used --- constructors from the result of solveInteract -addUsedGREs :: [GlobalRdrElt] -> TcS () -addUsedGREs gres = wrapTcS $ TcM.addUsedGREs gres +-- Any use of this function is a bit suspect, because it violates the +-- pure veneer of TcS. But it's just about warnings around unused imports +-- and local constructors (GHC will issue fewer warnings than it otherwise +-- might), so it's not worth losing sleep over. +recordUsedGREs :: Bag GlobalRdrElt -> TcS () +recordUsedGREs gres + = do { wrapTcS $ TcM.addUsedGREs gre_list + -- If a newtype constructor was imported, don't warn about not + -- importing it... + ; wrapTcS $ traverse_ (TcM.keepAlive . greMangledName) gre_list } + -- ...and similarly, if a newtype constructor was defined in the same + -- module, don't warn about it being unused. + -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils. -addUsedGRE :: Bool -> GlobalRdrElt -> TcS () -addUsedGRE warn_if_deprec gre = wrapTcS $ TcM.addUsedGRE warn_if_deprec gre - -keepAlive :: Name -> TcS () -keepAlive = wrapTcS . TcM.keepAlive + where + gre_list = bagToList gres -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index 6892e9853f..b4e4b25a29 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -3,7 +3,7 @@ {-# LANGUAGE DeriveFunctor #-} module GHC.Tc.Solver.Rewrite( - rewrite, rewriteArgsNom, + rewrite, rewriteForErrors, rewriteArgsNom, rewriteType ) where @@ -42,6 +42,7 @@ import GHC.Builtin.Types (tYPETyCon) import Data.List ( find ) import GHC.Data.List.Infinite (Infinite) import qualified GHC.Data.List.Infinite as Inf +import GHC.Tc.Instance.Family (tcTopNormaliseNewTypeTF_maybe) {- ************************************************************************ @@ -223,6 +224,22 @@ rewrite ev ty ; traceTcS "rewrite }" (ppr $ reductionReducedType redn) ; return result } +-- | See Note [Rewriting] +-- This variant of 'rewrite' rewrites w.r.t. nominal equality only, +-- as this is better than full rewriting for error messages. Specifically, +-- we want to avoid unwrapping newtypes, as doing so can end up causing +-- an otherwise-unnecessary stack overflow. +rewriteForErrors :: CtEvidence -> TcType + -> TcS (Reduction, RewriterSet) +rewriteForErrors ev ty + = do { traceTcS "rewriteForErrors {" (ppr ty) + ; result@(redn, rewriters) <- + runRewrite (ctEvLoc ev) (ctEvFlavour ev) NomEq (rewrite_one ty) + ; traceTcS "rewriteForErrors }" (ppr $ reductionReducedType redn) + ; return $ case ctEvEqRel ev of + NomEq -> result + ReprEq -> (mkSubRedn redn, rewriters) } + -- See Note [Rewriting] rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS (Reductions, RewriterSet) @@ -482,16 +499,27 @@ rewrite_one (TyVarTy tv) rewrite_one (AppTy ty1 ty2) = rewrite_app_tys ty1 [ty2] -rewrite_one (TyConApp tc tys) +rewrite_one ty@(TyConApp tc tys) -- If it's a type family application, try to reduce it | isTypeFamilyTyCon tc = rewrite_fam_app tc tys - -- For * a normal data type application - -- * data family application - -- we just recursively rewrite the arguments. | otherwise - = rewrite_ty_con_app tc tys + = do { eq_rel <- getEqRel + ; if eq_rel == ReprEq + + then -- Rewriting w.r.t. representational equality requires + -- unwrapping newtypes; see GHC.Tc.Solver.Canonical. + -- Note [Unwrap newtypes first] + -- NB: try rewrite_newtype_app even when tc isn't a newtype; + -- the allows the possibility of having a newtype buried under + -- a synonym. Needed for e.g. T12067. + rewrite_newtype_app ty + + else -- For * a normal data type application + -- * data family application + -- we just recursively rewrite the arguments. + rewrite_ty_con_app tc tys } rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 }) = do { arg_redn <- rewrite_one ty1 @@ -650,7 +678,43 @@ rewrite_vector ki roles tys fvs = tyCoVarsOfType ki {-# INLINE rewrite_vector #-} -{- +-- Rewrite a (potential) newtype application +-- Precondition: the ambient EqRel is ReprEq +-- Precondition: the type is a TyConApp +-- See Note [Newtypes can blow the stack] +rewrite_newtype_app :: TcType -> RewriteM Reduction +rewrite_newtype_app ty@(TyConApp tc tys) + = do { rdr_env <- liftTcS getGlobalRdrEnvTcS + ; tf_envs <- liftTcS getFamInstEnvs + ; case (tcTopNormaliseNewTypeTF_maybe tf_envs rdr_env ty) of + Nothing -> -- Non-newtype or abstract newtype + rewrite_ty_con_app tc tys + + Just ((used_ctors, co), ty') -- co :: ty ~ ty' + -> do { liftTcS $ recordUsedGREs used_ctors + ; checkStackDepth ty + ; rewrite_reduction (Reduction co ty') } } + +rewrite_newtype_app other_ty = pprPanic "rewrite_newtype_app" (ppr other_ty) + +{- Note [Newtypes can blow the stack] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + + newtype X = MkX (Int -> X) + newtype Y = MkY (Int -> Y) + +and now wish to prove + + [W] X ~R Y + +This Wanted will loop, expanding out the newtypes ever deeper looking +for a solid match or a solid discrepancy. Indeed, there is something +appropriate to this looping, because X and Y *do* have the same representation, +in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized +coercion will ever witness it. This loop won't actually cause GHC to hang, +though, because we check our depth when unwrapping newtypes. + Note [Rewriting synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Not expanding synonyms aggressively improves error messages, and diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs index 19c911d01b..5625bad539 100644 --- a/compiler/GHC/Tc/Types.hs +++ b/compiler/GHC/Tc/Types.hs @@ -294,6 +294,7 @@ data RewriteEnv -- ^ At what role are we rewriting? -- -- See Note [Rewriter EqRels] in GHC.Tc.Solver.Rewrite + , re_rewriters :: !(TcRef RewriterSet) -- ^ See Note [Wanteds rewrite Wanteds] } -- RewriteEnv is mostly used in @GHC.Tc.Solver.Rewrite@, but it is defined diff --git a/testsuite/tests/typecheck/should_compile/T22519.hs b/testsuite/tests/typecheck/should_compile/T22519.hs new file mode 100644 index 0000000000..86ab824a1a --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22519.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE Haskell2010 #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module Bug where + +import Data.Coerce (coerce) +import Data.Kind (Type) +import GHC.TypeNats (Nat, type (<=)) + +f :: (1 <= w) + => IO (SymBV' sym w) + -> IO (SymBV sym w) +f = coerce + +---- + +data BaseType = BaseBVType Nat +type family SymExpr (sym :: Type) :: BaseType -> Type +type SymBV sym n = SymExpr sym (BaseBVType n) +newtype SymBV' sym w = MkSymBV' (SymBV sym w) diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index fc5ce4936b..416345e526 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -457,6 +457,7 @@ test('T10335', normal, compile, ['']) test('Improvement', normal, compile, ['']) test('T10009', normal, compile, ['']) test('T10390', normal, compile, ['']) +test('T22519', normal, compile, ['']) test('T8555', normal, compile, ['']) test('T8799', normal, compile, ['']) test('T10432', normal, compile, ['']) |