[Git][ghc/ghc][wip/cfuneqcan-refactor] 2 commits: Fix error output
Richard Eisenberg
gitlab at gitlab.haskell.org
Tue Nov 10 14:54:54 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
81480c41 by Richard Eisenberg at 2020-11-09T14:23:08-05:00
Fix error output
- - - - -
6a4ca962 by Richard Eisenberg at 2020-11-10T09:54:32-05:00
Reimplement flatten_exact_fam_app
Hopefully will be faster?
- - - - -
5 changed files:
- compiler/GHC/Data/Maybe.hs
- compiler/GHC/Tc/Solver/Flatten.hs
- compiler/GHC/Tc/Solver/Monad.hs
- testsuite/tests/patsyn/should_fail/T11010.stderr
- testsuite/tests/roles/should_compile/Roles3.stderr
Changes:
=====================================
compiler/GHC/Data/Maybe.hs
=====================================
@@ -16,7 +16,7 @@ module GHC.Data.Maybe (
failME, isSuccess,
orElse,
- firstJust, firstJusts,
+ firstJust, firstJusts, firstJustsM,
whenIsJust,
expectJust,
rightToMaybe,
@@ -31,6 +31,7 @@ import Control.Monad
import Control.Monad.Trans.Maybe
import Control.Exception (catch, SomeException(..))
import Data.Maybe
+import Data.Foldable ( foldlM )
import GHC.Utils.Misc (HasCallStack)
infixr 4 `orElse`
@@ -51,6 +52,15 @@ firstJust a b = firstJusts [a, b]
firstJusts :: [Maybe a] -> Maybe a
firstJusts = msum
+-- | Takes computations returnings @Maybes@; tries each one in order.
+-- The first one to return a @Just@ wins. Returns @Nothing@ if all computations
+-- return @Nothing at .
+firstJustsM :: (Monad m, Foldable f) => f (m (Maybe a)) -> m (Maybe a)
+firstJustsM = foldlM go Nothing where
+ go :: Monad m => Maybe a -> m (Maybe a) -> m (Maybe a)
+ go Nothing action = action
+ go result@(Just _) _action = return result
+
expectJust :: HasCallStack => String -> Maybe a -> a
{-# INLINE expectJust #-}
expectJust _ (Just x) = x
=====================================
compiler/GHC/Tc/Solver/Flatten.hs
=====================================
@@ -31,6 +31,7 @@ import GHC.Utils.Panic
import GHC.Tc.Solver.Monad as TcS
import GHC.Utils.Misc
+import GHC.Data.Maybe
import Control.Monad
import GHC.Utils.Monad ( zipWith3M )
import Data.List.NonEmpty ( NonEmpty(..) )
@@ -748,7 +749,6 @@ so those families can get reduced.
flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
-- flatten_fam_app can be over-saturated
- -- flatten_exact_fam_app is exactly saturated
-- flatten_exact_fam_app_fully lifts out the application to top level
-- Postcondition: Coercion :: Xi ~ F tys
flatten_fam_app tc tys -- Can be over-saturated
@@ -769,6 +769,92 @@ flatten_fam_app tc tys -- Can be over-saturated
-- See note [flatten_exact_fam_app_fully performance]
flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
flatten_exact_fam_app_fully tc tys
+ = do { checkStackDepth (mkTyConApp tc tys)
+
+ -- Step 1. Try to reduce without reducing arguments first.
+ ; result1 <- try_to_reduce tc tys
+ ; case result1 of
+ { Just (co, xi) -> finish (xi, co)
+ ; Nothing ->
+
+ -- That didn't work. So reduce the arguments.
+ do { (xis, cos, kind_co) <- flatten_args_tc tc (repeat Nominal) tys
+ -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys)
+
+ ; eq_rel <- getEqRel
+ ; let role = eqRelRole eq_rel
+ args_co = mkTyConAppCo role tc cos
+ -- args_co :: F xis ~r F tys
+
+ homogenise :: TcType -> TcCoercion -> (TcType, TcCoercion)
+ -- in (xi', co') = homogenise xi co
+ -- assume co :: xi ~r F xis, co is homogeneous
+ -- then xi' :: tcTypeKind(F tys)
+ -- and co' :: xi' ~r F tys, which is homogeneous
+ homogenise xi co = (casted_xi, final_co)
+ where
+ casted_xi = xi `mkCastTy` kind_co
+ -- casted_xi :: tcTypeKind(F tys)
+ homo_co = mkTcGReflLeftCo role xi kind_co
+ -- homo_co :: casted_xi ~r xi
+
+ final_co = homo_co `mkTcTransCo` co `mkTcTransCo` args_co
+
+ ; result2 <- liftTcS $ lookupFamAppInert tc xis
+ ; flavour <- getFlavour
+ ; case result2 of
+ { Just (co, xi, fr@(_, inert_eq_rel))
+ -- co :: F xis ~ir xi
+
+ | fr `eqCanRewriteFR` (flavour, eq_rel) ->
+ do { traceFlat "flatten/flat-cache hit" (ppr tc <+> ppr xis $$ ppr xi)
+ ; finish (homogenise xi downgraded_co) }
+ where
+ inert_role = eqRelRole inert_eq_rel
+ role = eqRelRole eq_rel
+ downgraded_co = tcDowngradeRole role inert_role (mkTcSymCo co)
+ -- downgraded_co :: xi ~r F xis
+
+ ; _ ->
+
+ -- inert didn't work. Try to reduce again
+ do { result3 <- try_to_reduce tc xis
+ ; case result3 of
+ Just (co, xi) -> finish (homogenise xi co)
+ Nothing -> return (homogenise reduced (mkTcReflCo role reduced))
+ where
+ reduced = mkTyConApp tc xis }}}}}
+ where
+ -- call this if the above attempts made progress.
+ -- This recursively flattens the result and then adds to the cache
+ finish :: (Xi, Coercion) -> FlatM (Xi, Coercion)
+ finish (xi, co) = do { (fully, fully_co) <- bumpDepth $ flatten_one xi
+ ; let final_co = fully_co `mkTcTransCo` co
+ ; eq_rel <- getEqRel
+ ; flavour <- getFlavour
+ ; when (eq_rel == NomEq && flavour /= Derived) $ -- the cache only wants Nominal eqs
+ liftTcS $ extendFamAppCache tc tys (final_co, fully)
+ ; return (fully, final_co) }
+
+-- Returned coercion is output ~r input, where r is the role in the FlatM monad
+try_to_reduce :: TyCon -> [TcType] -> FlatM (Maybe (TcCoercion, TcType))
+try_to_reduce tc tys
+ = do { flavour <- getFlavour
+ ; result <- liftTcS $ firstJustsM [ lookupFamAppCache flavour tc tys
+ , matchFam tc tys ]
+ ; downgrade result }
+ where
+ downgrade :: Maybe (TcCoercionN, TcType) -> FlatM (Maybe (TcCoercion, TcType))
+ downgrade Nothing = return Nothing
+ downgrade (Just (co, xi))
+ = do { traceFlat "Eager T.F. reduction success" $
+ vcat [ ppr tc, ppr tys, ppr xi
+ , ppr co <+> dcolon <+> ppr (coercionKind co)
+ ]
+ ; role <- getRole
+ ; return (Just (tcDowngradeRole role Nominal co, xi)) }
+
+{- "RAE"
-- See Note [Reduce type family applications eagerly]
-- the following tcTypeKind should never be evaluated, as it's just used in
-- casting, and casts by refl are dropped
@@ -872,9 +958,8 @@ flatten_exact_fam_app_fully tc tys
; eq_rel <- getEqRel
; let co = maybeTcSubCo eq_rel norm_co
`mkTransCo` mkSymCo final_co
- ; flavour <- getFlavour
- -- NB: only extend cache with nominal, given equalities
- ; when (eq_rel == NomEq && flavour == Given) $
+ -- NB: only extend cache with nominal equalities
+ ; when (eq_rel == NomEq) $
liftTcS $ extendFamAppCache tc tys (co, xi)
; let role = eqRelRole eq_rel
xi' = xi `mkCastTy` kind_co
@@ -899,9 +984,12 @@ flatten_exact_fam_app_fully tc tys
`mkTransCo` mkSymCo final_co)
; return $ Just (xi, co) }
Nothing -> pure Nothing }
+-}
{- Note [Reduce type family applications eagerly]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+"RAE": Update Note.
+
If we come across a type-family application like (Append (Cons x Nil) t),
then, rather than flattening to a skolem etc, we may as well just reduce
it on the spot to (Cons x t). This saves a lot of intermediate steps.
@@ -943,6 +1031,8 @@ have any knowledge as to *why* these facts are true.
Note [Runaway Derived rewriting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+"RAE": Remove. We do occurs-checking now.
+
Suppose we have
[WD] F a ~ T (F a)
We *don't* want to fall into a hole using that to rewrite a Derived
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -91,7 +91,7 @@ module GHC.Tc.Solver.Monad (
foldIrreds,
-- The flattening cache
- lookupFamApp, extendFamAppCache,
+ lookupFamAppInert, lookupFamAppCache, extendFamAppCache,
pprKicked,
-- Inert function equalities
@@ -189,6 +189,7 @@ import Data.List ( partition, mapAccumL )
import qualified Data.Semigroup as S
import Data.List.NonEmpty ( NonEmpty(..), cons, toList, nonEmpty )
import qualified Data.List.NonEmpty as NE
+import Control.Arrow ( first )
#if defined(DEBUG)
import GHC.Data.Graph.Directed
@@ -404,13 +405,15 @@ data InertSet
, inert_famapp_cache :: FunEqMap (TcCoercion, TcType)
-- If F tys :-> (co, rhs, flav),
- -- then co :: F tys ~ rhs
- -- flav is [G]
+ -- then co :: rhs ~ F tys
+ --
+ -- Some entries in the cache might have arisen from Wanteds, and
+ -- so this should be used only for rewriting Wanteds.
--
-- Just a hash-cons cache for use when reducing family applications
-- only
--
- -- Only nominal, Given equalities end up in here (along with
+ -- Only nominal equalities end up in here (along with
-- top-level instances)
, inert_solved_dicts :: DictMap CtEvidence
@@ -2368,13 +2371,12 @@ removeInertCt is ct =
CIrredCan {} -> panic "removeInertCt: CIrredEvCan"
CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
--- | Looks up a family application in both the inerts and the famapp-cache
-lookupFamApp :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavourRole))
-lookupFamApp fam_tc tys
- = do { IS { inert_famapp_cache = famapp_cache
- , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
- ; return (firstJusts [lookup_inerts inert_funeqs,
- lookup_famapps famapp_cache]) }
+-- | Looks up a family application in the inerts; returned coercion
+-- is oriented input ~ output
+lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavourRole))
+lookupFamAppInert fam_tc tys
+ = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
+ ; return (lookup_inerts inert_funeqs) }
where
lookup_inerts inert_funeqs
| Just (EqualCtList (CEqCan { cc_ev = ctev, cc_rhs = rhs } :| _))
@@ -2382,11 +2384,12 @@ lookupFamApp fam_tc tys
= Just (ctEvCoercion ctev, rhs, ctEvFlavourRole ctev)
| otherwise = Nothing
- lookup_famapps famapp_cache
- | Just (co, rhs) <- findFunEq famapp_cache fam_tc tys
- = Just (co, rhs, (Given, NomEq))
- | otherwise = Nothing
-
+lookupFamAppCache :: CtFlavour -> TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
+lookupFamAppCache Given _ _ = return Nothing
+ -- the famapp_cache contains some wanteds. Not appropriate to rewrite a Given.
+lookupFamAppCache _ fam_tc tys
+ = do { IS { inert_famapp_cache = famapp_cache } <- getTcSInerts
+ ; return (findFunEq famapp_cache fam_tc tys) }
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
@@ -3209,6 +3212,7 @@ zonkTyCoVarKind tv = wrapTcS (TcM.zonkTyCoVarKind tv)
----------------------------
extendFamAppCache :: TyCon -> [Type] -> (TcCoercion, TcType) -> TcS ()
+-- NB: co :: rhs ~ F tys, to match expectations of flattener
extendFamAppCache tc xi_args stuff@(_, ty)
= do { dflags <- getDynFlags
; when (gopt Opt_FamAppCache dflags) $
@@ -3489,8 +3493,8 @@ checkReductionDepth loc ty
solverDepthErrorTcS loc ty }
matchFam :: TyCon -> [Type] -> TcS (Maybe (CoercionN, TcType))
--- Given (F tys) return (ty, co), where co :: F tys ~N ty
-matchFam tycon args = wrapTcS $ matchFamTcM tycon args
+-- Given (F tys) return (ty, co), where co :: ty ~N F tys
+matchFam tycon args = fmap (fmap (first mkTcSymCo)) $ wrapTcS $ matchFamTcM tycon args
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (CoercionN, TcType))
-- Given (F tys) return (ty, co), where co :: F tys ~N ty
=====================================
testsuite/tests/patsyn/should_fail/T11010.stderr
=====================================
@@ -1,5 +1,5 @@
-T11010.hs:9:36: error:
+T11010.hs:9:34: error:
• Could not deduce: a1 ~ Int
from the context: a ~ Int
bound by the signature for pattern synonym ‘IntFun’
=====================================
testsuite/tests/roles/should_compile/Roles3.stderr
=====================================
@@ -21,7 +21,7 @@ COERCION AXIOMS
axiom Roles3.N:C3 :: C3 a b = a -> F3 b -> F3 b
axiom Roles3.N:C4 :: C4 a b = a -> F4 b -> F4 b
Dependent modules: []
-Dependent packages: [base-4.15.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
+Dependent packages: [base-4.16.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
==================== Typechecker ====================
Roles3.$tcC4
@@ -48,20 +48,18 @@ Roles3.$tc'C:C1
= GHC.Types.TyCon
4508088879886988796## 13962145553903222779## Roles3.$trModule
(GHC.Types.TrNameS "'C:C1"#) 1 $krep
-$krep [InlPrag=NOUSERINLINE[~]] = GHC.Types.KindRepVar 0
-$krep [InlPrag=NOUSERINLINE[~]] = GHC.Types.KindRepVar 1
-$krep [InlPrag=NOUSERINLINE[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=NOUSERINLINE[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=NOUSERINLINE[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=NOUSERINLINE[~]]
- = GHC.Types.KindRepFun GHC.Types.krep$* $krep
-$krep [InlPrag=NOUSERINLINE[~]]
- = GHC.Types.KindRepFun GHC.Types.krep$* $krep
-$krep [InlPrag=NOUSERINLINE[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=NOUSERINLINE[~]]
+$krep [InlPrag=[~]] = GHC.Types.KindRepVar 0
+$krep [InlPrag=[~]] = GHC.Types.KindRepVar 1
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]]
= GHC.Types.KindRepTyConApp GHC.Types.$tcConstraint []
-$krep [InlPrag=NOUSERINLINE[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=NOUSERINLINE[~]]
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]]
= GHC.Types.KindRepTyConApp
GHC.Types.$tc~ ((:) GHC.Types.krep$* ((:) $krep ((:) $krep [])))
$krep [InlPrag=[~]]
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a97a29b2f471d15fbfbc6572debdbde4c056e637...6a4ca962c448cba22b2a3f6c870a769f254f9ce1
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a97a29b2f471d15fbfbc6572debdbde4c056e637...6a4ca962c448cba22b2a3f6c870a769f254f9ce1
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/20201110/97b2480b/attachment-0001.html>
More information about the ghc-commits
mailing list