[Git][ghc/ghc][wip/cfuneqcan-refactor] Introduce canNC
Richard Eisenberg
gitlab at gitlab.haskell.org
Tue Nov 24 20:14:57 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
803bbf04 by Richard Eisenberg at 2020-11-24T15:14:44-05:00
Introduce canNC
- - - - -
3 changed files:
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcType.hs
Changes:
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -92,32 +92,20 @@ last time through, so we can skip the classification step.
canonicalize :: Ct -> TcS (StopOrContinue Ct)
canonicalize (CNonCanonical { cc_ev = ev })
= {-# SCC "canNC" #-}
- case classifyPredType pred of
- ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
- canClassNC ev cls tys
- EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
- canEqNC ev eq_rel ty1 ty2
- IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred)
- canIrred OtherCIS ev
- ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred)
- canForAllNC ev tvs th p
- where
- pred = ctEvPred ev
+ canNC ev
canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
= canForAll ev pend_sc
-canonicalize (CIrredCan { cc_ev = ev, cc_status = status })
- | EqPred eq_rel ty1 ty2 <- classifyPredType (ctEvPred ev)
- = -- For insolubles (all of which are equalities), do /not/ rewrite the arguments
+canonicalize (CIrredCan { cc_ev = ev })
+ = canNC ev
+ -- Instead of rewriting the evidence before classifying, it's possible we
+ -- can make progress without the rewrite. Try this first.
+ -- For insolubles (all of which are equalities), do /not/ rewrite the arguments
-- In #14350 doing so led entire-unnecessary and ridiculously large
-- type function expansion. Instead, canEqNC just applies
-- the substitution to the predicate, and may do decomposition;
-- e.g. a ~ [a], where [G] a ~ [Int], can decompose
- canEqNC ev eq_rel ty1 ty2
-
- | otherwise
- = canIrred status ev
canonicalize (CDictCan { cc_ev = ev, cc_class = cls
, cc_tyargs = xis, cc_pend_sc = pend_sc })
@@ -131,6 +119,20 @@ canonicalize (CEqCan { cc_ev = ev
= {-# SCC "canEqLeafTyVarEq" #-}
canEqNC ev eq_rel (canEqLHSType lhs) rhs
+canNC :: CtEvidence -> TcS (StopOrContinue Ct)
+canNC ev =
+ case classifyPredType pred of
+ ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
+ canClassNC ev cls tys
+ EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
+ canEqNC ev eq_rel ty1 ty2
+ IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred)
+ canIrred ev
+ ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred)
+ canForAllNC ev tvs th p
+ where
+ pred = ctEvPred ev
+
{-
************************************************************************
* *
@@ -694,24 +696,24 @@ See also Note [Evidence for quantified constraints] in GHC.Core.Predicate.
************************************************************************
-}
-canIrred :: CtIrredStatus -> CtEvidence -> TcS (StopOrContinue Ct)
+canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
-- Precondition: ty not a tuple and no other evidence form
-canIrred status ev
+canIrred ev
= do { let pred = ctEvPred ev
; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
; (xi,co) <- rewrite ev pred -- co :: xi ~ pred
; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
do { -- Re-classify, in case rewriting has improved its shape
- -- Code is like the CNonCanonical case of canonicalize, except
+ -- Code is like the canNC, except
-- that the IrredPred branch stops work
; case classifyPredType (ctEvPred new_ev) of
ClassPred cls tys -> canClassNC new_ev cls tys
EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
- ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred)
- canForAllNC ev tvs th p
+ ForAllPred {} -> pprPanic "rewriting revealed a ForAllTy"
+ (ppr ev)
IrredPred {} -> continueWith $
- mkIrredCt status new_ev } }
+ mkIrredCt OtherCIS new_ev } }
{- *********************************************************************
* *
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -1448,7 +1448,7 @@ data TcEvDest
| HoleDest CoercionHole -- ^ fill in this hole with the evidence
-- HoleDest is always used for type-equalities
- -- See Note [Coercion holes] in "GHC.Core.TyCo.Rep"
+ -- See Note [Coercion holes] in GHC.Core.TyCo.Rep
data CtEvidence
= CtGiven -- Truly given, not depending on subgoals
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -83,7 +83,7 @@ module GHC.Tc.Utils.TcType (
isIntegerTy, isNaturalTy,
isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
- isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck,
+ isPredTy, isTyVarClassPred, isInsolubleOccursCheck,
checkValidClsArgs, hasTyVarHead,
isRigidTy,
@@ -2136,18 +2136,6 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
Just (tc, _) -> uniq == getUnique tc
Nothing -> False
--- | Does the given tyvar appear at the head of a chain of applications
--- (a t1 ... tn)
-isTyVarHead :: TcTyVar -> TcType -> Bool
-isTyVarHead tv (TyVarTy tv') = tv == tv'
-isTyVarHead tv (AppTy fun _) = isTyVarHead tv fun
-isTyVarHead tv (CastTy ty _) = isTyVarHead tv ty
-isTyVarHead _ (TyConApp {}) = False
-isTyVarHead _ (LitTy {}) = False
-isTyVarHead _ (ForAllTy {}) = False
-isTyVarHead _ (FunTy {}) = False
-isTyVarHead _ (CoercionTy {}) = False
-
{- Note [AppTy and ReprEq]
~~~~~~~~~~~~~~~~~~~~~~~~~~
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/803bbf04f5df6bb58f8cf05b74c82535184430fe
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/803bbf04f5df6bb58f8cf05b74c82535184430fe
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/20201124/37425dd7/attachment-0001.html>
More information about the ghc-commits
mailing list