[Git][ghc/ghc][wip/t22519] Unwrap newtypes in two places
Richard Eisenberg (@rae)
gitlab at gitlab.haskell.org
Mon Jan 2 18:47:45 UTC 2023
Richard Eisenberg pushed to branch wip/t22519 at Glasgow Haskell Compiler / GHC
Commits:
7fdcf917 by Richard Eisenberg at 2023-01-02T13:47:33-05:00
Unwrap newtypes in two places
- - - - -
2 changed files:
- compiler/GHC/Tc/Solver/Canonical.hs
- testsuite/tests/typecheck/should_fail/T15801.stderr
Changes:
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -34,6 +34,7 @@ import GHC.Core.Reduction
import GHC.Core
import GHC.Types.Id( mkTemplateLocals )
import GHC.Core.FamInstEnv ( FamInstEnvs )
+import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
import GHC.Types.Var
import GHC.Types.Var.Env( mkInScopeSet )
import GHC.Types.Var.Set( delVarSetList, anyVarSet )
@@ -1007,6 +1008,18 @@ can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
| ty1 `tcEqType` ty2
= canEqReflexive ev ReprEq ty1
+-- When working with ReprEq, unwrap newtypes.
+-- See Note [Unwrap newtypes first]
+-- This must be above the TyVarTy case, in order to guarantee (TyEq:N)
+can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+ | ReprEq <- eq_rel
+ , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
+ = can_eq_newtype_nc ev NotSwapped ty1 stuff1 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
+
-- Then, get rid of casts
can_eq_nc' rewritten _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
| isNothing (canEqLHS_maybe ty2) -- See (3) in Note [Equalities with incompatible kinds]
@@ -1036,17 +1049,14 @@ 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 _
- | (eq_rel == NomEq || rewritten)
- -- NomEq: See Note [Unwrap newtypes first]
- -- unwrapping is done in the rewriter, hence the check for `rewritten`
- , Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
+ | 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
-- error messages rather than decomposing into AppTys;
-- 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) _) _
@@ -1068,11 +1078,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].
@@ -1110,6 +1117,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
@@ -1384,6 +1401,34 @@ we do a reflexivity check.
E.] am worried that it would slow down the common case.)
-}
+------------------------
+-- | We're able to unwrap a newtype. Update the bits accordingly.
+can_eq_newtype_nc :: CtEvidence -- ^ :: ty1 ~ ty2
+ -> SwapFlag
+ -> TcType -- ^ ty1
+ -> ((Bag GlobalRdrElt, TcCoercion), TcType) -- ^ :: ty1 ~ ty1'
+ -> TcType -- ^ ty2
+ -> TcType -- ^ ty2, with type synonyms
+ -> TcS (StopOrContinue Ct)
+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:
+ -- See Note [Newtypes can blow the stack]
+ ; checkReductionDepth (ctEvLoc ev) ty1
+
+ -- Next, we record uses of newtype constructors, since coercing
+ -- through newtypes is tantamount to using their constructors.
+ ; recordUsedGREs gres
+
+ ; let redn1 = mkReduction co1 ty1'
+
+ ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
+ redn1
+ (mkReflRedn Representational ps_ty2)
+ ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
+
---------
-- ^ Decompose a type application.
-- All input types must be rewritten. See Note [Canonicalising type applications]
@@ -1458,7 +1503,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)
@@ -1466,13 +1512,15 @@ 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 }
-- See Note [Skolem abstract data] in GHC.Core.Tycon
| tyConSkolem tc1 || tyConSkolem tc2
=====================================
testsuite/tests/typecheck/should_fail/T15801.stderr
=====================================
@@ -1,6 +1,6 @@
T15801.hs:52:10: error: [GHC-18872]
- • Couldn't match representation of type: op_a --> b
- with that of: UnOp op_a -> UnOp b
+ • Couldn't match representation of type: UnOp op_a -> UnOp b
+ with that of: op_a --> b
arising from the superclasses of an instance declaration
• In the instance declaration for ‘OpRíki (Op (*))’
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7fdcf917035e8d17493176adc263fcaf2f930874
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7fdcf917035e8d17493176adc263fcaf2f930874
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/20230102/a9171c29/attachment-0001.html>
More information about the ghc-commits
mailing list