Commit 8bb52d91 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot
Browse files

Remove flattening variables

This patch redesigns the flattener to simplify type family applications
directly instead of using flattening meta-variables and skolems. The key new
innovation is the CanEqLHS type and the new CEqCan constraint (Ct). A CanEqLHS
is either a type variable or exactly-saturated type family application; either
can now be rewritten using a CEqCan constraint in the inert set.

Because the flattener no longer reduces all type family applications to
variables, there was some performance degradation if a lengthy type family
application is now flattened over and over (not making progress). To
compensate, this patch contains some extra optimizations in the flattener,
leading to a number of performance improvements.

Close #18875.
Close #18910.

There are many extra parts of the compiler that had to be affected in writing
this patch:

* The family-application cache (formerly the flat-cache) sometimes stores
  coercions built from Given inerts. When these inerts get kicked out, we must
  kick out from the cache as well. (This was, I believe, true previously, but
  somehow never caused trouble.) Kicking out from the cache requires adding a
  filterTM function to TrieMap.

* This patch obviates the need to distinguish "blocking" coercion holes from
  non-blocking ones (which, previously, arose from CFunEqCans). There is thus
  some simplification around coercion holes.

* Extra commentary throughout parts of the code I read through, to preserve
  the knowledge I gained while working.

* A change in the pure unifier around unifying skolems with other types.
  Unifying a skolem now leads to SurelyApart, not MaybeApart, as documented
  in Note [Binding when looking up instances] in GHC.Core.InstEnv.

* Some more use of MCoercion where appropriate.

* Previously, class-instance lookup automatically noticed that e.g. C Int was
  a "unifier" to a target [W] C (F Bool), because the F Bool was flattened to
  a variable. Now, a little more care must be taken around checking for
  unifying instances.

* Previously, tcSplitTyConApp_maybe would split (Eq a => a). This is silly,
  because (=>) is not a tycon in Haskell. Fixed now, but there are some
  knock-on changes in e.g. TrieMap code and in the canonicaliser.

* New function anyFreeVarsOf{Type,Co} to check whether a free variable
  satisfies a certain predicate.

* Type synonyms now remember whether or not they are "forgetful"; a forgetful
  synonym drops at least one argument. This is useful when flattening; see
  flattenView.

* The pattern-match completeness checker invokes the solver. This invocation
  might need to look through newtypes when checking representational equality.
  Thus, the desugarer needs to keep track of the in-scope variables to know
  what newtype constructors are in scope. I bet this bug was around before but
  never noticed.

* Extra-constraints wildcards are no longer simplified before printing.
  See Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver.

* Whether or not there are Given equalities has become slightly subtler.
  See the new HasGivenEqs datatype.

* Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
  explains a significant new wrinkle in the new approach.

* See Note [What might match later?] in GHC.Tc.Solver.Interact, which
  explains the fix to #18910.

* The inert_count field of InertCans wasn't actually used, so I removed
  it.

Though I (Richard) did the implementation, Simon PJ was very involved
in design and review.

This updates the Haddock submodule to avoid #18932 by adding
a type signature.

-------------------------
Metric Decrease:
    T12227
    T5030
    T9872a
    T9872b
    T9872c
Metric Increase:
    T9872d
-------------------------
parent 0dd45d0a
......@@ -141,6 +141,7 @@ instance TrieMap LabelMap where
alterTM k f m = mapAlter f k m
foldTM k m z = mapFoldr k z m
mapTM f m = mapMap f m
filterTM f m = mapFilter f m
-----------------------------------------------------------------------------
-- FactBase
......
......@@ -13,8 +13,8 @@
--
module GHC.Core.Coercion (
-- * Main data type
Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
UnivCoProvenance, CoercionHole(..), BlockSubstFlag(..),
Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionN, MCoercionR,
UnivCoProvenance, CoercionHole(..),
coHoleCoVar, setCoHoleCoVar,
LeftOrRight(..),
Var, CoVar, TyCoVar,
......@@ -69,8 +69,10 @@ module GHC.Core.Coercion (
pickLR,
isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
isReflCoVar_maybe, isGReflMCo,
coToMCo, mkTransMCo, mkTransMCoL,
isReflCoVar_maybe, isGReflMCo, mkGReflLeftMCo, mkGReflRightMCo,
mkCoherenceRightMCo,
coToMCo, mkTransMCo, mkTransMCoL, mkCastTyMCo, mkSymMCo, isReflMCo,
-- ** Coercion variables
mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
......@@ -79,7 +81,7 @@ module GHC.Core.Coercion (
-- ** Free variables
tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
coercionSize,
coercionSize, anyFreeVarsOfCo,
-- ** Substitution
CvSubstEnv, emptyCvSubstEnv,
......@@ -121,7 +123,8 @@ module GHC.Core.Coercion (
simplifyArgsWorker,
badCoercionHole, badCoercionHoleCo
hasCoercionHoleTy, hasCoercionHoleCo,
HoleSet, coercionHolesOfType, coercionHolesOfCo
) where
#include "HsVersions.h"
......@@ -154,6 +157,7 @@ import GHC.Builtin.Types.Prim
import GHC.Data.List.SetOps
import GHC.Data.Maybe
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set
import GHC.Utils.Misc
import GHC.Utils.Outputable
......@@ -331,6 +335,32 @@ mkTransMCoL :: MCoercion -> Coercion -> MCoercion
mkTransMCoL MRefl co2 = MCo co2
mkTransMCoL (MCo co1) co2 = MCo (mkTransCo co1 co2)
-- | Get the reverse of an 'MCoercion'
mkSymMCo :: MCoercion -> MCoercion
mkSymMCo MRefl = MRefl
mkSymMCo (MCo co) = MCo (mkSymCo co)
-- | Cast a type by an 'MCoercion'
mkCastTyMCo :: Type -> MCoercion -> Type
mkCastTyMCo ty MRefl = ty
mkCastTyMCo ty (MCo co) = ty `mkCastTy` co
mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflLeftMCo r ty MRefl = mkReflCo r ty
mkGReflLeftMCo r ty (MCo co) = mkGReflLeftCo r ty co
mkGReflRightMCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflRightMCo r ty MRefl = mkReflCo r ty
mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co
-- | Like 'mkCoherenceRightCo', but with an 'MCoercion'
mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion
mkCoherenceRightMCo _ _ MRefl co2 = co2
mkCoherenceRightMCo r ty (MCo co) co2 = mkCoherenceRightCo r ty co co2
isReflMCo :: MCoercion -> Bool
isReflMCo MRefl = True
isReflMCo _ = False
{-
%************************************************************************
......@@ -1219,7 +1249,7 @@ mkKindCo co
| otherwise
= KindCo co
mkSubCo :: Coercion -> Coercion
mkSubCo :: HasDebugCallStack => Coercion -> Coercion
-- Input coercion is Nominal, result is Representational
-- see also Note [Role twiddling functions]
mkSubCo (Refl ty) = GRefl Representational ty MRefl
......@@ -1675,6 +1705,11 @@ data NormaliseStepResult ev
-- ^ ev is evidence;
-- Usually a co :: old type ~ new type
instance Outputable ev => Outputable (NormaliseStepResult ev) where
ppr NS_Done = text "NS_Done"
ppr NS_Abort = text "NS_Abort"
ppr (NS_Step _ ty ev) = sep [text "NS_Step", ppr ty, ppr ev]
mapStepResult :: (ev1 -> ev2)
-> NormaliseStepResult ev1 -> NormaliseStepResult ev2
mapStepResult f (NS_Step rec_nts ty ev) = NS_Step rec_nts ty (f ev)
......@@ -2634,7 +2669,8 @@ FamInstEnv, and so lives here.
Note [simplifyArgsWorker]
~~~~~~~~~~~~~~~~~~~~~~~~~
Invariant (F2) of Note [Flattening] says that flattening is homogeneous.
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
of arguments, perhaps with dependency. For example, suppose
......@@ -2913,7 +2949,7 @@ simplifyArgsWorker :: [TyCoBinder] -> Kind
-> [(Type, Coercion)] -- flattened type arguments, arg
-- each comes with the coercion used to flatten it,
-- with co :: flattened_type ~ original_type
-> ([Type], [Coercion], CoercionN)
-> ([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),
......@@ -2935,14 +2971,15 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
-> 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
-> ([Type], [Coercion], CoercionN)
-> ([Type], [Coercion], MCoercionN)
go acc_xis acc_cos !lc binders inner_ki _ []
-- The !lc makes the function strict in the lifting context
-- which means GHC can unbox that pair. A modest win.
= (reverse acc_xis, reverse acc_cos, kind_co)
where
final_kind = mkPiTys binders inner_ki
kind_co = liftCoSubst Nominal lc final_kind
kind_co | noFreeVarsOfType final_kind = MRefl
| 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),
......@@ -2998,7 +3035,7 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
(xis_out, cos_out, res_co_out)
= go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_args
in
(xis_out, cos_out, res_co_out `mkTransCo` res_co)
(xis_out, cos_out, res_co_out `mkTransMCoL` res_co)
go _ _ _ _ _ _ _ = panic
"simplifyArgsWorker wandered into deeper water than usual"
......@@ -3024,31 +3061,40 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
%************************************************************************
-}
bad_co_hole_ty :: Type -> Monoid.Any
bad_co_hole_co :: Coercion -> Monoid.Any
(bad_co_hole_ty, _, bad_co_hole_co, _)
has_co_hole_ty :: Type -> Monoid.Any
has_co_hole_co :: Coercion -> Monoid.Any
(has_co_hole_ty, _, has_co_hole_co, _)
= foldTyCo folder ()
where
folder = TyCoFolder { tcf_view = const Nothing
, tcf_tyvar = const2 (Monoid.Any False)
, tcf_covar = const2 (Monoid.Any False)
, tcf_hole = const hole
, tcf_hole = const2 (Monoid.Any True)
, tcf_tycobinder = const2
}
const2 :: a -> b -> c -> a
const2 x _ _ = x
hole :: CoercionHole -> Monoid.Any
hole (CoercionHole { ch_blocker = YesBlockSubst }) = Monoid.Any True
hole _ = Monoid.Any False
-- | Is there a coercion hole in this type?
hasCoercionHoleTy :: Type -> Bool
hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
-- | Is there a coercion hole in this coercion?
hasCoercionHoleCo :: Coercion -> Bool
hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
-- | Is there a blocking coercion hole in this type? See
-- "GHC.Tc.Solver.Canonical" Note [Equalities with incompatible kinds]
badCoercionHole :: Type -> Bool
badCoercionHole = Monoid.getAny . bad_co_hole_ty
-- | A set of 'CoercionHole's
type HoleSet = UniqSet CoercionHole
-- | Is there a blocking coercion hole in this coercion? See
-- GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds]
badCoercionHoleCo :: Coercion -> Bool
badCoercionHoleCo = Monoid.getAny . bad_co_hole_co
-- | Extract out all the coercion holes from a given type
coercionHolesOfType :: Type -> UniqSet CoercionHole
coercionHolesOfCo :: Coercion -> UniqSet CoercionHole
(coercionHolesOfType, _, coercionHolesOfCo, _) = foldTyCo folder ()
where
folder = TyCoFolder { tcf_view = const Nothing -- don't look through synonyms
, tcf_tyvar = \ _ _ -> mempty
, tcf_covar = \ _ _ -> mempty
, tcf_hole = const unitUniqSet
, tcf_tycobinder = \ _ _ _ -> ()
}
......@@ -30,7 +30,7 @@ mkInstCo :: Coercion -> Coercion -> Coercion
mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
mkNomReflCo :: Type -> Coercion
mkKindCo :: Coercion -> Coercion
mkSubCo :: Coercion -> Coercion
mkSubCo :: HasDebugCallStack => Coercion -> Coercion
mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
......
......@@ -584,9 +584,21 @@ instance Outputable CoAxiomRule where
-- Type checking of built-in families
data BuiltInSynFamily = BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
-- Does this reduce on the given arguments?
-- If it does, returns (CoAxiomRule, types to instantiate the rule at, rhs type)
-- That is: mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
-- :: F tys ~r rhs,
-- where the r in the output is coaxrRole of the rule. It is up to the
-- caller to ensure that this role is appropriate.
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
-- If given these type arguments and RHS, returns the equalities that
-- are guaranteed to hold.
, sfInteractInert :: [Type] -> Type ->
[Type] -> Type -> [TypeEqn]
-- If given one set of arguments and result, and another set of arguments
-- and result, returns the equalities that are guaranteed to hold.
}
-- Provides default implementations that do nothing.
......
......@@ -27,7 +27,6 @@ import GHC.Types.Var.Env
import GHC.Data.Pair
import GHC.Data.List.SetOps ( getNth )
import GHC.Core.Unify
import GHC.Core.InstEnv
import Control.Monad ( zipWithM )
import GHC.Utils.Outputable
......@@ -1006,7 +1005,7 @@ checkAxInstCo (AxiomInstCo ax ind cos)
check_no_conflict _ [] = Nothing
check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
-- See Note [Apartness] in GHC.Core.FamInstEnv
| SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
| SurelyApart <- tcUnifyTysFG (const BindMe) flat lhs_incomp
= check_no_conflict flat rest
| otherwise
= Just b
......
......@@ -428,7 +428,8 @@ Here is how we do it:
apart(target, pattern) = not (unify(flatten(target), pattern))
where flatten (implemented in flattenTys, below) converts all type-family
applications into fresh variables. (See Note [Flattening] in GHC.Core.Unify.)
applications into fresh variables. (See
Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.)
Note [Compatibility]
~~~~~~~~~~~~~~~~~~~~
......@@ -1141,6 +1142,7 @@ reduceTyFamApp_maybe envs role tc tys
| Just ax <- isBuiltInSynFamTyCon_maybe tc
, Just (coax,ts,ty) <- sfMatchFam ax tys
, role == coaxrRole coax
= let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
in Just (co, ty)
......@@ -1175,7 +1177,8 @@ findBranch branches target_tys
, cab_incomps = incomps }) = branch
in_scope = mkInScopeSet (unionVarSets $
map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
-- See Note [Flattening] in GHC.Core.Unify
-- See Note [Flattening type-family applications when matching instances]
-- in GHC.Core.Unify
flattened_target = flattenTys in_scope target_tys
in case tcMatchTys tpl_lhs target_tys of
Just subst -- matching worked. now, check for apartness.
......@@ -1192,11 +1195,11 @@ findBranch branches target_tys
-- (POPL '14). This should be used when determining if an equation
-- ('CoAxBranch') of a closed type family can be used to reduce a certain target
-- type family application.
apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure
-- they're flattened! See Note [Flattening]
-- in GHC.Core.Unify
-- (NB: This "flat" is a different
-- "flat" than is used in GHC.Tc.Solver.Flatten.)
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.)
-> CoAxBranch -- ^ the candidate equation we wish to use
-- Precondition: this matches the target
-> Bool -- ^ True <=> equation can fire
......@@ -1316,7 +1319,7 @@ topNormaliseType_maybe env ty
tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
tyFamStepper rec_nts tc tys -- Try to step a type/data family
= case topReduceTyFamApp_maybe env tc tys of
Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, MCo res_co)
Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, res_co)
_ -> NS_Done
---------------
......@@ -1362,14 +1365,14 @@ normalise_tc_app tc tys
assemble_result :: Role -- r, ambient role in NormM monad
-> Type -- nty, result type, possibly of changed kind
-> Coercion -- orig_ty ~r nty, possibly heterogeneous
-> CoercionN -- typeKind(orig_ty) ~N typeKind(nty)
-> MCoercionN -- typeKind(orig_ty) ~N typeKind(nty)
-> (Coercion, Type) -- (co :: orig_ty ~r nty_casted, nty_casted)
-- where nty_casted has same kind as orig_ty
assemble_result r nty orig_to_nty kind_co
= ( final_co, nty_old_kind )
where
nty_old_kind = nty `mkCastTy` mkSymCo kind_co
final_co = mkCoherenceRightCo r nty (mkSymCo kind_co) orig_to_nty
nty_old_kind = nty `mkCastTyMCo` mkSymMCo kind_co
final_co = mkCoherenceRightMCo r nty (mkSymMCo kind_co) orig_to_nty
---------------
-- | Try to simplify a type-family application, by *one* step
......@@ -1378,7 +1381,7 @@ normalise_tc_app tc tys
-- res_co :: typeKind(F tys) ~ typeKind(rhs)
-- Type families and data families; always Representational role
topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type]
-> Maybe (Coercion, Type, Coercion)
-> Maybe (Coercion, Type, MCoercion)
topReduceTyFamApp_maybe envs fam_tc arg_tys
| isFamilyTyCon fam_tc -- type families and data families
, Just (co, rhs) <- reduceTyFamApp_maybe envs role fam_tc ntys
......@@ -1391,7 +1394,7 @@ topReduceTyFamApp_maybe envs fam_tc arg_tys
normalise_tc_args fam_tc arg_tys
normalise_tc_args :: TyCon -> [Type] -- tc tys
-> NormM (Coercion, [Type], CoercionN)
-> NormM (Coercion, [Type], MCoercionN)
-- (co, new_tys), where
-- co :: tc tys ~ tc new_tys; might not be homogeneous
-- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys)
......@@ -1474,14 +1477,14 @@ normalise_type ty
; role <- getRole
; let nty = mkAppTys nfun nargs
nco = mkAppCos fun_co args_cos
nty_casted = nty `mkCastTy` mkSymCo res_co
final_co = mkCoherenceRightCo role nty (mkSymCo res_co) nco
nty_casted = nty `mkCastTyMCo` mkSymMCo res_co
final_co = mkCoherenceRightMCo role nty (mkSymMCo res_co) nco
; return (final_co, nty_casted) } }
normalise_args :: Kind -- of the function
-> [Role] -- roles at which to normalise args
-> [Type] -- args
-> NormM ([Coercion], [Type], Coercion)
-> NormM ([Coercion], [Type], MCoercion)
-- returns (cos, xis, res_co), where each xi is the normalised
-- version of the corresponding type, each co is orig_arg ~ xi,
-- and the res_co :: kind(f orig_args) ~ kind(f xis)
......@@ -1491,7 +1494,7 @@ normalise_args :: Kind -- of the function
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
; return (map mkSymCo cos, xis, mkSymCo res_co) }
; return (map mkSymCo cos, xis, mkSymMCo res_co) }
where
(ki_binders, inner_ki) = splitPiTys fun_ki
fvs = tyCoVarsOfTypes args
......
......@@ -828,18 +828,22 @@ lookupInstEnv' ie vis_mods cls tys
= find ms us rest
| otherwise
= ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tv_set,
= ASSERT2( tys_tv_set `disjointVarSet` tpl_tv_set,
(ppr cls <+> ppr tys <+> ppr all_tvs) $$
(ppr tpl_tvs <+> ppr tpl_tys)
)
-- Unification will break badly if the variables overlap
-- They shouldn't because we allocate separate uniques for them
-- See Note [Template tyvars are fresh]
case tcUnifyTys instanceBindFun tpl_tys tys of
Just _ -> find ms (item:us) rest
Nothing -> find ms us rest
case tcUnifyTysFG instanceBindFun tpl_tys tys of
-- We consider MaybeApart to be a case where the instance might
-- apply in the future. This covers an instance like C Int and
-- a target like [W] C (F a), where F is a type family.
SurelyApart -> find ms us rest
_ -> find ms (item:us) rest
where
tpl_tv_set = mkVarSet tpl_tvs
tys_tv_set = tyCoVarsOfTypes tys
---------------
-- This is the common way to call this function.
......@@ -1023,20 +1027,28 @@ When looking up in the instance environment, or family-instance environment,
we are careful about multiple matches, as described above in
Note [Overlapping instances]
The key_tys can contain skolem constants, and we can guarantee that those
The target tys can contain skolem constants. For existentials and instance variables,
we can guarantee that those
are never going to be instantiated to anything, so we should not involve
them in the unification test. Example:
them in the unification test. These are called "super skolems". Example:
class Foo a where { op :: a -> Int }
instance Foo a => Foo [a] -- NB overlap
instance Foo [Int] -- NB overlap
data T = forall a. Foo a => MkT a
f :: T -> Int
f (MkT x) = op [x,x]
The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
complain, saying that the choice of instance depended on the instantiation
of 'a'; but of course it isn't *going* to be instantiated.
We do this only for isOverlappableTyVar skolems. For example we reject
The op [x,x] means we need (Foo [a]). This `a` will never be instantiated, and
so it is a super skolem. (See the use of tcInstSuperSkolTyVarsX in
GHC.Tc.Gen.Pat.tcDataConPat.) Super skolems respond True to
isOverlappableTyVar, and the use of Skolem in instanceBindFun, above, means
that these will be treated as fresh constants in the unification algorithm
during instance lookup. Without this treatment, GHC would complain, saying
that the choice of instance depended on the instantiation of 'a'; but of
course it isn't *going* to be instantiated. Note that it is necessary that
the unification algorithm returns SurelyApart for these super-skolems
for GHC to be able to commit to another instance.
We do this only for super skolems. For example we reject
g :: forall a => [a] -> Int
g x = op x
on the grounds that the correct instance depends on the instantiation of 'a'
......
......@@ -116,6 +116,7 @@ instance TrieMap CoreMap where
alterTM k f (CoreMap m) = CoreMap (alterTM (deBruijnize k) f m)
foldTM k (CoreMap m) = foldTM k m
mapTM f (CoreMap m) = CoreMap (mapTM f m)
filterTM f (CoreMap m) = CoreMap (filterTM f m)
-- | @CoreMapG a@ is a map from @DeBruijn CoreExpr@ to @a@. The extended
-- key makes it suitable for recursive traversal, since it can track binders,
......@@ -197,6 +198,7 @@ instance TrieMap CoreMapX where
alterTM = xtE
foldTM = fdE
mapTM = mapE
filterTM = ftE
--------------------------
mapE :: (a->b) -> CoreMapX a -> CoreMapX b
......@@ -213,6 +215,20 @@ mapE f (CM { cm_var = cvar, cm_lit = clit
, cm_letr = mapTM (mapTM (mapTM f)) cletr, cm_case = mapTM (mapTM f) ccase
, cm_ecase = mapTM (mapTM f) cecase, cm_tick = mapTM (mapTM f) ctick }
ftE :: (a->Bool) -> CoreMapX a -> CoreMapX a
ftE f (CM { cm_var = cvar, cm_lit = clit
, cm_co = cco, cm_type = ctype
, cm_cast = ccast , cm_app = capp
, cm_lam = clam, cm_letn = cletn
, cm_letr = cletr, cm_case = ccase
, cm_ecase = cecase, cm_tick = ctick })
= CM { cm_var = filterTM f cvar, cm_lit = filterTM f clit
, cm_co = filterTM f cco, cm_type = filterTM f ctype
, cm_cast = mapTM (filterTM f) ccast, cm_app = mapTM (filterTM f) capp
, cm_lam = mapTM (filterTM f) clam, cm_letn = mapTM (mapTM (filterTM f)) cletn
, cm_letr = mapTM (mapTM (filterTM f)) cletr, cm_case = mapTM (filterTM f) ccase
, cm_ecase = mapTM (filterTM f) cecase, cm_tick = mapTM (filterTM f) ctick }
--------------------------
lookupCoreMap :: CoreMap a -> CoreExpr -> Maybe a
lookupCoreMap cm e = lookupTM e cm
......@@ -330,6 +346,7 @@ instance TrieMap AltMap where
alterTM = xtA emptyCME
foldTM = fdA
mapTM = mapA
filterTM = ftA
instance Eq (DeBruijn CoreAlt) where
D env1 a1 == D env2 a2 = go a1 a2 where
......@@ -348,6 +365,12 @@ mapA f (AM { am_deflt = adeflt, am_data = adata, am_lit = alit })
, am_data = mapTM (mapTM f) adata
, am_lit = mapTM (mapTM f) alit }
ftA :: (a->Bool) -> AltMap a -> AltMap a
ftA f (AM { am_deflt = adeflt, am_data = adata, am_lit = alit })
= AM { am_deflt = filterTM f adeflt
, am_data = mapTM (filterTM f) adata
, am_lit = mapTM (filterTM f) alit }
lkA :: CmEnv -> CoreAlt -> AltMap a -> Maybe a
lkA env (DEFAULT, _, rhs) = am_deflt >.> lkG (D env rhs)
lkA env (LitAlt lit, _, rhs) = am_lit >.> lookupTM lit >=> lkG (D env rhs)
......
......@@ -8,6 +8,9 @@
{-# LANGUAGE TypeFamilies #-}
module GHC.Core.Map.Type (
-- * Re-export generic interface
TrieMap(..),
-- * Maps over 'Type's
TypeMap, emptyTypeMap, extendTypeMap, lookupTypeMap, foldTypeMap,
LooseTypeMap,
......@@ -45,6 +48,7 @@ import GHC.Types.Var.Env
import GHC.Types.Unique.FM
import GHC.Utils.Outputable
import GHC.Data.Maybe
import GHC.Utils.Panic
import qualified Data.Map as Map
......@@ -86,6 +90,7 @@ instance TrieMap CoercionMap where
alterTM k f (CoercionMap m) = CoercionMap (alterTM (deBruijnize k) f m)
foldTM k (CoercionMap m) = foldTM k m
mapTM f (CoercionMap m) = CoercionMap (mapTM f m)
filterTM f (CoercionMap m) = CoercionMap (filterTM f m)
type CoercionMapG = GenMap CoercionMapX
newtype CoercionMapX a = CoercionMapX (TypeMapX a)
......@@ -97,6 +102,7 @@ instance TrieMap CoercionMapX where
alterTM = xtC
foldTM f (CoercionMapX core_tm) = foldTM f core_tm
mapTM f (CoercionMapX core_tm) = CoercionMapX (mapTM f core_tm)
filterTM f (CoercionMapX core_tm) = CoercionMapX (filterTM f core_tm)
instance Eq (DeBruijn Coercion) where
D env1 co1 == D env2 co2
......@@ -135,6 +141,12 @@ data TypeMapX a
= TM { tm_var :: VarMap a
, tm_app :: TypeMapG (TypeMapG a)
, tm_tycon :: DNameEnv a
-- only InvisArg arrows here
, tm_funty :: TypeMapG (TypeMapG (TypeMapG a))
-- keyed on the argument, result rep, and result
-- constraints are never linear-restricted and are always lifted
, tm_forall :: TypeMapG (BndrMap a) -- See Note [Binders] in GHC.Core.Map.Expr
, tm_tylit :: TyLitMap a
, tm_coerce :: Maybe a
......@@ -142,10 +154,12 @@ data TypeMapX a
-- Note that there is no tyconapp case; see Note [Equality on AppTys] in GHC.Core.Type
-- | Squeeze out any synonyms, and change TyConApps to nested AppTys. Why the
-- last one? See Note [Equality on AppTys] in "GHC.Core.Type"
-- last one? See Note [Equality on AppTys] in GHC.Core.Type
--
-- Note, however, that we keep Constraint and Type apart here, despite the fact
-- that they are both synonyms of TYPE 'LiftedRep (see #11715).
--
-- We also keep (Eq a => a) as a FunTy, distinct from ((->) (Eq a) a).
trieMapView :: Type -> Maybe Type
trieMapView ty
-- First check for TyConApps that need to be expanded to
......@@ -164,6 +178,7 @@ instance TrieMap TypeMapX where
alterTM = xtT
foldTM = fdT
mapTM = mapT
filterTM = filterT
instance Eq (DeBruijn Type) where
env_t@(D env t) == env_t'@(D env' t')
......@@ -184,8 +199,11 @@ instance Eq (DeBruijn Type) where
-> D env t1 == D env' t1' && D env t2 == D env' t2'
(s, AppTy t1' t2') | Just (t1, t2) <- repSplitAppTy_maybe s
-> D env t1 == D env' t1' && D env t2 == D env' t2'
(FunTy _ w1 t1 t2, FunTy _ w1' t1' t2')
-> D env w1 == D env w1' && D env t1 == D env' t1' && D env t2 == D env' t2'
(FunTy v1 w1 t1 t2, FunTy v1' w1' t1' t2')
-> v1 == v1' &&
D env w1 == D env w1' &&
D env t1 == D env' t1' &&
D env t2 == D env' t2'
(TyConApp tc tys, TyConApp tc' tys')
-> tc == tc' && D env tys == D env' tys'
(LitTy l, LitTy l')
......@@ -205,17 +223,19 @@ emptyT :: TypeMapX a
emptyT = TM { tm_var = emptyTM
, tm_app = emptyTM
, tm_tycon = emptyDNameEnv
, tm_funty = emptyTM
, tm_forall = emptyTM
, tm_tylit = emptyTyLitMap
, tm_coerce = Nothing }
mapT :: (a->b) -> TypeMapX a -> TypeMapX b
mapT f (TM { tm_var = tvar, tm_app = tapp, tm_tycon = ttycon
, tm_forall = tforall, tm_tylit = tlit
, tm_funty = tfunty, tm_forall = tforall, tm_tylit = tlit
, tm_coerce = tcoerce })
= TM { tm_var = mapTM f tvar
, tm_app = mapTM (mapTM f) tapp
, tm_tycon = mapTM f ttycon
, tm_funty = mapTM (mapTM (mapTM f)) tfunty
, tm_forall = mapTM (mapTM f) tforall
, tm_tylit = mapTM f tlit
, tm_coerce = fmap f tcoerce }
......@@ -233,6 +253,11 @@ lkT (D env ty) m = go ty m
go (LitTy l) = tm_tylit >.> lkTyLit l
go (ForAllTy (Bndr tv _) ty) = tm_forall >.> lkG (D (extendCME env tv) ty)
>=> lkBndr env tv
go (FunTy InvisArg _ arg res)