summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRichard Eisenberg <rae@richarde.dev>2020-11-25 15:00:36 -0500
committerRichard Eisenberg <rae@richarde.dev>2020-11-30 11:42:41 -0500
commit973fb5098dfe197456bc1670f6ce62265ab6f6aa (patch)
tree2be5f2b6f85aae5e5dd4f37a4fe5858e282d3895
parent50b22545b7ae4cbb718fdf452e9fc71dbe04cd91 (diff)
downloadhaskell-wip/cfuneqcan-refactor.tar.gz
Rename the flattener to become the rewriter.wip/cfuneqcan-refactor
Now that flattening doesn't produce flattening variables, it's not really flattening anything: it's rewriting. This change also means that the rewriter can no longer be confused the core flattener (in GHC.Core.Unify), which is sometimes used during type-checking.
Diffstat
-rw-r--r--compiler/GHC/Core/Coercion.hs86
-rw-r--r--compiler/GHC/Core/FamInstEnv.hs11
-rw-r--r--compiler/GHC/Core/Unify.hs5
-rw-r--r--compiler/GHC/Tc/Errors.hs6
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs2
-rw-r--r--compiler/GHC/Tc/Solver.hs16
-rw-r--r--compiler/GHC/Tc/Solver/Canonical.hs192
-rw-r--r--compiler/GHC/Tc/Solver/Interact.hs4
-rw-r--r--compiler/GHC/Tc/Solver/Monad.hs24
-rw-r--r--compiler/GHC/Tc/Solver/Rewrite.hs (renamed from compiler/GHC/Tc/Solver/Flatten.hs)551
-rw-r--r--compiler/GHC/Tc/Types/Constraint.hs20
-rw-r--r--compiler/GHC/Tc/Utils/TcMType.hs19
-rw-r--r--compiler/GHC/Tc/Utils/TcType.hs6
-rw-r--r--compiler/GHC/Tc/Utils/Unify.hs3
-rw-r--r--compiler/GHC/Utils/Monad.hs4
-rw-r--r--compiler/ghc.cabal.in2
16 files changed, 459 insertions, 492 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 051f415572..21e7202b96 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -1650,7 +1650,7 @@ where the two kind coercions are identical. In that case we can exploit the
situation where the main coercion is reflexive, via the special cases for Refl
and GRefl.
-This is important when flattening (ty |> co). We flatten ty, yielding
+This is important when rewriting (ty |> co). We rewrite ty, yielding
fco :: ty ~ ty'
and now we want a coercion xco between
xco :: (ty |> co) ~ (ty' |> co)
@@ -2664,19 +2664,19 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
%* *
%************************************************************************
-The function below morally belongs in GHC.Tc.Solver.Flatten, but it is used also in
+The function below morally belongs in GHC.Tc.Solver.Rewrite, but it is used also in
FamInstEnv, and so lives here.
Note [simplifyArgsWorker]
~~~~~~~~~~~~~~~~~~~~~~~~~
-Invariant (F2) of Note [Flattening] in GHC.Tc.Solver.Flatten says that
-flattening is homogeneous.
-This causes some trouble when flattening a function applied to a telescope
+Invariant (F2) of Note [Rewriting] in GHC.Tc.Solver.Rewrite says that
+rewriting is homogeneous.
+This causes some trouble when rewriting a function applied to a telescope
of arguments, perhaps with dependency. For example, suppose
type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]
-and we wish to flatten the args of (with kind applications explicit)
+and we wish to rewrite the args of (with kind applications explicit)
F a b (Just a c) (Right a b d) False
@@ -2692,7 +2692,7 @@ where all variables are skolems and
[G] cco :: c ~ fc
[G] dco :: d ~ fd
-The first step is to flatten all the arguments. This is done before calling
+The first step is to rewrite all the arguments. This is done before calling
simplifyArgsWorker. We start from
a
@@ -2713,26 +2713,26 @@ where
co6 :: Maybe fa ~ Maybe a
co7 :: Either fa fb ~ Either a b
-We now process the flattened args in left-to-right order. The first two args
-need no further processing. But now consider the third argument. Let f3 = the flattened
+We now process the rewritten args in left-to-right order. The first two args
+need no further processing. But now consider the third argument. Let f3 = the rewritten
result, Just fa (fc |> aco) |> co6.
-This f3 flattened argument has kind (Maybe a), due to
+This f3 rewritten argument has kind (Maybe a), due to
(F2). And yet, when we build the application (F fa fb ...), we need this
argument to have kind (Maybe fa), not (Maybe a). We must cast this argument.
The coercion to use is
determined by the kind of F: we see in F's kind that the third argument has
kind Maybe j. Critically, we also know that the argument corresponding to j
-(in our example, a) flattened with a coercion co1. We can thus know the
+(in our example, a) rewrote with a coercion co1. We can thus know the
coercion needed for the 3rd argument is (Maybe (sym co1)), thus building
(f3 |> Maybe (sym co1))
More generally, we must use the Lifting Lemma, as implemented in
Coercion.liftCoSubst. As we work left-to-right, any variable that is a
dependent parameter (j and k, in our example) gets mapped in a lifting context
-to the coercion that is output from flattening the corresponding argument (co1
-and co2, in our example). Then, after flattening later arguments, we lift the
+to the coercion that is output from rewriting the corresponding argument (co1
+and co2, in our example). Then, after rewriting later arguments, we lift the
kind of these arguments in the lifting context that we've be building up.
-This coercion is then used to keep the result of flattening well-kinded.
+This coercion is then used to keep the result of rewriting well-kinded.
Working through our example, this is what happens:
@@ -2748,7 +2748,7 @@ Working through our example, this is what happens:
4. Lifting the kind (Either j k) with our LC
yields co9 :: Either fa fb ~ Either a b. Use (f4 |> sym co9) as the 4th
- argument to F, where f4 is the flattened form of argument 4, written above.
+ argument to F, where f4 is the rewritten form of argument 4, written above.
5. We lift Bool with our LC, getting <Bool>;
casting has no effect.
@@ -2789,14 +2789,14 @@ Here is an example.
co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
co = forall (j :: sym axStar). (<j> -> sym axStar)
- We are flattening:
+ We are rewriting:
a (forall (j :: Star). (j |> axStar) -> Star) -- 1
(Proxy |> co) -- 2
(bo |> sym axStar) -- 3
(NoWay |> sym bc) -- 4
:: Star
-First, we flatten all the arguments (before simplifyArgsWorker), like so:
+First, we rewrite all the arguments (before simplifyArgsWorker), like so:
(forall j. j -> Type, co1 :: (forall j. j -> Type) ~
(forall (j :: Star). (j |> axStar) -> Star)) -- 1
@@ -2808,7 +2808,7 @@ Then we do the process described in Note [simplifyArgsWorker].
1. Lifting Type (the kind of the first arg) gives us a reflexive coercion, so we
don't use it. But we do build a lifting context [k -> co1] (where co1 is a
- result of flattening an argument, written above).
+ result of rewriting an argument, written above).
2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> sym co1).
This is not a dependent argument, so we don't extend the lifting context.
@@ -2827,10 +2827,10 @@ to instantiate any kind parameters. Look at the type of co1. If we just
decomposed it, we would end up with coercions whose types include j, which is
out of scope here. Accordingly, decomposePiCos takes a list of types whose
kinds are the *right-hand* types in the decomposed coercion. (See comments on
-decomposePiCos.) Because the flattened types have unflattened kinds (because
-flattening is homogeneous), passing the list of flattened types to decomposePiCos
+decomposePiCos.) Because the rewritten types have unrewritten kinds (because
+rewriting is homogeneous), passing the list of rewritten types to decomposePiCos
just won't do: later arguments' kinds won't be as expected. So we need to get
-the *unflattened* types to pass to decomposePiCos. We can do this easily enough
+the *unrewritten* types to pass to decomposePiCos. We can do this easily enough
by taking the kind of the argument coercions, passed in originally.
(Alternative 1: We could re-engineer decomposePiCos to deal with this situation.
@@ -2842,7 +2842,7 @@ behavior into simplifyArgsWorker. This would work, I think, but then all of the
complication of decomposePiCos would end up layered on top of all the complication
here. Please, no.)
-(Alternative 3: We could pass the unflattened arguments into simplifyArgsWorker
+(Alternative 3: We could pass the unrewritten arguments into simplifyArgsWorker
so that we don't have to recreate them. But that would complicate the interface
of this function to handle a very dark, dark corner case. Better to keep our
demons to ourselves here instead of exposing them to callers. This decision is
@@ -2863,7 +2863,7 @@ to get
== bo ~ bo
res_co :: Type ~ Star
-We then use these casts on (the flattened) (3) and (4) to get
+We then use these casts on (the rewritten) (3) and (4) to get
(Bool |> sym axStar |> co5 :: Type) -- (C3)
(False |> sym bc |> co6 :: bo) -- (C4)
@@ -2884,9 +2884,9 @@ it.
This recursive call returns ([Bool, False], [...], Refl). The Bool and False
are the correct arguments we wish to return. But we must be careful about the
-result coercion: our new, flattened application will have kind Type, but we
+result coercion: our new, rewritten application will have kind Type, but we
want to make sure that the result coercion casts this back to Star. (Why?
-Because we started with an application of kind Star, and flattening is homogeneous.)
+Because we started with an application of kind Star, and rewriting is homogeneous.)
So, we have to twiddle the result coercion appropriately.
@@ -2930,7 +2930,7 @@ be an application of a variable. Here is the example:
k :: Type
x :: k
- flatten (f @Type @((->) k) x)
+ rewrite (f @Type @((->) k) x)
After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)`
is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.
@@ -2938,7 +2938,7 @@ is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.
-}
--- This is shared between the flattener and the normaliser in GHC.Core.FamInstEnv.
+-- This is shared between the rewriter and the normaliser in GHC.Core.FamInstEnv.
-- See Note [simplifyArgsWorker]
{-# INLINE simplifyArgsWorker #-}
simplifyArgsWorker :: [TyCoBinder] -> Kind
@@ -2946,15 +2946,15 @@ simplifyArgsWorker :: [TyCoBinder] -> Kind
-- list of binders can be shorter or longer than the list of args
-> TyCoVarSet -- free vars of the args
-> [Role] -- list of roles, r
- -> [(Type, Coercion)] -- flattened type arguments, arg
- -- each comes with the coercion used to flatten it,
- -- with co :: flattened_type ~ original_type
+ -> [(Type, Coercion)] -- rewritten type arguments, arg
+ -- each comes with the coercion used to rewrite it,
+ -- with co :: rewritten_type ~ original_type
-> ([Type], [Coercion], MCoercionN)
-- Returns (xis, cos, res_co), where each co :: xi ~ arg,
-- and res_co :: kind (f xis) ~ kind (f tys), where f is the function applied to the args
-- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in),
--- then (f orig_tys) is well kinded. Note that (f flattened_tys) might *not* be well-kinded.
--- Massaging the flattened_tys in order to make (f flattened_tys) well-kinded is what this
+-- then (f orig_tys) is well kinded. Note that (f rewritten_tys) might *not* be well-kinded.
+-- Massaging the rewritten_tys in order to make (f rewritten_tys) well-kinded is what this
-- function is all about. That is, (f xis), where xis are the returned arguments, *is*
-- well kinded.
simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
@@ -2966,11 +2966,11 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
go :: [Type] -- Xis accumulator, in reverse order
-> [Coercion] -- Coercions accumulator, in reverse order
-- These are in 1-to-1 correspondence
- -> LiftingContext -- mapping from tyvars to flattening coercions
+ -> LiftingContext -- mapping from tyvars to rewriting coercions
-> [TyCoBinder] -- Unsubsted binders of function's kind
-> Kind -- Unsubsted result kind of function (not a Pi-type)
- -> [Role] -- Roles at which to flatten these ...
- -> [(Type, Coercion)] -- flattened arguments, with their flattening coercions
+ -> [Role] -- Roles at which to rewrite these ...
+ -> [(Type, Coercion)] -- rewritten arguments, with their rewriting coercions
-> ([Type], [Coercion], MCoercionN)
go acc_xis acc_cos !lc binders inner_ki _ []
-- The !lc makes the function strict in the lifting context
@@ -2982,10 +2982,10 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
| otherwise = MCo $ liftCoSubst Nominal lc final_kind
go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) ((xi,co):args)
- = -- By Note [Flattening] in GHC.Tc.Solver.Flatten invariant (F2),
+ = -- By Note [Rewriting] in GHC.Tc.Solver.Rewrite invariant (F2),
-- tcTypeKind(xi) = tcTypeKind(ty). But, it's possible that xi will be
-- used as an argument to a function whose kind is different, if
- -- earlier arguments have been flattened to new types. We thus
+ -- earlier arguments have been rewritten to new types. We thus
-- need a coercion (kind_co :: old_kind ~ new_kind).
--
-- The bangs here have been observed to improve performance
@@ -3014,8 +3014,8 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
go acc_xis acc_cos lc [] inner_ki roles args
= let co1 = liftCoSubst Nominal lc inner_ki
co1_kind = coercionKind co1
- unflattened_tys = map (coercionRKind . snd) args
- (arg_cos, res_co) = decomposePiCos co1 co1_kind unflattened_tys
+ unrewritten_tys = map (coercionRKind . snd) args
+ (arg_cos, res_co) = decomposePiCos co1 co1_kind unrewritten_tys
casted_args = ASSERT2( equalLength args arg_cos
, ppr args $$ ppr arg_cos )
[ (casted_xi, casted_co)
@@ -3029,8 +3029,8 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
-- ... -> k, that k will be substituted to perhaps reveal more
-- binders.
zapped_lc = zapLiftingContext lc
- Pair flattened_kind _ = co1_kind
- (bndrs, new_inner) = splitPiTys flattened_kind
+ Pair rewritten_kind _ = co1_kind
+ (bndrs, new_inner) = splitPiTys rewritten_kind
(xis_out, cos_out, res_co_out)
= go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_args
@@ -3041,8 +3041,8 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
"simplifyArgsWorker wandered into deeper water than usual"
-- This debug information is commented out because leaving it in
-- causes a ~2% increase in allocations in T9872d.
- -- That's independent of the analogous case in flatten_args_fast
- -- in GHC.Tc.Solver.Flatten:
+ -- That's independent of the analogous case in rewrite_args_fast
+ -- in GHC.Tc.Solver.Rewrite:
-- each of these causes a 2% increase on its own, so commenting them
-- both out gives a 4% decrease in T9872d.
{-
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index a6c7604008..0876cacf57 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -1198,8 +1198,7 @@ findBranch branches target_tys
apartnessCheck :: [Type]
-- ^ /flattened/ target arguments. Make sure they're flattened! See
-- Note [Flattening type-family applications when matching instances]
- -- in GHC.Core.Unify. (NB: This "flat" is a different
- -- "flat" than is used in GHC.Tc.Solver.Flatten.)
+ -- in GHC.Core.Unify.
-> CoAxBranch -- ^ the candidate equation we wish to use
-- Precondition: this matches the target
-> Bool -- ^ True <=> equation can fire
@@ -1459,14 +1458,14 @@ normalise_type ty
go_app_tys :: Type -- function
-> [Type] -- args
-> NormM (Coercion, Type)
- -- cf. GHC.Tc.Solver.Flatten.flatten_app_ty_args
+ -- cf. GHC.Tc.Solver.Rewrite.rewrite_app_ty_args
go_app_tys (AppTy ty1 ty2) tys = go_app_tys ty1 (ty2 : tys)
go_app_tys fun_ty arg_tys
= do { (fun_co, nfun) <- go fun_ty
; case tcSplitTyConApp_maybe nfun of
Just (tc, xis) ->
do { (second_co, nty) <- go (mkTyConApp tc (xis ++ arg_tys))
- -- flatten_app_ty_args avoids redundantly processing the xis,
+ -- rewrite_app_ty_args avoids redundantly processing the xis,
-- but that's a much more performance-sensitive function.
-- This type normalisation is not called in a loop.
; return (mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTransCo` second_co, nty) }
@@ -1490,7 +1489,7 @@ normalise_args :: Kind -- of the function
-- and the res_co :: kind(f orig_args) ~ kind(f xis)
-- NB: The xis might *not* have the same kinds as the input types,
-- but the resulting application *will* be well-kinded
--- cf. GHC.Tc.Solver.Flatten.flatten_args_slow
+-- cf. GHC.Tc.Solver.Rewrite.rewrite_args_slow
normalise_args fun_ki roles args
= do { normed_args <- zipWithM normalise1 roles args
; let (xis, cos, res_co) = simplifyArgsWorker ki_binders inner_ki fvs roles normed_args
@@ -1499,7 +1498,7 @@ normalise_args fun_ki roles args
(ki_binders, inner_ki) = splitPiTys fun_ki
fvs = tyCoVarsOfTypes args
- -- flattener conventions are different from ours
+ -- rewriter conventions are different from ours
impedance_match :: NormM (Coercion, Type) -> NormM (Type, Coercion)
impedance_match action = do { (co, ty) <- action
; return (ty, mkSymCo co) }
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index a8f75535ab..709ccf10b4 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -692,10 +692,7 @@ unifier It does /not/ work up to ~.
The algorithm implemented here is rather delicate, and we depend on it
to uphold certain properties. This is a summary of these required
-properties. Any reference to "flattening" refers to the flattening
-algorithm in GHC.Core.Unify (See
-Note [Flattening type-family applications when matching instances] in GHC.Core.Unify),
-not the flattening algorithm in the solver.
+properties.
Notation:
θ,φ substitutions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index c2c4c2c53b..71b919b4fd 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -2736,16 +2736,12 @@ Consider (C (Maybe (F x))), where F is a type function, and we have
instances
C (Maybe Int) and C (Maybe a)
Since (F x) might turn into Int, this is an overlap situation, and
-indeed (because of flattening) the main solver will have refrained
+indeed the main solver will have refrained
from solving. But by the time we get to error message generation, we've
un-flattened the constraint. So we must *re*-flatten it before looking
up in the instance environment, lest we only report one matching
instance when in fact there are two.
-Re-flattening is pretty easy, because we don't need to keep track of
-evidence. We don't re-use the code in GHC.Tc.Solver.Canonical because that's in
-the TcS monad, and we are in TcM here.
-
Note [Kind arguments in error messages]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It can be terribly confusing to get an error message like (#9171)
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 0246426222..bf4b1c91d1 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -3939,6 +3939,8 @@ more. So I use a HACK:
Result works fine, but it may eventually bite us.
+See also Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver for
+information about how these are printed.
************************************************************************
* *
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 8a2ff39116..8b21b72768 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -43,7 +43,7 @@ import GHC.Tc.Errors
import GHC.Tc.Types.Evidence
import GHC.Tc.Solver.Interact
import GHC.Tc.Solver.Canonical ( makeSuperClasses, solveCallStack )
-import GHC.Tc.Solver.Flatten ( flattenType )
+import GHC.Tc.Solver.Rewrite ( rewriteType )
import GHC.Tc.Utils.Unify ( buildTvImplication )
import GHC.Tc.Utils.TcMType as TcM
import GHC.Tc.Utils.Monad as TcM
@@ -802,7 +802,7 @@ tcNormalise inerts ty
= do { norm_loc <- getCtLocM PatCheckOrigin Nothing
; (res, _new_inerts) <- runTcSInerts inerts $
do { traceTcS "tcNormalise {" (ppr inerts)
- ; ty' <- flattenType norm_loc ty
+ ; ty' <- rewriteType norm_loc ty
; traceTcS "tcNormalise }" (ppr ty')
; pure ty' }
; return res }
@@ -844,7 +844,7 @@ if some local equalities are solved for. See "Wrinkle: Local equalities"
in Note [Type normalisation] in "GHC.HsToCore.Pmc".
To accomplish its stated goal, tcNormalise first initialises the solver monad
-with the given InertCans, then uses flattenType to simplify the desired type
+with the given InertCans, then uses rewriteType to simplify the desired type
with respect to the Givens in the InertCans.
***********************************************************************************
@@ -2057,7 +2057,7 @@ simplifyHoles = mapBagM simpl_hole
-- we must do so here, and not in the error-message generation
-- code, because we have all the givens already set up
simpl_hole h@(Hole { hole_ty = ty, hole_loc = loc })
- = do { ty' <- flattenType loc ty
+ = do { ty' <- rewriteType loc ty
; return (h { hole_ty = ty' }) }
{- Note [Delete dead Given evidence bindings]
@@ -2120,7 +2120,8 @@ the example for why (partial-sigs/should_compile/T12844):
GHC correctly infers that the extra-constraints wildcard on `bar`
should be (Head rngs ~ '(r, r'), Foo rngs). It then adds this constraint
-as a Given on the implication constraint for `bar`. The Hole for
+as a Given on the implication constraint for `bar`. (This implication is
+created by mkResidualConstraints in simplifyInfer.) The Hole for
the _ is stored within the implication's WantedConstraints.
When simplifyHoles is called, that constraint is already assumed as
a Given. Simplifying with respect to it turns it into
@@ -2135,6 +2136,9 @@ is simple: just don't simplify extra-constraints wildcards.
This is the only reason we need to track ConstraintHole separately
from TypeHole in HoleSort.
+See also Note [Extra-constraint holes in partial type signatures]
+in GHC.Tc.Gen.HsType.
+
Note [Tracking redundant constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With Opt_WarnRedundantConstraints, GHC can report which
@@ -2550,7 +2554,7 @@ floatEqualities skols given_ids ev_binds_var has_given_eqs
; binds <- TcS.getTcEvBindsMap ev_binds_var
-- Now we can pick the ones to float
- -- The constraints are un-flattened and de-canonicalised
+ -- The constraints are de-canonicalised
; let (candidate_eqs, no_float_cts) = partitionBag is_float_eq_candidate simples
seed_skols = mkVarSet skols `unionVarSet`
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 60300b70f4..5ba0149d09 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -20,7 +20,7 @@ import GHC.Tc.Types.Origin
import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.TcType
import GHC.Core.Type
-import GHC.Tc.Solver.Flatten
+import GHC.Tc.Solver.Rewrite
import GHC.Tc.Solver.Monad
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.EvTerm
@@ -77,7 +77,7 @@ CNonCanonicals. We know nothing about these constraints. So, first:
are equalities, class predicates, or other.
Then proceed depending on the shape of the constraint. Generally speaking,
-each constraint gets flattened and then decomposed into one of several forms
+each constraint gets rewritten and then decomposed into one of several forms
(see type Ct in GHC.Tc.Types).
When an already-canonicalized constraint gets kicked out of the inert set,
@@ -99,9 +99,9 @@ canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
canonicalize (CIrredCan { cc_ev = ev })
= canNC ev
- -- Instead of flattening the evidence before classifying, it's possible we
- -- can make progress without the flatten. Try this first.
- -- For insolubles (all of which are equalities), do /not/ flatten the arguments
+ -- 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;
@@ -202,7 +202,7 @@ canClass :: CtEvidence
canClass ev cls tys pend_sc
= -- all classes do *nominal* matching
ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
- do { (xis, cos) <- flattenArgsNom ev cls_tc tys
+ do { (xis, cos) <- rewriteArgsNom ev cls_tc tys
; let co = mkTcTyConAppCo Nominal cls_tc cos
xi = mkClassPred cls xis
mk_ct new_ev = CDictCan { cc_ev = new_ev
@@ -701,10 +701,10 @@ canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
canIrred ev
= do { let pred = ctEvPred ev
; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
- ; (xi,co) <- flatten ev pred -- co :: xi ~ pred
+ ; (xi,co) <- rewrite ev pred -- co :: xi ~ pred
; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
- do { -- Re-classify, in case flattening has improved its shape
+ do { -- Re-classify, in case rewriting has improved its shape
-- Code is like the canNC, except
-- that the IrredPred branch stops work
; case classifyPredType (ctEvPred new_ev) of
@@ -816,11 +816,11 @@ canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
canForAll ev pend_sc
= do { -- First rewrite it to apply the current substitution
let pred = ctEvPred ev
- ; (xi,co) <- flatten ev pred -- co :: xi ~ pred
+ ; (xi,co) <- rewrite ev pred -- co :: xi ~ pred
; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
do { -- Now decompose into its pieces and solve it
- -- (It takes a lot less code to flatten before decomposing.)
+ -- (It takes a lot less code to rewrite before decomposing.)
; case classifyPredType (ctEvPred new_ev) of
ForAllPred tvs theta pred
-> solveForAll new_ev tvs theta pred pend_sc
@@ -896,14 +896,14 @@ Note [Canonicalising equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In order to canonicalise an equality, we look at the structure of the
two types at hand, looking for similarities. A difficulty is that the
-types may look dissimilar before flattening but similar after flattening.
-However, we don't just want to jump in and flatten right away, because
+types may look dissimilar before rewriting but similar after rewriting.
+However, we don't just want to jump in and rewrite right away, because
this might be wasted effort. So, after looking for similarities and failing,
-we flatten and then try again. Of course, we don't want to loop, so we
-track whether or not we've already flattened.
+we rewrite and then try again. Of course, we don't want to loop, so we
+track whether or not we've already rewritten.
It is conceivable to do a better job at tracking whether or not a type
-is flattened, but this is left as future work. (Mar '15)
+is rewritten, but this is left as future work. (Mar '15)
Note [Decomposing FunTy]
@@ -933,21 +933,21 @@ canEqNC ev eq_rel ty1 ty2
Right ty -> canEqReflexive ev eq_rel ty }
can_eq_nc
- :: Bool -- True => both types are flat
+ :: Bool -- True => both types are rewritten
-> CtEvidence
-> EqRel
-> Type -> Type -- LHS, after and before type-synonym expansion, resp
-> Type -> Type -- RHS, after and before type-synonym expansion, resp
-> TcS (StopOrContinue Ct)
-can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+can_eq_nc rewritten ev eq_rel ty1 ps_ty1 ty2 ps_ty2
= do { traceTcS "can_eq_nc" $
- vcat [ ppr flat, ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
+ vcat [ ppr rewritten, ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
; rdr_env <- getGlobalRdrEnvTcS
; fam_insts <- getFamInstEnvs
- ; can_eq_nc' flat rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
+ ; can_eq_nc' rewritten rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
can_eq_nc'
- :: Bool -- True => both input types are flattened
+ :: Bool -- True => both input types are rewritten
-> GlobalRdrEnv -- needed to see which newtypes are in scope
-> FamInstEnvs -- needed to unwrap data instances
-> CtEvidence
@@ -957,14 +957,14 @@ can_eq_nc'
-> TcS (StopOrContinue Ct)
-- Expand synonyms first; see Note [Type synonyms and canonicalization]
-can_eq_nc' flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
- | Just ty1' <- tcView ty1 = can_eq_nc' flat rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2
- | Just ty2' <- tcView ty2 = can_eq_nc' flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2
+can_eq_nc' rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+ | Just ty1' <- tcView ty1 = can_eq_nc' rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2
+ | Just ty2' <- tcView ty2 = can_eq_nc' rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2
-- need to check for reflexivity in the ReprEq case.
-- See Note [Eager reflexivity check]
--- Check only when flat because the zonk_eq_types check in canEqNC takes
--- care of the non-flat case.
+-- Check only when rewritten because the zonk_eq_types check in canEqNC takes
+-- care of the non-rewritten case.
can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
| ty1 `tcEqType` ty2
= canEqReflexive ev ReprEq ty1
@@ -972,7 +972,7 @@ can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
-- 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' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+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
@@ -982,26 +982,26 @@ can_eq_nc' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
= can_eq_newtype_nc ev IsSwapped ty2 stuff2 ty1 ps_ty1
-- Then, get rid of casts
-can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
+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]
- = canEqCast flat ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
-can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
+ = canEqCast rewritten ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
+can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
| isNothing (canEqLHS_maybe ty1) -- See (3) in Note [Equalities with incompatible kinds]
- = canEqCast flat ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
+ = canEqCast rewritten ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
----------------------
-- Otherwise try to decompose
----------------------
-- Literals
-can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
+can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
| l1 == l2
= do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
; stopWith ev "Equal LitTy" }
-- Decompose FunTy: (s -> t) and (c => t)
-- NB: don't decompose (Int -> blah) ~ (Show a => blah)
-can_eq_nc' _flat _rdr_env _envs ev eq_rel
+can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
(FunTy { ft_mult = am1, ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ps_ty1
(FunTy { ft_mult = am2, ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ps_ty2
| af1 == af2 -- Don't decompose (Int -> blah) ~ (Show a => blah)
@@ -1015,7 +1015,7 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel
-- Decompose type constructor applications
-- NB: we have expanded type synonyms already
-can_eq_nc' _flat _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
@@ -1025,13 +1025,13 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
, not (isTypeFamilyTyCon tc2)
= canTyConApp ev eq_rel tc1 tys1 tc2 tys2
-can_eq_nc' _flat _rdr_env _envs ev eq_rel
+can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
s1@(ForAllTy (Bndr _ vis1) _) _
s2@(ForAllTy (Bndr _ vis2) _) _
| vis1 `sameVis` vis2 -- Note [ForAllTy and typechecker equality]
= can_eq_nc_forall ev eq_rel s1 s2
--- See Note [Canonicalising type applications] about why we require flat types
+-- See Note [Canonicalising type applications] about why we require rewritten types
-- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families
-- NB: Only decompose AppTy for nominal equality. See Note [Decomposing equality]
can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
@@ -1043,19 +1043,19 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
-- Can't decompose.
-------------------
--- No similarity in type structure detected. Flatten and try again.
+-- 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 { (xi1, co1) <- flatten ev ps_ty1
- ; (xi2, co2) <- flatten ev ps_ty2
+ = do { (xi1, co1) <- rewrite ev ps_ty1
+ ; (xi2, co2) <- rewrite ev ps_ty2
; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
----------------------------
-- Look for a canonical LHS. See Note [Canonical LHS].
--- Only flat types end up below here.
+-- Only rewritten types end up below here.
----------------------------
--- NB: pattern match on True: we want only flat types sent to canEqLHS
+-- NB: pattern match on True: we want only rewritten types sent to canEqLHS
-- This means we've rewritten any variables and reduced any type family redexes
-- See also Note [No top-level newtypes on RHS of representational equalities]
can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
@@ -1077,14 +1077,14 @@ can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
-- Fall-through. Give up.
----------------------------
--- We've flattened and the types don't match. Give up.
+-- We've rewritten and the types don't match. Give up.
can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
= do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
; case eq_rel of -- See Note [Unsolved equalities]
ReprEq -> continueWith (mkIrredCt OtherCIS ev)
NomEq -> continueWith (mkIrredCt InsolubleCIS ev) }
-- No need to call canEqFailure/canEqHardFailure because they
- -- flatten, and the types involved here are already flat
+ -- rewrite, and the types involved here are already rewritten
{- Note [Unsolved equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1236,7 +1236,7 @@ can_eq_nc_forall ev eq_rel s1 s2
-- as soon as it finds that two types are not equal.
-- This is quite handy when some unification has made two
-- types in an inert Wanted to be equal. We can discover the equality without
--- flattening, which is sometimes very expensive (in the case of type functions).
+-- rewriting, which is sometimes very expensive (in the case of type functions).
-- In particular, this function makes a ~20% improvement in test case
-- perf/compiler/T5030.
--
@@ -1308,7 +1308,7 @@ zonk_eq_types = go
tyvar :: SwapFlag -> TcTyVar -> TcType
-> TcS (Either (Pair TcType) TcType)
-- Try to do as little as possible, as anything we do here is redundant
- -- with flattening. In particular, no need to zonk kinds. That's why
+ -- with rewriting. In particular, no need to zonk kinds. That's why
-- we don't use the already-defined zonking functions
tyvar swapped tv ty
= case tcTyVarDetails tv of
@@ -1419,7 +1419,7 @@ and
Naively, we would start unwrapping X and end up in a loop. Instead,
we do this eager reflexivity check. This is necessary only for representational
-equality because the flattener technology deals with the similar case
+equality because the rewriter technology deals with the similar case
(recursive type families) for nominal equality.
Note that this check does not catch all cases, but it will catch the cases
@@ -1472,7 +1472,7 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
---------
-- ^ Decompose a type application.
--- All input types must be flat. See Note [Canonicalising type applications]
+-- All input types must be rewritten. See Note [Canonicalising type applications]
-- Nominal equality only!
can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
-> Xi -> Xi -- s1 t1
@@ -1529,21 +1529,21 @@ can_eq_app ev s1 t1 s2 t2
-----------------------
-- | Break apart an equality over a casted type
-- looking like (ty1 |> co1) ~ ty2 (modulo a swap-flag)
-canEqCast :: Bool -- are both types flat?
+canEqCast :: Bool -- are both types rewritten?
-> CtEvidence
-> EqRel
-> SwapFlag
-> TcType -> Coercion -- LHS (res. RHS), ty1 |> co1
-> TcType -> TcType -- RHS (res. LHS), ty2 both normal and pretty
-> TcS (StopOrContinue Ct)
-canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
+canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
= do { traceTcS "Decomposing cast" (vcat [ ppr ev
, ppr ty1 <+> text "|>" <+> ppr co1
, ppr ps_ty2 ])
; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2
(mkTcGReflRightCo role ty1 co1)
(mkTcReflCo role ps_ty2)
- ; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
+ ; can_eq_nc rewritten new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
where
role = eqRelRole eq_rel
@@ -1899,9 +1899,9 @@ canEqFailure :: CtEvidence -> EqRel
canEqFailure ev NomEq ty1 ty2
= canEqHardFailure ev ty1 ty2
canEqFailure ev ReprEq ty1 ty2
- = do { (xi1, co1) <- flatten ev ty1
- ; (xi2, co2) <- flatten ev ty2
- -- We must flatten the types before putting them in the
+ = do { (xi1, co1) <- rewrite ev ty1
+ ; (xi2, co2) <- rewrite ev ty2
+ -- We must rewrite the types before putting them in the
-- inert set, so that we are sure to kick them out when
-- new equalities become available
; traceTcS "canEqFailure with ReprEq" $
@@ -1915,8 +1915,8 @@ canEqHardFailure :: CtEvidence
-- See Note [Make sure that insolubles are fully rewritten]
canEqHardFailure ev ty1 ty2
= do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2)
- ; (s1, co1) <- flatten ev ty1
- ; (s2, co2) <- flatten ev ty2
+ ; (s1, co1) <- rewrite ev ty1
+ ; (s2, co2) <- rewrite ev ty2
; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
; continueWith (mkIrredCt InsolubleCIS new_ev) }
@@ -1951,7 +1951,7 @@ decompose the application eagerly, yielding
we get an error "Can't match Array ~ Maybe",
but we'd prefer to get "Can't match Array b ~ Maybe c".
-So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
+So instead can_eq_wanted_app rewrites the LHS and RHS, in the hope of
replacing (a b) by (Array b), before using try_decompose_app to
decompose it.
@@ -1997,8 +1997,8 @@ Suppose we're in this situation:
where
newtype Id a = Id a
-We want to make sure canEqCanLHS sees [W] a ~R a, after b is flattened
-and the Id newtype is unwrapped. This is assured by requiring only flat
+We want to make sure canEqCanLHS sees [W] a ~R a, after b is rewritten
+and the Id newtype is unwrapped. This is assured by requiring only rewritten
types in canEqCanLHS *and* having the newtype-unwrapping check above
the tyvar check in can_eq_nc.
@@ -2057,7 +2057,7 @@ and then, using g1, to
[D] w5 : a ~ beta
at which point we can unify and go on to glory. (This rewriting actually
-happens all at once, in the call to flatten during canonicalisation.)
+happens all at once, in the call to rewrite during canonicalisation.)
But what about the new LHS makes it better? It mentions a variable (beta)
that can appear in a Wanted -- a touchable metavariable never appears
@@ -2073,8 +2073,8 @@ Ticket #12526 is another good example of this in action.
canEqCanLHS :: CtEvidence -- ev :: lhs ~ rhs
-> EqRel -> SwapFlag
-> CanEqLHS -- lhs (or, if swapped, rhs)
- -> TcType -- lhs: pretty lhs, already flat
- -> TcType -> TcType -- rhs: already flat
+ -> TcType -- lhs: pretty lhs, already rewritten
+ -> TcType -> TcType -- rhs: already rewritten
-> TcS (StopOrContinue Ct)
canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
| k1 `tcEqType` k2
@@ -2332,7 +2332,7 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
; continueWith (CEqCan { cc_ev = new_ev, cc_lhs = lhs
, cc_rhs = rhs, cc_eq_rel = eq_rel }) }
-- it is possible that cc_rhs mentions the LHS if the LHS is a type
- -- family. This will cause later flattening to potentially loop, but
+ -- family. This will cause later rewriting to potentially loop, but
-- that will be caught by the depth counter. The other option is an
-- occurs-check for a function application, which seems awkward.
@@ -2441,8 +2441,8 @@ canEqOK dflags eq_rel lhs rhs
-- we don't want to rewrite existing inerts with it, otherwise
-- we'd risk divergence in the constraint solver
- -- NB: no occCheckExpand here; see Note [Flattening synonyms]
- -- in GHC.Tc.Solver.Flatten
+ -- NB: no occCheckExpand here; see Note [Rewriting synonyms]
+ -- in GHC.Tc.Solver.Rewrite
| otherwise -> CanEqNotOK OtherCIS
-- A representational equality with an occurs-check problem isn't
@@ -2524,38 +2524,39 @@ Wrinkles:
must be sure to kick out any such CIrredCan constraints that mention coercion holes
when those holes get filled in, so that the unification step can now proceed.
- (2a) We must now kick out any constraints that mention a newly-filled-in
- coercion hole, but only if there are no more remaining coercion
- holes. This is done in kickOutAfterFillingCoercionHole. The extra
- check that there are no more remaining holes avoids needless work
- when rewriting evidence (which fills coercion holes) and aids
- efficiency.
-
- Moreover, kicking out when there are remaining unfilled holes can
- cause a loop in the solver in this case:
- [W] w1 :: (ty1 :: F a) ~ (ty2 :: s)
- After canonicalisation, we discover that this equality is heterogeneous.
- So we emit
- [W] co_abc :: F a ~ s
- and preserve the original as
- [W] w2 :: (ty1 |> co_abc) ~ ty2 (blocked on co_abc)
- Then, co_abc comes becomes the work item. It gets swapped in
- canEqCanLHS2 and then back again in canEqTyVarFunEq. We thus get
- co_abc := sym co_abd, and then co_abd := sym co_abe, with
- [W] co_abe :: F a ~ s
- This process has filled in co_abc. Suppose w2 were kicked out.
- When it gets processed,
- would get this whole chain going again. The solution is to
- kick out a blocked constraint only when the result of filling
- in the blocking coercion involves no further blocking coercions.
- Alternatively, we could be careful not to do unnecessary swaps during
- canonicalisation, but that seems hard to do, in general.
+ The kicking out is done in kickOutAfterFillingCoercionHole.
+
+ However, we must be careful: we kick out only when no coercion holes are
+ left. The holes in the type are stored in the BlockedCIS CtIrredStatus.
+ The extra check that there are no more remaining holes avoids
+ needless work when rewriting evidence (which fills coercion holes) and
+ aids efficiency.
+
+ Moreover, kicking out when there are remaining unfilled holes can
+ cause a loop in the solver in this case:
+ [W] w1 :: (ty1 :: F a) ~ (ty2 :: s)
+ After canonicalisation, we discover that this equality is heterogeneous.
+ So we emit
+ [W] co_abc :: F a ~ s
+ and preserve the original as
+ [W] w2 :: (ty1 |> co_abc) ~ ty2 (blocked on co_abc)
+ Then, co_abc comes becomes the work item. It gets swapped in
+ canEqCanLHS2 and then back again in canEqTyVarFunEq. We thus get
+ co_abc := sym co_abd, and then co_abd := sym co_abe, with
+ [W] co_abe :: F a ~ s
+ This process has filled in co_abc. Suppose w2 were kicked out.
+ When it gets processed,
+ would get this whole chain going again. The solution is to
+ kick out a blocked constraint only when the result of filling
+ in the blocking coercion involves no further blocking coercions.
+ Alternatively, we could be careful not to do unnecessary swaps during
+ canonicalisation, but that seems hard to do, in general.
(3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the
algorithm detailed here, producing [W] co :: k2 ~ k1, and adding
[W] (a :: k1) ~ ((rhs |> co) :: k1) to the irreducibles. Some time
later, we solve co, and fill in co's coercion hole. This kicks out
- the irreducible as described in (2a).
+ the irreducible as described in (2).
But now, during canonicalization, we see the cast
and remove it, in canEqCast. By the time we get into canEqCanLHS, the equality
is heterogeneous again, and the process repeats.
@@ -2832,9 +2833,10 @@ Details:
they originally stood for (e.g. cbv1 := TF a, cbv2 := TF Int),
not what may be in a rewritten constraint.
- Not breaking cycles fursther makes sense, because
- we only want to break cycles for user-written loopy Givens, and
- a CycleBreakerTv certainly isn't user-written.
+ Not breaking cycles further (which would mean changing TF cbv1 to cbv3
+ and TF cbv2 to cbv4) makes sense, because we only want to break cycles
+ for user-written loopy Givens, and a CycleBreakerTv certainly isn't
+ user-written.
NB: This same situation (an equality like b ~ Maybe (F b)) can arise with
Wanteds, but we have no concrete case incentivising special treatment. It
@@ -2912,7 +2914,7 @@ may reflect the result of unification alpha := ty, so new_pred might
not _look_ the same as old_pred, and it's vital to proceed from now on
using new_pred.
-qThe flattener preserves type synonyms, so they should appear in new_pred
+The rewriter preserves type synonyms, so they should appear in new_pred
as well as in old_pred; that is important for good error messages.
-}
@@ -2922,7 +2924,7 @@ rewriteEvidence old_ev@(CtDerived {}) new_pred _co
-- This is very important, DO NOT re-order the equations for
-- rewriteEvidence to put the isTcReflCo test first!
-- Why? Because for *Derived* constraints, c, the coercion, which
- -- was produced by flattening, may contain suspended calls to
+ -- was produced by rewriting, may contain suspended calls to
-- (ctEvExpr c), which fails for Derived constraints.
-- (Getting this wrong caused #7384.)
continueWith (old_ev { ctev_pred = new_pred })
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 49d4ad20ab..dc20b90260 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -201,7 +201,7 @@ runTcPluginsGiven
; updInertIrreds (\irreds -> extendCtsList irreds insols)
; return (pluginNewCts p) } } }
--- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
+-- | Given a bag of (rewritten, zonked) wanteds, invoke the plugins on
-- them and produce an updated bag of wanteds (possibly with some new
-- work) and a bag of insolubles. The boolean indicates whether
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
@@ -862,7 +862,7 @@ Suppose we have (#13943)
instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where ..
And we have [W] Take 3. That only matches one instance so we get
-[W] Take (3-1). Really we should now flatten to reduce the (3-1) to 2, and
+[W] Take (3-1). Really we should now rewrite to reduce the (3-1) to 2, and
so on -- but that is reproducing yet more of the solver. Sigh. For now,
we just give up (remember all this is just an optimisation).
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 80f6e7f3a8..76d9316bf6 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -90,7 +90,7 @@ module GHC.Tc.Solver.Monad (
-- Irreds
foldIrreds,
- -- The flattening cache
+ -- The family application cache
lookupFamAppInert, lookupFamAppCache, extendFamAppCache,
pprKicked,
@@ -124,7 +124,7 @@ module GHC.Tc.Solver.Monad (
-- if the whole instance matcher simply belongs
-- here
- breakTyVarCycle, flattenView
+ breakTyVarCycle, rewriterView
) where
#include "HsVersions.h"
@@ -1193,7 +1193,7 @@ old inert, because a [D] can rewrite a [WD].
inert: [D] F v ~ alpha (CEqCan)
Can't make progress on this work item either (although GHC tries by
-decomposing the cast and reflattening... but that doesn't make a difference),
+decomposing the cast and rewriting... but that doesn't make a difference),
which is still hetero. Emit a new kind equality and add to inert set. But,
critically, we split the Irred.
@@ -1215,7 +1215,7 @@ We decompose the cast, yielding
[D] a ~ beta
-We then flatten the kinds. The lhs kind is F v, which flattens to alpha.
+We then rewrite the kinds. The lhs kind is F v, which flattens to alpha.
co' :: F v ~ alpha
[D] (a |> co') ~ beta
@@ -1782,7 +1782,7 @@ kickOutAfterUnification new_tv
; setInertCans ics2
; return n_kicked }
--- See Wrinkle (2a) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
+-- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS ()
kickOutAfterFillingCoercionHole hole filled_co
= do { ics <- getInertCans
@@ -2230,7 +2230,6 @@ type family applications? (Examples are below the explanation.)
To allow flexibility in how type family applications unify we use
the Core flattener. See
Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.
-This is *distinct* from the flattener in GHC.Tc.Solver.Flatten.
The Core flattener replaces all type family applications with
fresh variables. The next question: should we allow these fresh
variables in the domain of a unifying substitution?
@@ -2445,7 +2444,7 @@ lookupFamAppCache fam_tc tys
Nothing -> return Nothing }
extendFamAppCache :: TyCon -> [Type] -> (TcCoercion, TcType) -> TcS ()
--- NB: co :: rhs ~ F tys, to match expectations of flattener
+-- NB: co :: rhs ~ F tys, to match expectations of rewriter
extendFamAppCache tc xi_args stuff@(_, ty)
= do { dflags <- getDynFlags
; when (gopt Opt_FamAppCache dflags) $
@@ -2728,7 +2727,6 @@ data TcSEnv
tcs_inerts :: IORef InertSet, -- Current inert set
- -- The main work-list and the flattening worklist
-- See Note [WorkList priorities] and
tcs_worklist :: IORef WorkList -- Current worklist
}
@@ -3577,7 +3575,7 @@ breakTyVarCycle :: CtLoc
-- This could be considerably more efficient. See Detail (5) of Note.
breakTyVarCycle loc = go
where
- go ty | Just ty' <- flattenView ty = go ty'
+ go ty | Just ty' <- rewriterView ty = go ty'
go (Rep.TyConApp tc tys)
| isTypeFamilyTyCon tc
= do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys
@@ -3621,9 +3619,9 @@ restoreTyVarCycles is
-- Unwrap a type synonym only when either:
-- The type synonym is forgetful, or
-- the type synonym mentions a type family in its expansion
--- See Note [Flattening synonyms] in GHC.Tc.Solver.Flatten.
-flattenView :: TcType -> Maybe TcType
-flattenView ty@(Rep.TyConApp tc _)
+-- See Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite.
+rewriterView :: TcType -> Maybe TcType
+rewriterView ty@(Rep.TyConApp tc _)
| isForgetfulSynTyCon tc || (isTypeSynonymTyCon tc && not (isFamFreeTyCon tc))
= tcView ty
-flattenView _other = Nothing
+rewriterView _other = Nothing
diff --git a/compiler/GHC/Tc/Solver/Flatten.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index c94dc21f2a..7e4993ad8d 100644
--- a/compiler/GHC/Tc/Solver/Flatten.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -4,9 +4,9 @@
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
-module GHC.Tc.Solver.Flatten(
- flatten, flattenKind, flattenArgsNom,
- flattenType
+module GHC.Tc.Solver.Rewrite(
+ rewrite, rewriteKind, rewriteArgsNom,
+ rewriteType
) where
#include "HsVersions.h"
@@ -41,127 +41,127 @@ import Control.Arrow ( first )
{-
************************************************************************
* *
-* FlattenEnv & FlatM
-* The flattening environment & monad
+* RewriteEnv & RewriteM
+* The rewriting environment & monad
* *
************************************************************************
-}
-data FlattenEnv
- = FE { fe_loc :: !CtLoc -- See Note [Flattener CtLoc]
+data RewriteEnv
+ = FE { fe_loc :: !CtLoc -- See Note [Rewriter CtLoc]
, fe_flavour :: !CtFlavour
- , fe_eq_rel :: !EqRel -- See Note [Flattener EqRels]
+ , fe_eq_rel :: !EqRel -- See Note [Rewriter EqRels]
}
--- | The 'FlatM' monad is a wrapper around 'TcS' with a 'FlattenEnv'
-newtype FlatM a
- = FlatM { runFlatM :: FlattenEnv -> TcS a }
+-- | The 'RewriteM' monad is a wrapper around 'TcS' with a 'RewriteEnv'
+newtype RewriteM a
+ = RewriteM { runRewriteM :: RewriteEnv -> TcS a }
deriving (Functor)
-instance Monad FlatM where
- m >>= k = FlatM $ \env ->
- do { a <- runFlatM m env
- ; runFlatM (k a) env }
+instance Monad RewriteM where
+ m >>= k = RewriteM $ \env ->
+ do { a <- runRewriteM m env
+ ; runRewriteM (k a) env }
-instance Applicative FlatM where
- pure x = FlatM $ const (pure x)
+instance Applicative RewriteM where
+ pure x = RewriteM $ const (pure x)
(<*>) = ap
-instance HasDynFlags FlatM where
+instance HasDynFlags RewriteM where
getDynFlags = liftTcS getDynFlags
-liftTcS :: TcS a -> FlatM a
+liftTcS :: TcS a -> RewriteM a
liftTcS thing_inside
- = FlatM $ const thing_inside
+ = RewriteM $ const thing_inside
-- convenient wrapper when you have a CtEvidence describing
--- the flattening operation
-runFlattenCtEv :: CtEvidence -> FlatM a -> TcS a
-runFlattenCtEv ev
- = runFlatten (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
-
--- Run thing_inside (which does the flattening)
-runFlatten :: CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a
-runFlatten loc flav eq_rel thing_inside
- = runFlatM thing_inside fmode
+-- the rewriting operation
+runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS a
+runRewriteCtEv ev
+ = runRewrite (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
+
+-- Run thing_inside (which does the rewriting)
+runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
+runRewrite loc flav eq_rel thing_inside
+ = runRewriteM thing_inside fmode
where
fmode = FE { fe_loc = loc
, fe_flavour = flav
, fe_eq_rel = eq_rel }
-traceFlat :: String -> SDoc -> FlatM ()
-traceFlat herald doc = liftTcS $ traceTcS herald doc
-{-# INLINE traceFlat #-} -- see Note [INLINE conditional tracing utilities]
+traceRewriteM :: String -> SDoc -> RewriteM ()
+traceRewriteM herald doc = liftTcS $ traceTcS herald doc
+{-# INLINE traceRewriteM #-} -- see Note [INLINE conditional tracing utilities]
-getFlatEnvField :: (FlattenEnv -> a) -> FlatM a
-getFlatEnvField accessor
- = FlatM $ \env -> return (accessor env)
+getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
+getRewriteEnvField accessor
+ = RewriteM $ \env -> return (accessor env)
-getEqRel :: FlatM EqRel
-getEqRel = getFlatEnvField fe_eq_rel
+getEqRel :: RewriteM EqRel
+getEqRel = getRewriteEnvField fe_eq_rel
-getRole :: FlatM Role
+getRole :: RewriteM Role
getRole = eqRelRole <$> getEqRel
-getFlavour :: FlatM CtFlavour
-getFlavour = getFlatEnvField fe_flavour
+getFlavour :: RewriteM CtFlavour
+getFlavour = getRewriteEnvField fe_flavour
-getFlavourRole :: FlatM CtFlavourRole
+getFlavourRole :: RewriteM CtFlavourRole
getFlavourRole
= do { flavour <- getFlavour
; eq_rel <- getEqRel
; return (flavour, eq_rel) }
-getLoc :: FlatM CtLoc
-getLoc = getFlatEnvField fe_loc
+getLoc :: RewriteM CtLoc
+getLoc = getRewriteEnvField fe_loc
-checkStackDepth :: Type -> FlatM ()
+checkStackDepth :: Type -> RewriteM ()
checkStackDepth ty
= do { loc <- getLoc
; liftTcS $ checkReductionDepth loc ty }
--- | Change the 'EqRel' in a 'FlatM'.
-setEqRel :: EqRel -> FlatM a -> FlatM a
+-- | Change the 'EqRel' in a 'RewriteM'.
+setEqRel :: EqRel -> RewriteM a -> RewriteM a
setEqRel new_eq_rel thing_inside
- = FlatM $ \env ->
+ = RewriteM $ \env ->
if new_eq_rel == fe_eq_rel env
- then runFlatM thing_inside env
- else runFlatM thing_inside (env { fe_eq_rel = new_eq_rel })
+ then runRewriteM thing_inside env
+ else runRewriteM thing_inside (env { fe_eq_rel = new_eq_rel })
{-# INLINE setEqRel #-}
--- | Make sure that flattening actually produces a coercion (in other
+-- | Make sure that rewriting actually produces a coercion (in other
-- words, make sure our flavour is not Derived)
-- Note [No derived kind equalities]
-noBogusCoercions :: FlatM a -> FlatM a
+noBogusCoercions :: RewriteM a -> RewriteM a
noBogusCoercions thing_inside
- = FlatM $ \env ->
+ = RewriteM $ \env ->
-- No new thunk is made if the flavour hasn't changed (note the bang).
let !env' = case fe_flavour env of
Derived -> env { fe_flavour = Wanted WDeriv }
_ -> env
in
- runFlatM thing_inside env'
+ runRewriteM thing_inside env'
-bumpDepth :: FlatM a -> FlatM a
-bumpDepth (FlatM thing_inside)
- = FlatM $ \env -> do
- -- bumpDepth can be called a lot during flattening so we force the
+bumpDepth :: RewriteM a -> RewriteM a
+bumpDepth (RewriteM thing_inside)
+ = RewriteM $ \env -> do
+ -- bumpDepth can be called a lot during rewriting so we force the
-- new env to avoid accumulating thunks.
{ let !env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
; thing_inside env' }
{-
-Note [Flattener EqRels]
+Note [Rewriter EqRels]
~~~~~~~~~~~~~~~~~~~~~~~
-When flattening, we need to know which equality relation -- nominal
+When rewriting, we need to know which equality relation -- nominal
or representation -- we should be respecting. The only difference is
that we rewrite variables by representational equalities when fe_eq_rel
-is ReprEq, and that we unwrap newtypes when flattening w.r.t.
+is ReprEq, and that we unwrap newtypes when rewriting w.r.t.
representational equality.
-Note [Flattener CtLoc]
+Note [Rewriter CtLoc]
~~~~~~~~~~~~~~~~~~~~~~
-The flattener does eager type-family reduction.
+The rewriter does eager type-family reduction.
Type families might loop, and we
don't want GHC to do so. A natural solution is to have a bounded depth
to these processes. A central difficulty is that such a solution isn't
@@ -169,8 +169,8 @@ quite compositional. For example, say it takes F Int 10 steps to get to Bool.
How many steps does it take to get from F Int -> F Int to Bool -> Bool?
10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to
know and hard to track. So, we punt, essentially. We store a CtLoc in
-the FlattenEnv and just update the environment when recurring. In the
-TyConApp case, where there may be multiple type families to flatten,
+the RewriteEnv and just update the environment when recurring. In the
+TyConApp case, where there may be multiple type families to rewrite,
we just copy the current CtLoc into each branch. If any branch hits the
stack limit, then the whole thing fails.
@@ -179,15 +179,15 @@ will be essentially impossible. So, the official recommendation if a
stack limit is hit is to disable the check entirely. Otherwise, there
will be baffling, unpredictable errors.
-Note [Phantoms in the flattener]
+Note [Phantoms in the rewriter]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
data Proxy p = Proxy
-and we're flattening (Proxy ty) w.r.t. ReprEq. Then, we know that `ty`
+and we're rewriting (Proxy ty) w.r.t. ReprEq. Then, we know that `ty`
is really irrelevant -- it will be ignored when solving for representational
-equality later on. So, we omit flattening `ty` entirely. This may
+equality later on. So, we omit rewriting `ty` entirely. This may
violate the expectation of "xi"s for a bit, but the canonicaliser will
soon throw out the phantoms when decomposing a TyConApp. (Or, the
canonicaliser will emit an insoluble, in which case we get
@@ -205,66 +205,63 @@ changes the flavour from Derived just for this purpose.
{- *********************************************************************
* *
-* Externally callable flattening functions *
+* Externally callable rewriting functions *
* *
-* They are all wrapped in runFlatten, so their *
-* flattening work gets put into the work list *
-* *
-*********************************************************************
+************************************************************************
-}
--- | See Note [Flattening].
--- If (xi, co) <- flatten mode ev ty, then co :: xi ~r ty
+-- | See Note [Rewriting].
+-- If (xi, co) <- rewrite mode ev ty, then co :: xi ~r ty
-- where r is the role in @ev@.
-flatten :: CtEvidence -> TcType
+rewrite :: CtEvidence -> TcType
-> TcS (Xi, TcCoercion)
-flatten ev ty
- = do { traceTcS "flatten {" (ppr ty)
- ; (ty', co) <- runFlattenCtEv ev (flatten_one ty)
- ; traceTcS "flatten }" (ppr ty')
+rewrite ev ty
+ = do { traceTcS "rewrite {" (ppr ty)
+ ; (ty', co) <- runRewriteCtEv ev (rewrite_one ty)
+ ; traceTcS "rewrite }" (ppr ty')
; return (ty', co) }
--- specialized to flattening kinds: never Derived, always Nominal
+-- specialized to rewriting kinds: never Derived, always Nominal
-- See Note [No derived kind equalities]
--- See Note [Flattening]
-flattenKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
-flattenKind loc flav ty
- = do { traceTcS "flattenKind {" (ppr flav <+> ppr ty)
+-- See Note [Rewriting]
+rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
+rewriteKind loc flav ty
+ = do { traceTcS "rewriteKind {" (ppr flav <+> ppr ty)
; let flav' = case flav of
Derived -> Wanted WDeriv -- the WDeriv/WOnly choice matters not
_ -> flav
- ; (ty', co) <- runFlatten loc flav' NomEq (flatten_one ty)
- ; traceTcS "flattenKind }" (ppr ty' $$ ppr co) -- co is never a panic
+ ; (ty', co) <- runRewrite loc flav' NomEq (rewrite_one ty)
+ ; traceTcS "rewriteKind }" (ppr ty' $$ ppr co) -- co is never a panic
; return (ty', co) }
--- See Note [Flattening]
-flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion])
--- Externally-callable, hence runFlatten
--- Flatten a vector of types all at once; in fact they are
+-- See Note [Rewriting]
+rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion])
+-- Externally-callable, hence runRewrite
+-- Rewrite a vector of types all at once; in fact they are
-- always the arguments of type family or class, so
-- ctEvFlavour ev = Nominal
--- and we want to flatten all at nominal role
+-- and we want to rewrite all at nominal role
-- The kind passed in is the kind of the type family or class, call it T
-- The kind of T args must be constant (i.e. not depend on the args)
--
-- For Derived constraints the returned coercion may be undefined
--- because flattening may use a Derived equality ([D] a ~ ty)
-flattenArgsNom ev tc tys
- = do { traceTcS "flatten_args {" (vcat (map ppr tys))
+-- because rewriting may use a Derived equality ([D] a ~ ty)
+rewriteArgsNom ev tc tys
+ = do { traceTcS "rewrite_args {" (vcat (map ppr tys))
; (tys', cos, kind_co)
- <- runFlattenCtEv ev (flatten_args_tc tc Nothing tys)
+ <- runRewriteCtEv ev (rewrite_args_tc tc Nothing tys)
; MASSERT( isReflMCo kind_co )
- ; traceTcS "flatten }" (vcat (map ppr tys'))
+ ; traceTcS "rewrite }" (vcat (map ppr tys'))
; return (tys', cos) }
--- | Flatten a type w.r.t. nominal equality. This is useful to rewrite
+-- | Rewrite a type w.r.t. nominal equality. This is useful to rewrite
-- a type w.r.t. any givens. It does not do type-family reduction. This
-- will never emit new constraints. Call this when the inert set contains
-- only givens.
-flattenType :: CtLoc -> TcType -> TcS TcType
-flattenType loc ty
- = do { (xi, _) <- runFlatten loc Given NomEq $
- flatten_one ty
+rewriteType :: CtLoc -> TcType -> TcS TcType
+rewriteType loc ty
+ = do { (xi, _) <- runRewrite loc Given NomEq $
+ rewrite_one ty
-- use Given flavor so that it is rewritten
-- only w.r.t. Givens, never Wanteds/Deriveds
-- (Shouldn't matter, if only Givens are present
@@ -273,13 +270,13 @@ flattenType loc ty
{- *********************************************************************
* *
-* The main flattening functions
+* The main rewriting functions
* *
********************************************************************* -}
-{- Note [Flattening]
+{- Note [Rewriting]
~~~~~~~~~~~~~~~~~~~~
- flatten ty ==> (xi, co)
+ rewrite ty ==> (xi, co)
where
xi has no reducible type functions
has no skolems that are mapped in the inert set
@@ -291,13 +288,13 @@ Key invariants:
(F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
(F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
-Note that it is flatten's job to try to reduce *every type function it sees*.
+Note that it is rewrite's job to try to reduce *every type function it sees*.
-Flattening also:
+Rewriting also:
* zonks, removing any metavariables, and
* applies the substitution embodied in the inert set
-Because flattening zonks and the returned coercion ("co" above) is also
+Because rewriting zonks and the returned coercion ("co" above) is also
zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
we can rely on this fact:
@@ -308,37 +305,33 @@ type may or may not be ty, however: if ty has unzonked filled-in metavariables,
then the right-hand type of co will be the zonk-equal to ty.
It is for this reason that we
occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
-even before we zonk the whole program. For example, see the FTRNotFollowed
-case in flattenTyVar.
+even before we zonk the whole program. For example, see the RTRNotFollowed
+case in rewriteTyVar.
-Why have these invariants on flattening? Because we sometimes use tcTypeKind
+Why have these invariants on rewriting? Because we sometimes use tcTypeKind
during canonicalisation, and we want this kind to be zonked (e.g., see
GHC.Tc.Solver.Canonical.canEqCanLHS).
-Flattening is always homogeneous. That is, the kind of the result of flattening is
+Rewriting is always homogeneous. That is, the kind of the result of rewriting is
always the same as the kind of the input, modulo zonking. More formally:
(F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
-This invariant means that the kind of a flattened type might not itself be flat.
-
-Recall that in comments we use alpha[flat = ty] to represent a
-flattening skolem variable alpha which has been generated to stand in
-for ty.
+This invariant means that the kind of a rewritten type might not itself be rewritten.
Note that we prefer to leave type synonyms unexpanded when possible,
-so when the flattener encounters one, it first asks whether its
+so when the rewriter encounters one, it first asks whether its
transitive expansion contains any type function applications or is
forgetful -- that is, omits one or more type variables in its RHS. If so,
it expands the synonym and proceeds; if not, it simply returns the
-unexpanded synonym. See also Note [Flattening synonyms].
+unexpanded synonym. See also Note [Rewriting synonyms].
-Note [flatten_args performance]
+Note [rewrite_args performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In programs with lots of type-level evaluation, flatten_args becomes
+In programs with lots of type-level evaluation, rewrite_args becomes
part of a tight loop. For example, see test perf/compiler/T9872a, which
-calls flatten_args a whopping 7,106,808 times. It is thus important
-that flatten_args be efficient.
+calls rewrite_args a whopping 7,106,808 times. It is thus important
+that rewrite_args be efficient.
Performance testing showed that the current implementation is indeed
efficient. It's critically important that zipWithAndUnzipM be
@@ -349,8 +342,8 @@ it. On test T9872a, here are the allocation stats (Dec 16, 2014):
* Specialized, uninlined: 6,639,253,488 bytes allocated in the heap
* Specialized, inlined: 6,281,539,792 bytes allocated in the heap
-To improve performance even further, flatten_args_nom is split off
-from flatten_args, as nominal equality is the common case. This would
+To improve performance even further, rewrite_args_nom is split off
+from rewrite_args, as nominal equality is the common case. This would
be natural to write using mapAndUnzipM, but even inlined, that function
is not as performant as a hand-written loop.
@@ -361,12 +354,12 @@ If you make any change here, pay close attention to the T9872{a,b,c} tests
and T5321Fun.
If we need to make this yet more performant, a possible way forward is to
-duplicate the flattener code for the nominal case, and make that case
+duplicate the rewriter code for the nominal case, and make that case
faster. This doesn't seem quite worth it, yet.
-Note [flatten_exact_fam_app performance]
+Note [rewrite_exact_fam_app performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Once we've got a flat rhs, we extend the famapp-cache to record
+Once we've got a rewritten rhs, we extend the famapp-cache to record
the result. Doing so can save lots of work when the same redex shows up more
than once. Note that we record the link from the redex all the way to its
*final* value, not just the single step reduction.
@@ -380,20 +373,20 @@ actually disastrous: it more than doubles the allocations for T9872a. So
we skip adding to the cache here.
-}
-{-# INLINE flatten_args_tc #-}
-flatten_args_tc
+{-# INLINE rewrite_args_tc #-}
+rewrite_args_tc
:: TyCon -- T
-> Maybe [Role] -- Nothing: ambient role is Nominal; all args are Nominal
-- Otherwise: no assumptions; use roles provided
-> [Type] -- Arg types [t1,..,tn]
- -> FlatM ( [Xi] -- List of flattened args [x1,..,xn]
+ -> RewriteM ( [Xi] -- List of rewritten args [x1,..,xn]
-- 1-1 corresp with [t1,..,tn]
, [Coercion] -- List of arg coercions [co1,..,con]
-- 1-1 corresp with [t1,..,tn]
-- coi :: xi ~r ti
, MCoercionN) -- Result coercion, rco
-- rco : (T t1..tn) ~N (T (x1 |> co1) .. (xn |> con))
-flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet
+rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet
-- NB: TyCon kinds are always closed
where
(bndrs, named)
@@ -405,47 +398,47 @@ flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet
!any_named_bndrs = named || inner_named
-- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.
-{-# INLINE flatten_args #-}
-flatten_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
+{-# INLINE rewrite_args #-}
+rewrite_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
-- named.
-> Kind -> TcTyCoVarSet -- function kind; kind's free vars
-> Maybe [Role] -> [Type] -- these are in 1-to-1 correspondence
-- Nothing: use all Nominal
- -> FlatM ([Xi], [Coercion], MCoercionN)
+ -> RewriteM ([Xi], [Coercion], MCoercionN)
-- Coercions :: Xi ~ Type, at roles given
-- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(fun tys)
-- That is, the third coercion relates the kind of some function (whose kind is
-- passed as the first parameter) instantiated at xis to the kind of that
--- function instantiated at the tys. This is useful in keeping flattening
+-- function instantiated at the tys. This is useful in keeping rewriting
-- homoegeneous. The list of roles must be at least as long as the list of
-- types.
-flatten_args orig_binders
+rewrite_args orig_binders
any_named_bndrs
orig_inner_ki
orig_fvs
orig_m_roles
orig_tys
= case (orig_m_roles, any_named_bndrs) of
- (Nothing, False) -> flatten_args_fast orig_tys
- _ -> flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
+ (Nothing, False) -> rewrite_args_fast orig_tys
+ _ -> rewrite_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
where orig_roles = fromMaybe (repeat Nominal) orig_m_roles
-{-# INLINE flatten_args_fast #-}
--- | fast path flatten_args, in which none of the binders are named and
+{-# INLINE rewrite_args_fast #-}
+-- | fast path rewrite_args, in which none of the binders are named and
-- therefore we can avoid tracking a lifting context.
-- There are many bang patterns in here. It's been observed that they
-- greatly improve performance of an optimized build.
-- The T9872 test cases are good witnesses of this fact.
-flatten_args_fast :: [Type]
- -> FlatM ([Xi], [Coercion], MCoercionN)
-flatten_args_fast orig_tys
+rewrite_args_fast :: [Type]
+ -> RewriteM ([Xi], [Coercion], MCoercionN)
+rewrite_args_fast orig_tys
= fmap finish (iterate orig_tys)
where
iterate :: [Type]
- -> FlatM ([Xi], [Coercion])
+ -> RewriteM ([Xi], [Coercion])
iterate (ty:tys) = do
- (xi, co) <- flatten_one ty
+ (xi, co) <- rewrite_one ty
(xis, cos) <- iterate tys
pure (xi : xis, co : cos)
iterate [] = pure ([], [])
@@ -454,16 +447,16 @@ flatten_args_fast orig_tys
finish :: ([Xi], [Coercion]) -> ([Xi], [Coercion], MCoercionN)
finish (xis, cos) = (xis, cos, MRefl)
-{-# INLINE flatten_args_slow #-}
--- | Slow path, compared to flatten_args_fast, because this one must track
+{-# INLINE rewrite_args_slow #-}
+-- | Slow path, compared to rewrite_args_fast, because this one must track
-- a lifting context.
-flatten_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
+rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
-> [Role] -> [Type]
- -> FlatM ([Xi], [Coercion], MCoercionN)
-flatten_args_slow binders inner_ki fvs roles tys
--- Arguments used dependently must be flattened with proper coercions, but
--- we're not guaranteed to get a proper coercion when flattening with the
--- "Derived" flavour. So we must call noBogusCoercions when flattening arguments
+ -> RewriteM ([Xi], [Coercion], MCoercionN)
+rewrite_args_slow binders inner_ki fvs roles tys
+-- Arguments used dependently must be rewritten with proper coercions, but
+-- we're not guaranteed to get a proper coercion when rewriting with the
+-- "Derived" flavour. So we must call noBogusCoercions when rewriting arguments
-- corresponding to binders that are dependent. However, we might legitimately
-- have *more* arguments than binders, in the case that the inner_ki is a variable
-- that gets instantiated with a Π-type. We conservatively choose not to produce
@@ -471,76 +464,76 @@ flatten_args_slow binders inner_ki fvs roles tys
-- a Derived rewriting a Derived. The solution would be to generate evidence for
-- Deriveds, thus avoiding this whole noBogusCoercions idea. See also
-- Note [No derived kind equalities]
- = do { flattened_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True)
+ = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True)
roles tys
- ; return (simplifyArgsWorker binders inner_ki fvs roles flattened_args) }
+ ; return (simplifyArgsWorker binders inner_ki fvs roles rewritten_args) }
where
{-# INLINE fl #-}
fl :: Bool -- must we ensure to produce a real coercion here?
-- see comment at top of function
- -> Role -> Type -> FlatM (Xi, Coercion)
+ -> Role -> Type -> RewriteM (Xi, Coercion)
fl True r ty = noBogusCoercions $ fl1 r ty
fl False r ty = fl1 r ty
{-# INLINE fl1 #-}
- fl1 :: Role -> Type -> FlatM (Xi, Coercion)
+ fl1 :: Role -> Type -> RewriteM (Xi, Coercion)
fl1 Nominal ty
= setEqRel NomEq $
- flatten_one ty
+ rewrite_one ty
fl1 Representational ty
= setEqRel ReprEq $
- flatten_one ty
+ rewrite_one ty
fl1 Phantom ty
- -- See Note [Phantoms in the flattener]
+ -- See Note [Phantoms in the rewriter]
= do { ty <- liftTcS $ zonkTcType ty
; return (ty, mkReflCo Phantom ty) }
------------------
-flatten_one :: TcType -> FlatM (Xi, Coercion)
--- Flatten a type to get rid of type function applications, returning
+rewrite_one :: TcType -> RewriteM (Xi, Coercion)
+-- Rewrite a type to get rid of type function applications, returning
-- the new type-function-free type, and a collection of new equality
--- constraints. See Note [Flattening] for more detail.
+-- constraints. See Note [Rewriting] for more detail.
--
-- Postcondition: Coercion :: Xi ~ TcType
--- The role on the result coercion matches the EqRel in the FlattenEnv
+-- The role on the result coercion matches the EqRel in the RewriteEnv
-flatten_one ty
- | Just ty' <- flattenView ty -- See Note [Flattening synonyms]
- = flatten_one ty'
+rewrite_one ty
+ | Just ty' <- rewriterView ty -- See Note [Rewriting synonyms]
+ = rewrite_one ty'
-flatten_one xi@(LitTy {})
+rewrite_one xi@(LitTy {})
= do { role <- getRole
; return (xi, mkReflCo role xi) }
-flatten_one (TyVarTy tv)
- = flattenTyVar tv
+rewrite_one (TyVarTy tv)
+ = rewriteTyVar tv
-flatten_one (AppTy ty1 ty2)
- = flatten_app_tys ty1 [ty2]
+rewrite_one (AppTy ty1 ty2)
+ = rewrite_app_tys ty1 [ty2]
-flatten_one (TyConApp tc tys)
+rewrite_one (TyConApp tc tys)
-- If it's a type family application, try to reduce it
| isTypeFamilyTyCon tc
- = flatten_fam_app tc tys
+ = rewrite_fam_app tc tys
-- For * a normal data type application
-- * data family application
- -- we just recursively flatten the arguments.
+ -- we just recursively rewrite the arguments.
| otherwise
- = flatten_ty_con_app tc tys
+ = rewrite_ty_con_app tc tys
-flatten_one ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
- = do { (xi1,co1) <- flatten_one ty1
- ; (xi2,co2) <- flatten_one ty2
- ; (xi3,co3) <- setEqRel NomEq $ flatten_one mult
+rewrite_one ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
+ = do { (xi1,co1) <- rewrite_one ty1
+ ; (xi2,co2) <- rewrite_one ty2
+ ; (xi3,co3) <- setEqRel NomEq $ rewrite_one mult
; role <- getRole
; return (ty { ft_mult = xi3, ft_arg = xi1, ft_res = xi2 }
, mkFunCo role co3 co1 co2) }
-flatten_one ty@(ForAllTy {})
--- TODO (RAE): This is inadequate, as it doesn't flatten the kind of
+rewrite_one ty@(ForAllTy {})
+-- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of
-- the bound tyvar. Doing so will require carrying around a substitution
-- and the usual substTyVarBndr-like silliness. Argh.
@@ -548,56 +541,56 @@ flatten_one ty@(ForAllTy {})
-- applications inside the forall involve the bound type variables.
= do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty
tvs = binderVars bndrs
- ; (rho', co) <- flatten_one rho
+ ; (rho', co) <- rewrite_one rho
; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
-flatten_one (CastTy ty g)
- = do { (xi, co) <- flatten_one ty
- ; (g', _) <- flatten_co g
+rewrite_one (CastTy ty g)
+ = do { (xi, co) <- rewrite_one ty
+ ; (g', _) <- rewrite_co g
; role <- getRole
; return (mkCastTy xi g', castCoercionKind1 co role xi ty g') }
-- It makes a /big/ difference to call castCoercionKind1 not
-- the more general castCoercionKind2.
-- See Note [castCoercionKind1] in GHC.Core.Coercion
-flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
+rewrite_one (CoercionTy co) = first mkCoercionTy <$> rewrite_co co
--- | "Flatten" a coercion. Really, just zonk it so we can uphold
--- (F1) of Note [Flattening]
-flatten_co :: Coercion -> FlatM (Coercion, Coercion)
-flatten_co co
+-- | "Rewrite" a coercion. Really, just zonk it so we can uphold
+-- (F1) of Note [Rewriting]
+rewrite_co :: Coercion -> RewriteM (Coercion, Coercion)
+rewrite_co co
= do { co <- liftTcS $ zonkCo co
; env_role <- getRole
; let co' = mkTcReflCo env_role (mkCoercionTy co)
; return (co, co') }
--- flatten (nested) AppTys
-flatten_app_tys :: Type -> [Type] -> FlatM (Xi, Coercion)
+-- rewrite (nested) AppTys
+rewrite_app_tys :: Type -> [Type] -> RewriteM (Xi, Coercion)
-- commoning up nested applications allows us to look up the function's kind
-- only once. Without commoning up like this, we would spend a quadratic amount
-- of time looking up functions' types
-flatten_app_tys (AppTy ty1 ty2) tys = flatten_app_tys ty1 (ty2:tys)
-flatten_app_tys fun_ty arg_tys
- = do { (fun_xi, fun_co) <- flatten_one fun_ty
- ; flatten_app_ty_args fun_xi fun_co arg_tys }
-
--- Given a flattened function (with the coercion produced by flattening) and
--- a bunch of unflattened arguments, flatten the arguments and apply.
--- The coercion argument's role matches the role stored in the FlatM monad.
+rewrite_app_tys (AppTy ty1 ty2) tys = rewrite_app_tys ty1 (ty2:tys)
+rewrite_app_tys fun_ty arg_tys
+ = do { (fun_xi, fun_co) <- rewrite_one fun_ty
+ ; rewrite_app_ty_args fun_xi fun_co arg_tys }
+
+-- Given a rewritten function (with the coercion produced by rewriting) and
+-- a bunch of unrewritten arguments, rewrite the arguments and apply.
+-- The coercion argument's role matches the role stored in the RewriteM monad.
--
-- The bang patterns used here were observed to improve performance. If you
-- wish to remove them, be sure to check for regeressions in allocations.
-flatten_app_ty_args :: Xi -> Coercion -> [Type] -> FlatM (Xi, Coercion)
-flatten_app_ty_args fun_xi fun_co []
- -- this will be a common case when called from flatten_fam_app, so shortcut
+rewrite_app_ty_args :: Xi -> Coercion -> [Type] -> RewriteM (Xi, Coercion)
+rewrite_app_ty_args fun_xi fun_co []
+ -- this will be a common case when called from rewrite_fam_app, so shortcut
= return (fun_xi, fun_co)
-flatten_app_ty_args fun_xi fun_co arg_tys
+rewrite_app_ty_args fun_xi fun_co arg_tys
= do { (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of
Just (tc, xis) ->
do { let tc_roles = tyConRolesRepresentational tc
arg_roles = dropList xis tc_roles
; (arg_xis, arg_cos, kind_co)
- <- flatten_vector (tcTypeKind fun_xi) arg_roles arg_tys
+ <- rewrite_vector (tcTypeKind fun_xi) arg_roles arg_tys
-- Here, we have fun_co :: T xi1 xi2 ~ ty
-- and we need to apply fun_co to the arg_cos. The problem is
@@ -616,7 +609,7 @@ flatten_app_ty_args fun_xi fun_co arg_tys
; return (app_xi, app_co, kind_co) }
Nothing ->
do { (arg_xis, arg_cos, kind_co)
- <- flatten_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
+ <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
; let arg_xi = mkAppTys fun_xi arg_xis
arg_co = mkAppCos fun_co arg_cos
; return (arg_xi, arg_co, kind_co) }
@@ -624,18 +617,18 @@ flatten_app_ty_args fun_xi fun_co arg_tys
; role <- getRole
; return (homogenise_result xi co role kind_co) }
-flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
-flatten_ty_con_app tc tys
+rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
+rewrite_ty_con_app tc tys
= do { role <- getRole
; let m_roles | Nominal <- role = Nothing
| otherwise = Just $ tyConRolesX role tc
- ; (xis, cos, kind_co) <- flatten_args_tc tc m_roles tys
+ ; (xis, cos, kind_co) <- rewrite_args_tc tc m_roles tys
; let tyconapp_xi = mkTyConApp tc xis
tyconapp_co = mkTyConAppCo role tc cos
; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) }
--- Make the result of flattening homogeneous (Note [Flattening] (F2))
-homogenise_result :: Xi -- a flattened type
+-- Make the result of rewriting homogeneous (Note [Rewriting] (F2))
+homogenise_result :: Xi -- a rewritten type
-> Coercion -- :: xi ~r original ty
-> Role -- r
-> MCoercionN -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty)
@@ -646,22 +639,22 @@ homogenise_result xi co r mco@(MCo kind_co)
= (xi `mkCastTy` kind_co, (mkSymCo $ GRefl r xi mco) `mkTransCo` co)
{-# INLINE homogenise_result #-}
--- Flatten a vector (list of arguments).
-flatten_vector :: Kind -- of the function being applied to these arguments
- -> [Role] -- If we're flatten w.r.t. ReprEq, what roles do the
+-- Rewrite a vector (list of arguments).
+rewrite_vector :: Kind -- of the function being applied to these arguments
+ -> [Role] -- If we're rewrite w.r.t. ReprEq, what roles do the
-- args have?
- -> [Type] -- the args to flatten
- -> FlatM ([Xi], [Coercion], MCoercionN)
-flatten_vector ki roles tys
+ -> [Type] -- the args to rewrite
+ -> RewriteM ([Xi], [Coercion], MCoercionN)
+rewrite_vector ki roles tys
= do { eq_rel <- getEqRel
; case eq_rel of
- NomEq -> flatten_args bndrs
+ NomEq -> rewrite_args bndrs
any_named_bndrs
inner_ki
fvs
Nothing
tys
- ReprEq -> flatten_args bndrs
+ ReprEq -> rewrite_args bndrs
any_named_bndrs
inner_ki
fvs
@@ -671,10 +664,10 @@ flatten_vector ki roles tys
where
(bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki -- "RAE" fix
fvs = tyCoVarsOfType ki
-{-# INLINE flatten_vector #-}
+{-# INLINE rewrite_vector #-}
{-
-Note [Flattening synonyms]
+Note [Rewriting synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Not expanding synonyms aggressively improves error messages, and
keeps types smaller. But we need to take care.
@@ -704,7 +697,7 @@ so those families can get reduced.
************************************************************************
* *
- Flattening a type-family application
+ Rewriting a type-family application
* *
************************************************************************
@@ -724,13 +717,13 @@ STEP 2. Try top-level instances. Note that we haven't simplified the arguments
If an instance is found, jump to FINISH.
-STEP 3. Flatten all arguments. This might expose more information so that we
+STEP 3. Rewrite all arguments. This might expose more information so that we
can use a top-level instance.
Continue to the next step.
-STEP 4. Try the inerts. Note that we try the inerts *after* flattening the
- arguments, because the inerts will have flattened LHSs.
+STEP 4. Try the inerts. Note that we try the inerts *after* rewriting the
+ arguments, because the inerts will have rewritten LHSs.
If an inert is found, jump to FINISH.
@@ -747,7 +740,7 @@ STEP 6. Try top-level instances, which might trigger now that we know more
STEP 7. No progress to be made. Return what we have. (Do not do FINISH.)
FINISH 1. We've made a reduction, but the new type may still have more
- work to do. So flatten the new type.
+ work to do. So rewrite the new type.
FINISH 2. Add the result to the famapp-cache, connecting the type we started
with to the one we ended with.
@@ -755,17 +748,17 @@ FINISH 2. Add the result to the famapp-cache, connecting the type we started
Because STEP 1/2 and STEP 5/6 happen the same way, they are abstracted into
try_to_reduce.
-FINISH is naturally implemented in `finish`. But, Note [flatten_exact_fam_app performance]
+FINISH is naturally implemented in `finish`. But, Note [rewrite_exact_fam_app performance]
tells us that we should not add to the famapp-cache after STEP 1/2. So `finish`
is inlined in that case, and only FINISH 1 is performed.
-}
-flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
- -- flatten_fam_app can be over-saturated
- -- flatten_exact_fam_app lifts out the application to top level
+rewrite_fam_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
+ -- rewrite_fam_app can be over-saturated
+ -- rewrite_exact_fam_app lifts out the application to top level
-- Postcondition: Coercion :: Xi ~ F tys
-flatten_fam_app tc tys -- Can be over-saturated
+rewrite_fam_app tc tys -- Can be over-saturated
= ASSERT2( tys `lengthAtLeast` tyConArity tc
, ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
@@ -774,22 +767,22 @@ flatten_fam_app tc tys -- Can be over-saturated
-- in which case the remaining arguments should
-- be dealt with by AppTys
do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
- ; (xi1, co1) <- flatten_exact_fam_app tc tys1
+ ; (xi1, co1) <- rewrite_exact_fam_app tc tys1
-- co1 :: xi1 ~ F tys1
- ; flatten_app_ty_args xi1 co1 tys_rest }
+ ; rewrite_app_ty_args xi1 co1 tys_rest }
-- the [TcType] exactly saturate the TyCon
-- See Note [How to normalise a family application]
-flatten_exact_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
-flatten_exact_fam_app tc tys
+rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
+rewrite_exact_fam_app tc tys
= do { checkStackDepth (mkTyConApp tc tys)
-- STEP 1/2. Try to reduce without reducing arguments first.
; result1 <- try_to_reduce tc tys
; case result1 of
-- Don't use the cache;
- -- See Note [flatten_exact_fam_app performance]
+ -- See Note [rewrite_exact_fam_app performance]
{ Just (co, xi) -> finish False (xi, co)
; Nothing ->
@@ -797,9 +790,9 @@ flatten_exact_fam_app tc tys
do { eq_rel <- getEqRel
-- checking eq_rel == NomEq saves ~0.5% in T9872a
; (xis, cos, kind_co) <- if eq_rel == NomEq
- then flatten_args_tc tc Nothing tys
+ then rewrite_args_tc tc Nothing tys
else setEqRel NomEq $
- flatten_args_tc tc Nothing tys
+ rewrite_args_tc tc Nothing tys
-- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys)
; let role = eqRelRole eq_rel
@@ -821,7 +814,7 @@ flatten_exact_fam_app tc tys
-- co :: F xis ~ir xi
| fr `eqCanRewriteFR` (flavour, eq_rel) ->
- do { traceFlat "rewrite family application with inert"
+ do { traceRewriteM "rewrite family application with inert"
(ppr tc <+> ppr xis $$ ppr xi)
; finish True (homogenise xi downgraded_co) }
-- this will sometimes duplicate an inert in the cache,
@@ -845,12 +838,12 @@ flatten_exact_fam_app tc tys
reduced = mkTyConApp tc xis }}}}}
where
-- call this if the above attempts made progress.
- -- This recursively flattens the result and then adds to the cache
+ -- This recursively rewrites the result and then adds to the cache
finish :: Bool -- add to the cache?
- -> (Xi, Coercion) -> FlatM (Xi, Coercion)
+ -> (Xi, Coercion) -> RewriteM (Xi, Coercion)
finish use_cache (xi, co)
- = do { -- flatten the result: FINISH 1
- (fully, fully_co) <- bumpDepth $ flatten_one xi
+ = do { -- rewrite the result: FINISH 1
+ (fully, fully_co) <- bumpDepth $ rewrite_one xi
; let final_co = fully_co `mkTcTransCo` co
; eq_rel <- getEqRel
; flavour <- getFlavour
@@ -864,9 +857,9 @@ flatten_exact_fam_app tc tys
; return (fully, final_co) }
{-# INLINE finish #-}
--- Returned coercion is output ~r input, where r is the role in the FlatM monad
+-- Returned coercion is output ~r input, where r is the role in the RewriteM monad
-- See Note [How to normalise a family application]
-try_to_reduce :: TyCon -> [TcType] -> FlatM (Maybe (TcCoercion, TcType))
+try_to_reduce :: TyCon -> [TcType] -> RewriteM (Maybe (TcCoercion, TcType))
try_to_reduce tc tys
= do { result <- liftTcS $ firstJustsM [ lookupFamAppCache tc tys -- STEP 5
, matchFam tc tys ] -- STEP 6
@@ -874,10 +867,10 @@ try_to_reduce tc tys
where
-- The result above is always Nominal. We might want a Representational
-- coercion; this downgrades (and prints, out of convenience).
- downgrade :: Maybe (TcCoercionN, TcType) -> FlatM (Maybe (TcCoercion, TcType))
+ downgrade :: Maybe (TcCoercionN, TcType) -> RewriteM (Maybe (TcCoercion, TcType))
downgrade Nothing = return Nothing
downgrade result@(Just (co, xi))
- = do { traceFlat "Eager T.F. reduction success" $
+ = do { traceRewriteM "Eager T.F. reduction success" $
vcat [ ppr tc, ppr tys, ppr xi
, ppr co <+> dcolon <+> ppr (coercionKind co)
]
@@ -891,61 +884,61 @@ try_to_reduce tc tys
{-
************************************************************************
* *
- Flattening a type variable
+ Rewriting a type variable
* *
********************************************************************* -}
--- | The result of flattening a tyvar "one step".
-data FlattenTvResult
- = FTRNotFollowed
+-- | The result of rewriting a tyvar "one step".
+data RewriteTvResult
+ = RTRNotFollowed
-- ^ The inert set doesn't make the tyvar equal to anything else
- | FTRFollowed TcType Coercion
- -- ^ The tyvar flattens to a not-necessarily flat other type.
+ | RTRFollowed TcType Coercion
+ -- ^ The tyvar rewrites to a not-necessarily rewritten other type.
-- co :: new type ~r old type, where the role is determined by
- -- the FlattenEnv
+ -- the RewriteEnv
-flattenTyVar :: TyVar -> FlatM (Xi, Coercion)
-flattenTyVar tv
- = do { mb_yes <- flatten_tyvar1 tv
+rewriteTyVar :: TyVar -> RewriteM (Xi, Coercion)
+rewriteTyVar tv
+ = do { mb_yes <- rewrite_tyvar1 tv
; case mb_yes of
- FTRFollowed ty1 co1 -- Recur
- -> do { (ty2, co2) <- flatten_one ty1
- -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2)
+ RTRFollowed ty1 co1 -- Recur
+ -> do { (ty2, co2) <- rewrite_one ty1
+ -- ; traceRewriteM "rewriteTyVar2" (ppr tv $$ ppr ty2)
; return (ty2, co2 `mkTransCo` co1) }
- FTRNotFollowed -- Done, but make sure the kind is zonked
- -- Note [Flattening] invariant (F0) and (F1)
+ RTRNotFollowed -- Done, but make sure the kind is zonked
+ -- Note [Rewriting] invariant (F0) and (F1)
-> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
; role <- getRole
; let ty' = mkTyVarTy tv'
; return (ty', mkTcReflCo role ty') } }
-flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
--- "Flattening" a type variable means to apply the substitution to it
+rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
+-- "Rewriting" a type variable means to apply the substitution to it
-- Specifically, look up the tyvar in
-- * the internal MetaTyVar box
-- * the inerts
--- See also the documentation for FlattenTvResult
+-- See also the documentation for RewriteTvResult
-flatten_tyvar1 tv
+rewrite_tyvar1 tv
= do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
; case mb_ty of
- Just ty -> do { traceFlat "Following filled tyvar"
+ Just ty -> do { traceRewriteM "Following filled tyvar"
(ppr tv <+> equals <+> ppr ty)
; role <- getRole
- ; return (FTRFollowed ty (mkReflCo role ty)) } ;
- Nothing -> do { traceFlat "Unfilled tyvar" (pprTyVar tv)
+ ; return (RTRFollowed ty (mkReflCo role ty)) } ;
+ Nothing -> do { traceRewriteM "Unfilled tyvar" (pprTyVar tv)
; fr <- getFlavourRole
- ; flatten_tyvar2 tv fr } }
+ ; rewrite_tyvar2 tv fr } }
-flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
+rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
-- The tyvar is not a filled-in meta-tyvar
-- Try in the inert equalities
-- See Definition [Applying a generalised substitution] in GHC.Tc.Solver.Monad
--- See Note [Stability of flattening] in GHC.Tc.Solver.Monad
+-- See Note [Stability of rewriting] in GHC.Tc.Solver.Monad
-flatten_tyvar2 tv fr@(_, eq_rel)
+rewrite_tyvar2 tv fr@(_, eq_rel)
= do { ieqs <- liftTcS $ getInertEqs
; case lookupDVarEnv ieqs tv of
Just (EqualCtList (ct :| _)) -- If the first doesn't work,
@@ -954,7 +947,7 @@ flatten_tyvar2 tv fr@(_, eq_rel)
, cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
, let ct_fr = (ctEvFlavour ctev, ct_eq_rel)
, ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR
- -> do { traceFlat "Following inert tyvar"
+ -> do { traceRewriteM "Following inert tyvar"
(ppr tv <+>
equals <+>
ppr rhs_ty $$ ppr ctev)
@@ -967,12 +960,12 @@ flatten_tyvar2 tv fr@(_, eq_rel)
(NomEq, NomEq) -> rewrite_co1
(NomEq, ReprEq) -> mkSubCo rewrite_co1
- ; return (FTRFollowed rhs_ty rewrite_co) }
+ ; return (RTRFollowed rhs_ty rewrite_co) }
-- NB: ct is Derived then fmode must be also, hence
-- we are not going to touch the returned coercion
-- so ctEvCoercion is fine.
- _other -> return FTRNotFollowed }
+ _other -> return RTRNotFollowed }
{-
Note [An alternative story for the inert substitution]
@@ -986,7 +979,7 @@ We used (GHC 7.8) to have this story for the inert substitution inert_eqs
* They are *inert* in the weaker sense that there is no infinite chain of
(i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc
-This means that flattening must be recursive, but it does allow
+This means that rewriting must be recursive, but it does allow
[G] a ~ [b]
[G] b ~ Maybe c
@@ -998,7 +991,7 @@ only if (a) the work item can rewrite the inert AND
This is significantly harder to think about. It can save a LOT of work
in occurs-check cases, but we don't care about them much. #5837
is an example, but it causes trouble only with the old (pre-Fall 2020)
-flattening story. It is unclear if there is any gain w.r.t. to
+rewriting story. It is unclear if there is any gain w.r.t. to
the new story.
-}
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 05fd70c674..3950f1db77 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -117,8 +117,8 @@ import qualified Data.Semigroup ( (<>) )
Note [CEqCan occurs check]
~~~~~~~~~~~~~~~~~~~~~~~~~~
A CEqCan relates a CanEqLHS (a type variable or type family applications) on
-its left to an arbitrary type on its right. It is used for rewriting, in the
-flattener. Because it is used for rewriting, it would be disastrous if the RHS
+its left to an arbitrary type on its right. It is used for rewriting.
+Because it is used for rewriting, it would be disastrous if the RHS
were to mention the LHS: this would cause a loop in rewriting.
We thus perform an occurs-check. There is, of course, some subtlety:
@@ -146,8 +146,8 @@ The occurs check is performed in GHC.Tc.Utils.Unify.checkTypeEq.
-}
-- | A 'Xi'-type is one that has been fully rewritten with respect
--- to the inert set; that is, it has been flattened by the algorithm
--- in GHC.Tc.Solver.Flatten. (Historical note: 'Xi', for years and years,
+-- to the inert set; that is, it has been rewritten by the algorithm
+-- in GHC.Tc.Solver.Rewrite. (Historical note: 'Xi', for years and years,
-- meant that a type was type-family-free. It does *not* mean this
-- any more.)
type Xi = TcType
@@ -257,7 +257,7 @@ data Hole
, hole_loc :: CtLoc -- ^ Where hole was written
}
-- For the hole_loc, we usually only want the TcLclEnv stored within.
- -- Except when we flatten, where we need a whole location. And this
+ -- Except when we rewrite, where we need a whole location. And this
-- might get reported to the user if reducing type families in a
-- hole type loops.
@@ -298,7 +298,7 @@ data CtIrredStatus
| BlockedCIS HoleSet
-- this constraint is blocked on the coercion hole(s) listed
-- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
- -- Wrinkle (4a). Why store the HoleSet? See Wrinkle (2a) of that
+ -- Wrinkle (4a). Why store the HoleSet? See Wrinkle (2) of that
-- same Note.
-- INVARIANT: A BlockedCIS is a homogeneous equality whose
-- left hand side can fit in a CanEqLHS.
@@ -527,19 +527,19 @@ tyCoFVsOfCts = foldr (unionFV . tyCoFVsOfCt) emptyFV
-- | Returns free variables of WantedConstraints as a non-deterministic
-- set. See Note [Deterministic FV] in "GHC.Utils.FV".
tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet
--- Only called on *zonked* things, hence no need to worry about flatten-skolems
+-- Only called on *zonked* things
tyCoVarsOfWC = fvVarSet . tyCoFVsOfWC
-- | Returns free variables of WantedConstraints as a deterministically
-- ordered list. See Note [Deterministic FV] in "GHC.Utils.FV".
tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]
--- Only called on *zonked* things, hence no need to worry about flatten-skolems
+-- Only called on *zonked* things
tyCoVarsOfWCList = fvVarList . tyCoFVsOfWC
-- | Returns free variables of WantedConstraints as a composable FV
-- computation. See Note [Deterministic FV] in "GHC.Utils.FV".
tyCoFVsOfWC :: WantedConstraints -> FV
--- Only called on *zonked* things, hence no need to worry about flatten-skolems
+-- Only called on *zonked* things
tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes })
= tyCoFVsOfCts simple `unionFV`
tyCoFVsOfBag tyCoFVsOfImplic implic `unionFV`
@@ -548,7 +548,7 @@ tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes })
-- | Returns free variables of Implication as a composable FV computation.
-- See Note [Deterministic FV] in "GHC.Utils.FV".
tyCoFVsOfImplic :: Implication -> FV
--- Only called on *zonked* things, hence no need to worry about flatten-skolems
+-- Only called on *zonked* things
tyCoFVsOfImplic (Implic { ic_skols = skols
, ic_given = givens
, ic_wanted = wanted })
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 62fab5500b..ccb9152e01 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -986,7 +986,6 @@ writeMetaTyVarRef tyvar ref ty
; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
-- Check for level OK
- -- See Note [Level check when unifying]
; MASSERT2( level_check_ok, level_check_msg )
-- Check Kinds ok
@@ -1007,22 +1006,6 @@ writeMetaTyVarRef tyvar ref ty
double_upd_msg details = hang (text "Double update of meta tyvar")
2 (ppr tyvar $$ ppr details)
-{- Note [Level check when unifying]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When unifying
- alpha:lvl := ty
-we expect that the TcLevel of 'ty' will be <= lvl.
-However, during unflatting we do
- fuv:l := ty:(l+1)
-which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
-See Note [TcLevel assignment] in GHC.Tc.Utils.TcType.
--}
-
-{-
-% Generating fresh variables for pattern match check
--}
-
-
{-
************************************************************************
* *
@@ -2174,7 +2157,7 @@ we have alpha := N Int, where N is a newtype.) Besides, the constraint
will be canonicalised again, so there is little benefit in keeping the
CEqCan structure.
-NB: Constraints are always re-flattened etc by the canonicaliser in
+NB: Constraints are always rewritten etc by the canonicaliser in
@GHC.Tc.Solver.Canonical@ even if they come in as CDictCan. Only canonical constraints that
are actually in the inert set carry all the guarantees. So it is okay if zonkCt
creates e.g. a CDictCan where the cc_tyars are /not/ fully reduced.
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 9d11505053..3e52419772 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -341,10 +341,6 @@ GHC #12785.
type TcCoVar = CoVar -- Used only during type inference
type TcType = Type -- A TcType can have mutable type variables
type TcTyCoVar = Var -- Either a TcTyVar or a CoVar
- -- Invariant on ForAllTy in TcTypes:
- -- forall a. T
- -- a cannot occur inside a MutTyVar in T; that is,
- -- T is "flattened" before quantifying over a
type TcTyVarBinder = TyVarBinder
type TcInvisTVBinder = InvisTVBinder
@@ -1647,7 +1643,7 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
-- sometimes hard to know directly because @ty@ might have some casts
-- obscuring the FunTy. And 'splitAppTy' is difficult because we can't
-- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or
- -- res is unzonked/unflattened. Thus this function, which handles this
+ -- res is unzonked. Thus this function, which handles this
-- corner case.
eqFunTy :: RnEnv2 -> Mult -> Type -> Type -> Type -> Bool
-- Last arg is /not/ FunTy
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 3529f598f8..b51bd6b7a9 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1668,8 +1668,7 @@ least in some cases. But it's disastrous for test case perf/compiler/T3064.
Here is the problem: Suppose we have (F ty) where we also have [G] F ty ~ a.
What do we do? Do we reduce F? Or do we use the given? Hard to know what's
best. GHC reduces. This is a disaster for T3064, where the type's size
-spirals out of control during reduction. (We're not helped by the fact that
-the flattener re-flattens all the arguments every time around.) If we prevent
+spirals out of control during reduction. If we prevent
unification with type families, then the solver happens to use the equality
before expanding the type family.
diff --git a/compiler/GHC/Utils/Monad.hs b/compiler/GHC/Utils/Monad.hs
index 19b0667ceb..da415ba44c 100644
--- a/compiler/GHC/Utils/Monad.hs
+++ b/compiler/GHC/Utils/Monad.hs
@@ -88,9 +88,7 @@ zipWith4M f xs ys ws zs = sequenceA (zipWith4 f xs ys ws zs)
zipWithAndUnzipM :: Monad m
=> (a -> b -> m (c, d)) -> [a] -> [b] -> m ([c], [d])
-{-# INLINABLE zipWithAndUnzipM #-}
--- See Note [flatten_args performance] in GHC.Tc.Solver.Flatten for why this
--- pragma is essential.
+{-# INLINABLE zipWithAndUnzipM #-} -- this allows specialization to a given monad
zipWithAndUnzipM f (x:xs) (y:ys)
= do { (c, d) <- f x y
; (cs, ds) <- zipWithAndUnzipM f xs ys
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index ffee979a90..86b86774a4 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -592,7 +592,7 @@ Library
GHC.Tc.Plugin
GHC.Tc.Solver
GHC.Tc.Solver.Canonical
- GHC.Tc.Solver.Flatten
+ GHC.Tc.Solver.Rewrite
GHC.Tc.Solver.Interact
GHC.Tc.Solver.Monad
GHC.Tc.TyCl
View Lorry Controller Status