[Git][ghc/ghc][wip/cfuneqcan-refactor] 2 commits: Address points from Hécate.
Richard Eisenberg
gitlab at gitlab.haskell.org
Wed Nov 11 23:09:12 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
b90a27ce by Richard Eisenberg at 2020-11-11T13:00:33-05:00
Address points from Hécate.
- - - - -
78425e2e by Richard Eisenberg at 2020-11-11T18:01:57-05:00
Reviews on GitLab
- - - - -
14 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Flatten.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -2659,7 +2659,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
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -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]
~~~~~~~~~~~~~~~~~~~~
@@ -1176,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.
@@ -1193,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
=====================================
compiler/GHC/Core/InstEnv.hs
=====================================
@@ -840,6 +840,8 @@ lookupInstEnv' ie vis_mods cls tys
flattened_tys = flattenTys in_scope tys in
-- NB: important to flatten here. Otherwise, it looks like
-- instance C Int cannot match a target [W] C (F Bool).
+ -- See Note [Flattening type-family applications when matching instances]
+ -- in GHC.Core.Unify.
case tcUnifyTysFG instanceBindFun tpl_tys flattened_tys of
SurelyApart -> find ms us rest
_ -> find ms (item:us) rest
@@ -1029,20 +1031,26 @@ 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.
+
+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'
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -821,8 +821,11 @@ data TyCon
-- any type synonym families (data families
-- are fine), again after expanding any
-- nested synonyms
- synIsForgetful :: Bool -- True <=> at least one argument is not mentioned
- -- in the RHS
+ synIsForgetful :: Bool -- True <= at least one argument is not mentioned
+ -- in the RHS (or is mentioned only under
+ -- forgetful synonyms)
+ -- Test is conservative, so True does not guarantee
+ -- forgetfulness.
}
-- | Represents families (both type and data)
@@ -2056,7 +2059,11 @@ isFamFreeTyCon (SynonymTyCon { synIsFamFree = fam_free }) = fam_free
isFamFreeTyCon (FamilyTyCon { famTcFlav = flav }) = isDataFamFlav flav
isFamFreeTyCon _ = True
--- | Is this a forgetful type synonym?
+-- | Is this a forgetful type synonym? If this is a type synonym whose
+-- RHS does not mention one (or more) of its bound variables, returns
+-- True. Thus, False means that all bound variables appear on the RHS;
+-- True may not mean anything, as the test to set this flag is
+-- conservative.
isForgetfulSynTyCon :: TyCon -> Bool
isForgetfulSynTyCon (SynonymTyCon { synIsForgetful = forget }) = forget
isForgetfulSynTyCon _ = False
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -719,8 +719,9 @@ 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.FamInstEnv (See Note [Flattening] in GHC.Core.Unify), not
-the flattening algorithm in the solver.
+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.
Notation:
θ,φ substitutions
@@ -1648,8 +1649,8 @@ pushRefl co =
* *
************************************************************************
-Note [Flattening]
-~~~~~~~~~~~~~~~~~
+Note [Flattening type-family applications when matching instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As described in "Closed type families with overlapping equations"
http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
we need to flatten core types before unifying them, when checking for "surely-apart"
@@ -1678,6 +1679,15 @@ can see that (F x x) can reduce to Double. So, it had better be the
case that (F blah blah) can reduce to Double, no matter what (blah)
is! Flattening as done below ensures this.
+We also use this flattening operation to check for class instances.
+If we have
+ instance C (Maybe b)
+ instance {-# OVERLAPPING #-} C (Maybe Bool)
+ [W] C (Maybe (F a))
+we want to know that the second instance might match later. So we
+flatten the (F a) in the target before trying to unify with instances.
+(This is done in GHC.Core.InstEnv.lookupInstEnv'.)
+
The algorithm works by building up a TypeMap TyVar, mapping
type family applications to fresh variables. This mapping must
be threaded through all the function calls, as any entry in
@@ -1794,7 +1804,7 @@ data FlattenEnv
-- domain: exactly-saturated type family applications
-- range: (fresh variable, type family tycon, args)
, fe_in_scope :: InScopeSet }
- -- See Note [Flattening]
+ -- See Note [Flattening type-family applications when matching instances]
emptyFlattenEnv :: InScopeSet -> FlattenEnv
emptyFlattenEnv in_scope
@@ -1805,11 +1815,11 @@ updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet env upd = env { fe_in_scope = upd (fe_in_scope env) }
flattenTys :: InScopeSet -> [Type] -> [Type]
--- See Note [Flattening]
+-- See Note [Flattening type-family applications when matching instances]
flattenTys in_scope tys = fst (flattenTysX in_scope tys)
flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
--- See Note [Flattening]
+-- See Note [Flattening type-family applications when matching instances]
-- NB: the returned types mention the fresh type variables
-- in the domain of the returned env, whose range includes
-- the original type family applications. Building a substitution
@@ -1889,7 +1899,7 @@ coreFlattenCo subst env co
(env1, kind') = coreFlattenTy subst env (coercionType co)
covar = mkFlattenFreshCoVar (fe_in_scope env1) kind'
-- Add the covar to the FlattenEnv's in-scope set.
- -- See Note [Flattening], wrinkle 2A.
+ -- See Note [Flattening type-family applications when matching instances], wrinkle 2A.
env2 = updateInScopeSet env1 (flip extendInScopeSet covar)
coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
@@ -1897,7 +1907,7 @@ coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
coreFlattenVarBndr subst env tv
= (env2, subst', tv')
where
- -- See Note [Flattening], wrinkle 2B.
+ -- See Note [Flattening type-family applications when matching instances], wrinkle 2B.
kind = varType tv
(env1, kind') = coreFlattenTy subst env kind
tv' = uniqAway (fe_in_scope env1) (setVarType tv kind')
@@ -1927,11 +1937,13 @@ coreFlattenTyFamApp tv_subst env fam_tc fam_args
(sat_fam_args, leftover_args) = ASSERT( arity <= length fam_args )
splitAt arity fam_args
-- Apply the substitution before looking up an application in the
- -- environment. See Note [Flattening], wrinkle 1.
+ -- environment. See Note [Flattening type-family applications when matching instances],
+ -- wrinkle 1.
-- NB: substTys short-cuts the common case when the substitution is empty.
sat_fam_args' = substTys tcv_subst sat_fam_args
(env', leftover_args') = coreFlattenTys tv_subst env leftover_args
- -- `fam_tc` may be over-applied to `fam_args` (see Note [Flattening],
+ -- `fam_tc` may be over-applied to `fam_args` (see
+ -- Note [Flattening type-family applications when matching instances]
-- wrinkle 3), so we split it into the arguments needed to saturate it
-- (sat_fam_args') and the rest (leftover_args')
fam_ty = mkTyConApp fam_tc sat_fam_args'
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1189,6 +1189,11 @@ tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
= do { checkWiredInTyCon typeSymbolKindCon
; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
+--------- Wildcards
+
+tc_hs_type mode ty@(HsWildCardTy _) ek
+ = tcAnonWildCardOcc NoExtraConstraint mode ty ek
+
--------- Potentially kind-polymorphic types: call the "up" checker
-- See Note [Future-proofing the type checker]
tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
@@ -1198,9 +1203,6 @@ tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsWildCardTy _) ek
- = tcAnonWildCardOcc NoExtraConstraint mode ty ek
-
{-
Note [Variable Specificity and Forall Visibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -898,6 +898,8 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv ex_tvs
-- Get location from monad, not from ex_tvs
-- This freshens: See Note [Freshen existentials]
+ -- Why "super"? See Note [Binding when lookup up instances]
+ -- in GHC.Core.InstEnv.
; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
-- pat_ty' is type of the actual constructor application
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1019,29 +1019,21 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
-- 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
- (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
- | Just ty1a_rep <- getRuntimeRep_maybe ty1a -- getRutimeRep_maybe:
+ (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)
+ , Just ty1a_rep <- getRuntimeRep_maybe ty1a -- getRutimeRep_maybe:
, Just ty1b_rep <- getRuntimeRep_maybe ty1b -- see Note [Decomposing FunTy]
, Just ty2a_rep <- getRuntimeRep_maybe ty2a
, Just ty2b_rep <- getRuntimeRep_maybe ty2b
- = if af1 == af2 -- Don't decompose (Int -> blah) ~ (Show a => blah)
- then canDecomposableTyConAppOK ev eq_rel funTyCon
+ = canDecomposableTyConAppOK ev eq_rel funTyCon
[am1, ty1a_rep, ty1b_rep, ty1a, ty1b]
[am2, ty2a_rep, ty2b_rep, ty2a, ty2b]
- else canEqHardFailure ev ps_ty1 ps_ty2
- -- in the "else" case, we don't want to fall through, because the TyConApp
- -- case may trigger, giving a worse error
-- Decompose type constructor applications
-- NB: we have expanded type synonyms already
--- We still have to handle the FunTy case separately, just to avoid decomposing
--- (Int -> blah) and (Show a => blah).
-can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
- -- use tcSplit to avoid splitting (Eq a => Bool)
- | Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
- , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
- , not (isTypeFamilyTyCon tc1)
+can_eq_nc' _flat _rdr_env _envs ev eq_rel (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
+ | not (isTypeFamilyTyCon tc1)
, not (isTypeFamilyTyCon tc2)
= canTyConApp ev eq_rel tc1 tys1 tc2 tys2
@@ -2040,7 +2032,7 @@ See also #10715, which induced this addition.
Note [Put touchable variables on the left]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-#10009, a very nasty example:
+Ticket #10009, a very nasty example:
f :: (UnF (F b) ~ b) => F b -> ()
@@ -2085,7 +2077,7 @@ in a Given. On the other hand, the original LHS mentioned only variables
that appear in Givens. We thus choose to put variables that can appear
in Wanteds on the left.
-#12526 is another good example of this in action.
+Ticket #12526 is another good example of this in action.
-}
@@ -2476,18 +2468,18 @@ canEqOK dflags eq_rel lhs rhs
-- are not generally insoluble
where
- good_rhs = kinds_match && not bad_newtype
+ good_rhs = kinds_match && not bad_newtype
- lhs_kind = canEqLHSKind lhs
- rhs_kind = tcTypeKind rhs
+ lhs_kind = canEqLHSKind lhs
+ rhs_kind = tcTypeKind rhs
- kinds_match = lhs_kind `tcEqType` rhs_kind
+ kinds_match = lhs_kind `tcEqType` rhs_kind
- bad_newtype | ReprEq <- eq_rel
- , Just tc <- tyConAppTyCon_maybe rhs
- = isNewTyCon tc
- | otherwise
- = False
+ bad_newtype | ReprEq <- eq_rel
+ , Just tc <- tyConAppTyCon_maybe rhs
+ = isNewTyCon tc
+ | otherwise
+ = False
{- Note [Equalities with incompatible kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2530,17 +2522,18 @@ Wrinkles:
tales of destruction.
So, we have an invariant on CEqCan (TyEq:H) that the RHS does not have
- any coercion holes. This is checked in metaTyVarUpdateOK. We also
+ any coercion holes. This is checked in checkTypeEq. Any equalities that
+ have such an RHS are turned in CIrredCans with a BlockedCIS status. We also
must be sure to kick out any constraints that mention coercion holes
- when those holes get filled in.
+ when those holes get filled in, so that the unification step can now proceed.
(2a) We must now absolutely make sure to kick out any constraints that
- mention a newly-filled-in coercion hole. This is done in
- kickOutAfterFillingCoercionHole. But we only kick out when the
- filling coercion contains no coercion holes. This extra check
- avoids needless work when rewriting evidence (which fills coercion
- holes) and aids efficiency. It also can avoid a loop in the solver
- that would otherwise arise in this case:
+ mention a newly-filled-in coercion hole -- 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. It also can avoid
+ a loop in the solver that would otherwise arise in this case:
[W] w1 :: (ty1 :: F a) ~ (ty2 :: s)
After canonicalisation, we discover that this equality is heterogeneous.
So we emit
@@ -2551,11 +2544,14 @@ Wrinkles:
and forth, as it goes through canEqTyVarFunEq. We thus get
co_abc := sym co_abd, and then co_abd := sym co_abe, with
[W] co_abe :: F a ~ s
- right back where we started. But all this filling in would,
- naively, cause kicking w2 out. Which, when it got processed,
+ right back where we started. (At this point, we're in canEqCanLHSFinish,
+ so we're not looping.) But all this filling in would,
+ naively, cause w2 to be kicked out. Which, when it got 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.
(2b) Consider this case:
[G] co_given :: k1 ~ k2
@@ -2592,8 +2588,8 @@ Wrinkles:
cast appears opposite a tyvar. This is implemented in the cast case
of can_eq_nc'.
- (4) Reporting an error for a constraint that is blocked only because
- of wrinkle (2) is hard: what would we say to users? And we don't
+ (4) Reporting an error for a constraint that is blocked with status BlockedCIS
+ is hard: what would we say to users? And we don't
really need to report, because if a constraint is blocked, then
there is unsolved wanted blocking it; that unsolved wanted will
be reported. We thus push such errors to the bottom of the queue
@@ -2671,7 +2667,25 @@ In order to solve the Wanted, we must use the Given to rewrite `a` to
Maybe (F a). But note that the Given has an occurs-check failure, and
so we can't straightforwardly add the Given to the inert set.
-Instead, we detect this scenario by the following characteristics:
+The key idea is to replace the (F a) in the RHS of the Given with a
+fresh variable, which we'll call a CycleBreakerTv, or cbv. Then, emit
+a new Given to connect cbv with F a. So our situation becomes
+
+ instance C (Maybe b)
+ [G] a ~ Maybe cbv
+ [G] F a ~ cbv
+ [W] C a
+
+Note the orientation of the second Given. The type family ends up
+on the left; see commentary on canEqTyVarFunEq, which decides how to
+orient such cases. No special treatment for CycleBreakerTvs is
+necessary. This scenario is now easily soluble, by using the first
+Given to rewrite the Wanted, which can now be solved.
+
+(The first Given actually also rewrites the second one. This causes
+no trouble.)
+
+More generally, we detect this scenario by the following characteristics:
- a Given CEqCan constraint
- with a tyvar on its LHS
- with a soluble occurs-check failure
@@ -2689,16 +2703,24 @@ after we're done running the solver (in nestImplicTcS and runTcSWithEvBinds).
This is done by restoreTyVarCycles, which uses the inert_cycle_breakers field in
InertSet, which contains the pairings invented in breakTyVarCycle.
-In our example, we start with
-
- [G] a ~ Maybe (F a)
-
-We then change this to become
-
- [G] a ~ Maybe cbv
- [G] F a ~ cbv
-
-and set cbv := F a after we're done solving.
+That is:
+
+We transform
+ [G] g : a ~ ...(F a)...
+to
+ [G] (Refl a) : F a ~ cbv -- CEqCan
+ [G] g : a ~ ...cbv... -- CEqCan
+
+Note that
+* `cbv` is a fresh cycle breaker variable.
+* `cbv` is a is a meta-tyvar, but it is completely untouchable.
+* We track the cycle-breaker variables in inert_cycle_breakers in InertSet
+* We eventually fill in the cycle-breakers, with `cbv := F a`.
+ No one else fills in cycle-breakers!
+* This fill-in is done when solving is complete, by restoreTyVarCycles
+ in nestImplicTcS and runTcSWithEvBinds.
+* The evidence for the new `F a ~ cbv` constraint is Refl, because we know this fill-in is
+ ultimately going to happen.
There are drawbacks of this approach:
@@ -2749,14 +2771,26 @@ Details:
The temporary ill-kinded type hurts no one, and avoiding this would
be quite painfully difficult.
+ Specifically, this detail does not contravene the Purely Kinded Type Invariant
+ (Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType).
+ The PKTI says that we can call typeKind on any type, without failure.
+ It would be violated if we, say, replaced a kind (a -> b) with a kind c,
+ because an arrow kind might be consulted in piResultTys. Here, we are
+ replacing one opaque type like (F a b c) with another, cbv (opaque in
+ that we never assume anything about its structure, like that it has a
+ result type or a RuntimeRep argument).
+
(4) The evidence for the produced Givens is all just reflexive, because
we will eventually set the cycle-breaker variable to be the type family,
and then, after the zonk, all will be well.
(5) The approach here is inefficient. For instance, we could choose to
- affect only type family applications that mention the offending variable.
- We could try to detect cases like a ~ (F a, F a) and use the same
- tyvar to replace F a. (Cf. Note [Flattening] in GHC.Core.Unify, which
+ affect only type family applications that mention the offending variable:
+ in a ~ (F b, G a), we need to replace only G a, not F b. Furthermore,
+ we could try to detect cases like a ~ (F a, F a) and use the same
+ tyvar to replace F a. (Cf.
+ Note [Flattening type-family applications when matching instances]
+ in GHC.Core.Unify, which
goes to this extra effort.) There may be other opportunities for
improvement. However, this is really a very small corner case, always
tickled by a user-written Given. The investment to craft a clever,
@@ -2768,7 +2802,9 @@ Details:
evidence itself. As in Detail (4), we don't need to change the
evidence term (as in e.g. rewriteEqEvidence) because the cycle
breaker variables are all zonked away by the time we examine the
- evidence.
+ evidence. That is, we must set the ctev_pred of the ctEvidence.
+ This is implemented in canEqCanLHSFinish, with a reference to
+ this detail.
(7) We don't wish to apply this magic to CycleBreakerTvs themselves.
Consider this, from typecheck/should_compile/ContextStack2:
@@ -2801,7 +2837,11 @@ Details:
unchecked, this will end up breaking cycles again, looping ad
infinitum (and resulting in a context-stack reduction error,
not an outright loop). The solution is easy: don't break cycles
- if the var is already a CycleBreakerTv. This makes sense, because
+ if the var is already a CycleBreakerTv. Instead, we mark this
+ final Given as a CIrredCan with an OtherCIS status (it's not
+ insoluble).
+
+ 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.
=====================================
compiler/GHC/Tc/Solver/Flatten.hs
=====================================
@@ -362,7 +362,7 @@ 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
faster. This doesn't seem quite worth it, yet.
-Note [flatten_exact_fam_app_fully performance]
+Note [flatten_exact_fam_app performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Once we've got a flat rhs, we extend the famapp-cache to record
the result. Doing so can save lots of work when the same redex shows up more
@@ -727,15 +727,22 @@ keeps types smaller. But we need to take care.
Suppose
type Syn a = Int
type instance F Bool = Syn (F Bool)
+ [G] F Bool ~ Syn (F Bool)
-If we don't expand the synonym, we'll fall into an unnecessary loop.
+If we don't expand the synonym, we'll get a spurious occurs-check
+failure. This is normally what occCheckExpand takes care of, but
+the LHS is a type family application, and occCheckExpand (already
+complex enough as it is) does not know how to expand to avoid
+a type family application.
In addition, expanding the forgetful synonym like this
-will generally yield a *smaller* type. We thus expand forgetful
+will generally yield a *smaller* type. To wit, if we spot
+S ( ... F tys ... ), where S is forgetful, we don't want to bother
+doing hard work simplifying (F tys). We thus expand forgetful
synonyms, but not others.
-One nice consequence is that we never have to occCheckExpand flattened
-types, as any forgetful synonyms are already expanded.
+isForgetfulSynTyCon returns True more often than it needs to, so
+we err on the side of more expansion.
We also, of course, must expand type synonyms that mention type families,
so those families can get reduced.
@@ -745,11 +752,63 @@ so those families can get reduced.
Flattening a type-family application
* *
************************************************************************
+
+Note [How to normalise a family application]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given an exactly saturated family application, how should we normalise it?
+This Note spells out the algorithm and its reasoning.
+
+STEP 1. Try the famapp-cache. If we get a cache hit, jump to FINISH.
+
+STEP 2. Try top-level instances. Note that we haven't simplified the arguments
+ yet. Example:
+ type instance F (Maybe a) = Int
+ target: F (Maybe (G Bool))
+ Instead of first trying to simplify (G Bool), we use the instance first. This
+ avoids the work of simplifying G Bool.
+
+ If an instance is found, jump to FINISH.
+
+STEP 3. Flatten 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.
+
+ If an inert is found, jump to FINISH.
+
+STEP 5. Try the famapp-cache again. Now that we've revealed more information
+ in the arguments, the cache might be helpful.
+
+ If we get a cache hit, jump to FINISH.
+
+STEP 6. Try top-level instances, which might trigger now that we know more
+ about the argumnents.
+
+ If an instance is found, jump to FINISH.
+
+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.
+
+FINISH 2. Add the result to the famapp-cache, connecting the type we started
+ with to the one we ended with.
+
+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]
+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_fully lifts out the application to top level
+ -- flatten_exact_fam_app lifts out the application to top level
-- Postcondition: Coercion :: Xi ~ F tys
flatten_fam_app tc tys -- Can be over-saturated
= ASSERT2( tys `lengthAtLeast` tyConArity tc
@@ -760,26 +819,27 @@ 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_fully tc tys1
+ ; (xi1, co1) <- flatten_exact_fam_app tc tys1
-- co1 :: xi1 ~ F tys1
; flatten_app_ty_args xi1 co1 tys_rest }
-- the [TcType] exactly saturate the TyCon
-flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
-flatten_exact_fam_app_fully tc tys
+-- See Note [How to normalise a family application]
+flatten_exact_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
+flatten_exact_fam_app tc tys
= do { checkStackDepth (mkTyConApp tc tys)
- -- Step 1. Try to reduce without reducing arguments first.
+ -- STEP 1/2. Try to reduce without reducing arguments first.
; result1 <- try_to_reduce tc tys
; case result1 of
-- Don't use `finish`;
- -- See Note [flatten_exact_fam_app_fully performance]
+ -- See Note [flatten_exact_fam_app performance]
{ Just (co, xi) -> do { (xi2, co2) <- bumpDepth $ flatten_one xi
; return (xi2, co2 `mkTcTransCo` co) }
; Nothing ->
- -- That didn't work. So reduce the arguments.
+ -- That didn't work. So reduce the arguments, in STEP 3.
do { (xis, cos, kind_co) <- flatten_args_tc tc (repeat Nominal) tys
-- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys)
@@ -795,6 +855,7 @@ flatten_exact_fam_app_fully tc tys
-- and co' :: xi' ~r F tys, which is homogeneous
homogenise xi co = homogenise_result xi (co `mkTcTransCo` args_co) role kind_co
+ -- STEP 4: try the inerts
; result2 <- liftTcS $ lookupFamAppInert tc xis
; flavour <- getFlavour
; case result2 of
@@ -813,11 +874,11 @@ flatten_exact_fam_app_fully tc tys
; _ ->
- -- inert didn't work. Try to reduce again
+ -- inert didn't work. Try to reduce again, in STEP 5/6.
do { result3 <- try_to_reduce tc xis
; case result3 of
Just (co, xi) -> finish (homogenise xi co)
- Nothing -> -- we have made no progress at all
+ Nothing -> -- we have made no progress at all: STEP 7.
return (homogenise reduced (mkTcReflCo role reduced))
where
reduced = mkTyConApp tc xis }}}}}
@@ -825,10 +886,13 @@ flatten_exact_fam_app_fully tc tys
-- call this if the above attempts made progress.
-- This recursively flattens the result and then adds to the cache
finish :: (Xi, Coercion) -> FlatM (Xi, Coercion)
- finish (xi, co) = do { (fully, fully_co) <- bumpDepth $ flatten_one xi
+ finish (xi, co) = do { -- flatten the result: FINISH 1
+ (fully, fully_co) <- bumpDepth $ flatten_one xi
; let final_co = fully_co `mkTcTransCo` co
; eq_rel <- getEqRel
; flavour <- getFlavour
+
+ -- extend the cache: FINISH 2
; when (eq_rel == NomEq && flavour /= Derived) $
-- the cache only wants Nominal eqs
-- and Wanteds can rewrite Deriveds; the cache
@@ -837,12 +901,15 @@ flatten_exact_fam_app_fully tc tys
; return (fully, final_co) }
-- Returned coercion is output ~r input, where r is the role in the FlatM monad
+-- See Note [How to normalise a family application]
try_to_reduce :: TyCon -> [TcType] -> FlatM (Maybe (TcCoercion, TcType))
try_to_reduce tc tys
- = do { result <- liftTcS $ firstJustsM [ lookupFamAppCache tc tys
- , matchFam tc tys ]
+ = do { result <- liftTcS $ firstJustsM [ lookupFamAppCache tc tys -- STEP 5
+ , matchFam tc tys ] -- STEP 6
; downgrade result }
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 Nothing = return Nothing
downgrade result@(Just (co, xi))
@@ -991,8 +1058,6 @@ split_pi_tys' ty = split ty ty
split orig_ty _ = ([], orig_ty, False)
{-# INLINE split_pi_tys' #-}
-
-
-- | Like 'tyConBindersTyCoBinders' but you also get a 'Bool' which is true iff
-- there is at least one named binder.
ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -2096,7 +2096,7 @@ The partial solution is that:
The end effect is that, much as we do for overlapping instances, we
delay choosing a class instance if there is a possibility of another
instance OR a given to match our constraint later on. This fixes
-#4981 and #5002.
+tickets #4981 and #5002.
Other notes:
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -802,6 +802,7 @@ Proof. By property (R2), with f1=f2
Definition [Generalised substitution]
A "generalised substitution" S is a set of triples (t0 -f-> t), where
t0 is a type variable or an exactly-saturated type family application
+ (that is, t0 is a CanEqLHS)
t is a type
f is a flavour
such that
@@ -876,7 +877,7 @@ Main Theorem [Stability under extension]
AND (K3) See Note [K3: completeness of solving]
{ (K3a) If the role of fs is nominal: s /= t0
(K3b) If the role of fs is representational:
- s is not of form (a t1 .. tn) } }
+ s is not of form (t0 t1 .. tn) } }
Conditions (T1-T3) are established by the canonicaliser
@@ -1149,6 +1150,9 @@ Additional notes:
* inert_dicts is a finite map keyed by
the type; it's inconvenient for it to map to TWO constraints
+Another example requiring Deriveds is in
+Note [Put touchable variables on the left] in GHC.Tc.Solver.Canonical.
+
Note [Splitting WD constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We are about to add a [WD] constraint to the inert set; and we
@@ -1774,7 +1778,7 @@ kick_out_rewritable new_fr new_lhs
&& fr_can_rewrite_ty eq_rel rhs_ty -- (K2d)
-- (K2c) is guaranteed by the first guard of keep_eq
- kick_out_for_completeness
+ kick_out_for_completeness -- (K3) and Note [K3: completeness of solving]
= case (eq_rel, new_lhs) of
(NomEq, _) -> rhs_ty `eqType` canEqLHSType new_lhs
(ReprEq, TyVarLHS new_tv) -> isTyVarHead new_tv rhs_ty
@@ -1815,6 +1819,8 @@ kickOutAfterFillingCoercionHole hole filled_co
; setInertCans ics' }
where
+ holes_of_co = coercionHolesOfCo filled_co
+
kick_out :: InertCans -> (WorkList, InertCans)
kick_out ics@(IC { inert_irreds = irreds })
= let (to_kick, to_keep) = partitionBagWith kick_ct irreds
@@ -1830,7 +1836,7 @@ kickOutAfterFillingCoercionHole hole filled_co
kick_ct ct@(CIrredCan { cc_status = BlockedCIS holes })
| hole `elementOfUniqSet` holes
= let new_holes = holes `delOneFromUniqSet` hole
- `unionUniqSets` coercionHolesOfCo filled_co
+ `unionUniqSets` holes_of_co
updated_ct = ct { cc_status = BlockedCIS new_holes }
in
if isEmptyUniqSet new_holes
@@ -2238,14 +2244,15 @@ We must determine whether a Given might later match a Wanted. We
definitely need to account for the possibility that any metavariable
in the Wanted might be arbitrarily instantiated. We do *not* want
to allow skolems in the Given to be instantiated. But what about
-type family applications?
+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] in GHC.Core.Unify.
+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 domian of a unifying substitution?
+variables in the domain of a unifying substitution?
A type family application that mentions only skolems is settled: any
skolems would have been rewritten w.r.t. Givens by now. These type
@@ -2256,6 +2263,30 @@ we use BindMe to tell the unifier to allow it in the substitution.
On the other hand, a type family application with only skolems is
considered rigid.
+Examples:
+ [G] C a
+ [W] C alpha
+ This easily might match later.
+
+ [G] C a
+ [W] C (F alpha)
+ This might match later, too, but we need to flatten the (F alpha)
+ to a fresh variable so that the unifier can connect the two.
+
+ [G] C (F alpha)
+ [W] C a
+ This also might match later. Again, we will need to flatten to
+ find this out. (Surprised about a metavariable in a Given? See
+ #18929.)
+
+ [G] C (F a)
+ [W] C a
+ This won't match later. We're not going to get new Givens that
+ can inform the F a, and so this is a no-go.
+
+This treatment fixes #18910 and is tested in
+typecheck/should_compile/InstanceGivenOverlap{,2}
+
Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider an implication
@@ -3599,7 +3630,7 @@ breakTyVarCycle loc = go
go ty@(Rep.ForAllTy {}) = return ty -- See Detail (1) of Note
go ty@(Rep.CoercionTy {}) = return ty -- See Detail (2) of Note
--- | Filli in CycleBreakerTvs with the variables they stand for.
+-- | Fill in CycleBreakerTvs with the variables they stand for.
-- See Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical.
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles is
@@ -3609,6 +3640,7 @@ 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 _)
| isForgetfulSynTyCon tc || (isTypeSynonymTyCon tc && not (isFamFreeTyCon tc))
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -113,6 +113,36 @@ import qualified Data.Semigroup ( (<>) )
* These are the constraints the low-level simplifier works with *
* *
************************************************************************
+
+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
+were to mention the LHS: this would cause a loop in rewriting.
+
+We thus perform an occurs-check. There is, of course, some subtlety:
+
+* For type variables, the occurs-check looks deeply. This is because
+ a CEqCan over a meta-variable is also used to inform unification,
+ in GHC.Tc.Solver.Interact.solveByUnification. If the LHS appears
+ anywhere, at all, in the RHS, unification will create an infinite
+ structure, which is bad.
+
+* For type family applications, the occurs-check is shallow; it looks
+ only in places where we might rewrite. (Specifically, it does not
+ look in kinds or coercions.) An occurrence of the LHS in, say, an
+ RHS coercion is OK, as we do not rewrite in coercions. No loop to
+ be found.
+
+ You might also worry about the possibility that a type family
+ application LHS doesn't exactly appear in the RHS, but something
+ that reduces to the LHS does. Yet that can't happen: the RHS is
+ already inert, with all type family redexes reduced. So a simple
+ syntactic check is just fine.
+
+The occurs check is performed in GHC.Tc.Utils.Unify.checkTypeEq.
+
-}
-- | A 'Xi'-type is one that has been fully rewritten with respect
@@ -157,8 +187,7 @@ data Ct
-- * See Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.Monad
-- * Many are checked in checkTypeEq in GHC.Tc.Utils.Unify
-- * (TyEq:OC) lhs does not occur in rhs (occurs check)
- -- (skips coercions if the lhs is a type family application, because
- -- we don't rewrite type families in coercions)
+ -- Note [CEqCan occurs check]
-- * (TyEq:F) rhs has no foralls
-- (this avoids substituting a forall for the tyvar in other types)
-- * (TyEq:K) tcTypeKind lhs `tcEqKind` tcTypeKind rhs; Note [Ct kind invariant]
@@ -243,6 +272,8 @@ data HoleSort = ExprHole Id
-- ^ A hole in a type (PartialTypeSignatures)
| ConstraintHole
-- ^ A hole in a constraint, like @f :: (_, Eq a) => ...
+ -- Differentiated from TypeHole because a ConstraintHole
+ -- is simplified differently. See GHC.Tc.Solver.simplifyHoles.
instance Outputable Hole where
ppr (Hole { hole_sort = ExprHole id
@@ -1141,8 +1172,9 @@ data ImplicStatus
| IC_Unsolved -- Neither of the above; might go either way
-- | Does this implication have Given equalities?
--- See Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad
--- and Note [Suppress redundant givens during error reporting] in GHC.Tc.Errors
+-- See Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad,
+-- which also explains why we need three options here. Also, see
+-- Note [Suppress redundant givens during error reporting] in GHC.Tc.Errors
data HasGivenEqs
= NoGivenEqs -- definitely no given equalities
| LocalGivenEqs -- might have Given equalities that affect only local skolems
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -2169,7 +2169,8 @@ Why?, for example:
- For CIrredCan we want to see if a constraint is insoluble with insolubleWC
On the other hand, we change CEqCan to CNonCanonical, because of all of
-CEqCan's invariants, which can break during zonking. Besides, the constraint
+CEqCan's invariants, which can break during zonking. (Example: a ~R alpha, where
+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.
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1976,7 +1976,8 @@ checkTyFamEq dflags fun_tc fun_args ty
= inline checkTypeEq dflags YesTypeFamilies (TyFamLHS fun_tc fun_args) ty
-- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
-checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType -> MetaTyVarUpdateResult ()
+checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType
+ -> MetaTyVarUpdateResult ()
-- Checks the invariants for CEqCan. In particular:
-- (a) a forall type (forall a. blah)
-- (b) a predicate type (c => ty)
@@ -1987,13 +1988,7 @@ checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType -> MetaTyVarU
-- For (a), (b), and (c) we check only the top level of the type, NOT
-- inside the kinds of variables it mentions. For (d) we look deeply
-- in coercions when the LHS is a tyvar (but skip coercions for type family
--- LHSs), and for (e) we do look in the kinds of course.
---
--- Why skip coercions for type families? Because we don't rewrite type family
--- applications in coercions, so there's no point in looking there. On the
--- other hand, we must check for type variables, lest we mutably create an
--- infinite structure during unification.
-
+-- LHSs), and for (e) see Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
checkTypeEq dflags ty_fam_ok lhs ty
= go ty
where
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ef7479323a85c965b50fb2dfd71f537872cedab1...78425e2e6d50575111568a2e6f9d8e7f7e8bae22
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ef7479323a85c965b50fb2dfd71f537872cedab1...78425e2e6d50575111568a2e6f9d8e7f7e8bae22
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201111/260c95d6/attachment-0001.html>
More information about the ghc-commits
mailing list