Commit 1cd3fa29 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Implement a coverage checker for injectivity

This fixes #16512.

There are lots of parts of this patch:

* The main payload is in FamInst. See
Note [Coverage condition for injective type families] there
for the overview. But it doesn't fix the bug.

* We now bump the reduction depth every time we discharge
a CFunEqCan. See Note [Flatten when discharging CFunEqCan]
in TcInteract.

* Exploration of this revealed a new, easy to maintain invariant
for CTyEqCans. See Note [Almost function-free] in TcRnTypes.

* We also realized that type inference for injectivity was a
bit incomplete. This means we exchanged lookupFlattenTyVar for
rewriteTyVar. See Note [rewriteTyVar] in TcFlatten. The new
function is monadic while the previous one was pure, necessitating
some faff in TcInteract. Nothing too bad.

* zonkCt did not maintain invariants on CTyEqCan. It's not worth
the bother doing so, so we just transmute CTyEqCans to
CNonCanonicals.

* The pure unifier was finding the fixpoint of the returned
substitution, even when doing one-way matching (in tcUnifyTysWithTFs).
Fixed now.

Test cases: typecheck/should_fail/T16512{a,b}
parent faa30dcb
......@@ -160,16 +160,14 @@ data Ct
| CTyEqCan { -- tv ~ rhs
-- Invariants:
-- * See Note [Applying the inert substitution] in TcFlatten
-- * See Note [inert_eqs: the inert equalities] in TcSMonad
-- * tv not in tvs(rhs) (occurs check)
-- * If tv is a TauTv, then rhs has no foralls
-- (this avoids substituting a forall for the tyvar in other types)
-- * tcTypeKind ty `tcEqKind` tcTypeKind tv; Note [Ct kind invariant]
-- * rhs may have at most one top-level cast
-- * rhs (perhaps under the one cast) is not necessarily function-free,
-- but it has no top-level function.
-- E.g. a ~ [F b] is fine
-- but a ~ F b is not
-- * rhs (perhaps under the one cast) is *almost function-free*,
-- See Note [Almost function-free]
-- * If the equality is representational, rhs has no top-level newtype
-- See Note [No top-level newtypes on RHS of representational
-- equalities] in TcCanonical
......@@ -289,6 +287,55 @@ of the rhs. This is necessary because both constraints are used for substitution
during solving. If the kinds differed, then the substitution would take a well-kinded
type to an ill-kinded one.
Note [Almost function-free]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
A type is *almost function-free* if it has no type functions (something that
responds True to isTypeFamilyTyCon), except (possibly)
* under a forall, or
* in a coercion (either in a CastTy or a CercionTy)
The RHS of a CTyEqCan must be almost function-free. This is for two reasons:
1. There cannot be a top-level function. If there were, the equality should
really be a CFunEqCan, not a CTyEqCan.
2. Nested functions aren't too bad, on the other hand. However, consider this
scenario:
type family F a = r | r -> a
[D] F ty1 ~ fsk1
[D] F ty2 ~ fsk2
[D] fsk1 ~ [G Int]
[D] fsk2 ~ [G Bool]
type instance G Int = Char
type instance G Bool = Char
If it was the case that fsk1 = fsk2, then we could unifty ty1 and ty2 --
good! They don't look equal -- but if we aggressively reduce that G Int and
G Bool they would become equal. The "almost function free" makes sure that
these redexes are exposed.
Note that this equality does *not* depend on casts or coercions, and so
skipping these forms is OK. In addition, the result of a type family cannot
be a polytype, so skipping foralls is OK, too. We skip foralls because we
want the output of the flattener to be almost function-free. See Note
[Flattening under a forall] in TcFlatten.
As I (Richard E) write this, it is unclear if the scenario pictured above
can happen -- I would expect the G Int and G Bool to be reduced. But
perhaps it can arise somehow, and maintaining almost function-free is cheap.
Historical note: CTyEqCans used to require only condition (1) above: that no
type family was at the top of an RHS. But work on #16512 suggested that the
injectivity checks were not complete, and adding the requirement that functions
do not appear even in a nested fashion was easy (it was already true, but
unenforced).
The almost-function-free property is checked by isAlmostFunctionFree in TcType.
The flattener (in TcFlatten) produces types that are almost function-free.
-}
mkNonCanonical :: CtEvidence -> Ct
......@@ -1637,8 +1684,7 @@ equality simplification, and type family reduction. (Why combine these? Because
it's actually quite easy to mistake one for another, in sufficiently involved
scenarios, like ConstraintKinds.)
The flag -fcontext-stack=n (not very well named!) fixes the maximium
level.
The flag -freduction-depth=n fixes the maximium level.
* The counter includes the depth of type class instance declarations. Example:
[W] d{7} : Eq [Int]
......
This diff is collapsed.
......@@ -29,10 +29,11 @@ import Type
import TcType( transSuperClasses )
import CoAxiom( TypeEqn )
import Unify
import FamInst( injTyVarsOfTypes )
import InstEnv
import VarSet
import VarEnv
import TyCoFVs
import FV
import Outputable
import ErrUtils( Validity(..), allValid )
import SrcLoc
......@@ -550,7 +551,7 @@ oclose preds fixed_tvs
-- closeOverKinds: see Note [Closing over kinds in coverage]
tv_fds :: [(TyCoVarSet,TyCoVarSet)]
tv_fds = [ (tyCoVarsOfTypes ls, injTyVarsOfTypes rs)
tv_fds = [ (tyCoVarsOfTypes ls, fvVarSet $ injectiveVarsOfTypes True rs)
-- See Note [Care with type functions]
| pred <- preds
, pred' <- pred : transSuperClasses pred
......
......@@ -1302,10 +1302,10 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
-- to an irreducible constraint; see typecheck/should_compile/T10494
-- See Note [Decomposing equality], note {4}
can_eq_app ev s1 t1 s2 t2
| CtDerived { ctev_loc = loc } <- ev
| CtDerived {} <- ev
= do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
; stopWith ev "Decomposed [D] AppTy" }
| CtWanted { ctev_dest = dest, ctev_loc = loc } <- ev
| CtWanted { ctev_dest = dest } <- ev
= do { co_s <- unifyWanted loc Nominal s1 s2
; let arg_loc
| isNextArgVisible s1 = loc
......@@ -1323,7 +1323,7 @@ can_eq_app ev s1 t1 s2 t2
| s1k `mismatches` s2k
= canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2)
| CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
| CtGiven { ctev_evar = evar } <- ev
= do { let co = mkTcCoVarCo evar
co_s = mkTcLRCo CLeft co
co_t = mkTcLRCo CRight co
......@@ -1335,6 +1335,8 @@ can_eq_app ev s1 t1 s2 t2
; canEqNC evar_s NomEq s1 s2 }
where
loc = ctEvLoc ev
s1k = tcTypeKind s1
s2k = tcTypeKind s2
......@@ -1585,6 +1587,7 @@ constraints: see Note [Instance and Given overlap] in TcInteract.
Conclusion:
* Decompose [W] N s ~R N t iff there no given constraint that could
later solve it.
-}
canDecomposableTyConAppOK :: CtEvidence -> EqRel
......@@ -1848,9 +1851,9 @@ canEqTyVar :: CtEvidence -- ev :: lhs ~ rhs
-> TcType -- lhs: pretty lhs, already flat
-> TcType -> TcType -- rhs: already flat
-> TcS (StopOrContinue Ct)
canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
canEqTyVar ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2
| k1 `tcEqType` k2
= canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
= canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2
-- So the LHS and RHS don't have equal kinds
-- Note [Flattening] in TcFlatten gives us (F2), which says that
......@@ -1889,7 +1892,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
(mkTcReflCo role xi1) rhs_co
-- NB: rewriteEqEvidence executes a swap, if any, so we're
-- NotSwapped now.
; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_ty1 new_rhs ps_rhs }
; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_xi1 new_rhs ps_rhs }
else
do { let sym_k1_co = mkTcSymCo k1_co -- :: kind(xi1) ~N flat_k1
sym_k2_co = mkTcSymCo k2_co -- :: kind(xi2) ~N flat_k2
......@@ -1905,7 +1908,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
-- no longer swapped, due to rewriteEqEvidence
; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_ty1
; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_xi1
new_rhs flat_k2 ps_rhs } }
where
xi1 = mkTyVarTy tv1
......@@ -1969,16 +1972,16 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
canEqTyVarHomo :: CtEvidence
-> EqRel -> SwapFlag
-> TcTyVar -- lhs: tv1
-> TcType -- pretty lhs
-> TcType -> TcType -- rhs (might not be flat)
-> TcType -- pretty lhs, flat
-> TcType -> TcType -- rhs, flat
-> TcS (StopOrContinue Ct)
canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _
| Just (tv2, _) <- tcGetCastedTyVar_maybe ty2
canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 _
| Just (tv2, _) <- tcGetCastedTyVar_maybe xi2
, tv1 == tv2
= canEqReflexive ev eq_rel (mkTyVarTy tv1)
-- we don't need to check co because it must be reflexive
| Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
| Just (tv2, co2) <- tcGetCastedTyVar_maybe xi2
, swapOverTyVars tv1 tv2
= do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
-- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
......@@ -1998,11 +2001,11 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _
; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
; dflags <- getDynFlags
; canEqTyVar2 dflags new_ev eq_rel IsSwapped tv2 (ps_ty1 `mkCastTy` sym_co2) }
; canEqTyVar2 dflags new_ev eq_rel IsSwapped tv2 (ps_xi1 `mkCastTy` sym_co2) }
canEqTyVarHomo ev eq_rel swapped tv1 _ _ ps_ty2
canEqTyVarHomo ev eq_rel swapped tv1 _ _ ps_xi2
= do { dflags <- getDynFlags
; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_xi2 }
-- The RHS here is either not a casted tyvar, or it's a tyvar but we want
-- to rewrite the LHS to the RHS (as per swapOverTyVars)
......@@ -2011,7 +2014,7 @@ canEqTyVar2 :: DynFlags
-> EqRel
-> SwapFlag
-> TcTyVar -- lhs = tv, flat
-> TcType -- rhs
-> TcType -- rhs, flat
-> TcS (StopOrContinue Ct)
-- LHS is an inert type variable,
-- and RHS is fully rewritten, but with type synonyms
......@@ -2186,7 +2189,7 @@ However, if we encounter an equality constraint with a type synonym
application on one side and a variable on the other side, we should
NOT (necessarily) expand the type synonym, since for the purpose of
good error messages we want to leave type synonyms unexpanded as much
as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
as possible. Hence the ps_xi1, ps_xi2 argument passed to canEqTyVar.
-}
......
......@@ -3,6 +3,7 @@
module TcFlatten(
FlattenMode(..),
flatten, flattenKind, flattenArgsNom,
rewriteTyVar,
unflattenWanteds
) where
......@@ -456,7 +457,8 @@ type FlatWorkListRef = TcRef [Ct] -- See Note [The flattening work list]
data FlattenEnv
= FE { fe_mode :: !FlattenMode
, fe_loc :: !CtLoc -- See Note [Flattener CtLoc]
, fe_loc :: CtLoc -- See Note [Flattener CtLoc]
-- unbanged because it's bogus in rewriteTyVar
, fe_flavour :: !CtFlavour
, fe_eq_rel :: !EqRel -- See Note [Flattener EqRels]
, fe_work :: !FlatWorkListRef } -- See Note [The flattening work list]
......@@ -520,7 +522,8 @@ runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a
runFlatten mode loc flav eq_rel thing_inside
= do { flat_ref <- newTcRef []
; let fmode = FE { fe_mode = mode
, fe_loc = loc
, fe_loc = bumpCtLocDepth loc
-- See Note [Flatten when discharging CFunEqCan]
, fe_flavour = flav
, fe_eq_rel = eq_rel
, fe_work = flat_ref }
......@@ -743,8 +746,27 @@ changes the flavour from Derived just for this purpose.
* They are all wrapped in runFlatten, so their *
* flattening work gets put into the work list *
* *
********************************************************************* -}
*********************************************************************
Note [rewriteTyVar]
~~~~~~~~~~~~~~~~~~~~~~
Suppose we have an injective function F and
inert_funeqs: F t1 ~ fsk1
F t2 ~ fsk2
inert_eqs: fsk1 ~ [a]
a ~ Int
fsk2 ~ [Int]
We never rewrite the RHS (cc_fsk) of a CFunEqCan. But we /do/ want to get the
[D] t1 ~ t2 from the injectiveness of F. So we flatten cc_fsk of CFunEqCans
when trying to find derived equalities arising from injectivity.
-}
-- | See Note [Flattening].
-- If (xi, co) <- flatten mode ev ty, then co :: xi ~r ty
-- where r is the role in @ev@. If @mode@ is 'FM_FlattenAll',
-- then 'xi' is almost function-free (Note [Almost function-free]
-- in TcRnTypes).
flatten :: FlattenMode -> CtEvidence -> TcType
-> TcS (Xi, TcCoercion)
flatten mode ev ty
......@@ -753,8 +775,27 @@ flatten mode ev ty
; traceTcS "flatten }" (ppr ty')
; return (ty', co) }
-- Apply the inert set as an *inert generalised substitution* to
-- a variable, zonking along the way.
-- See Note [inert_eqs: the inert equalities] in TcSMonad.
-- Equivalently, this flattens the variable with respect to NomEq
-- in a Derived constraint. (Why Derived? Because Derived allows the
-- most about of rewriting.) Returns no coercion, because we're
-- using Derived constraints.
-- See Note [rewriteTyVar]
rewriteTyVar :: TcTyVar -> TcS TcType
rewriteTyVar tv
= do { traceTcS "rewriteTyVar {" (ppr tv)
; (ty, _) <- runFlatten FM_SubstOnly fake_loc Derived NomEq $
flattenTyVar tv
; traceTcS "rewriteTyVar }" (ppr ty)
; return ty }
where
fake_loc = pprPanic "rewriteTyVar used a CtLoc" (ppr tv)
-- specialized to flattening 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)
......@@ -765,6 +806,7 @@ flattenKind loc flav ty
; traceTcS "flattenKind }" (ppr ty' $$ ppr co) -- co is never a panic
; return (ty', co) }
-- See Note [Flattening]
flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], TcCoercionN)
-- Externally-callable, hence runFlatten
-- Flatten a vector of types all at once; in fact they are
......@@ -811,6 +853,9 @@ Flattening also:
* zonks, removing any metavariables, and
* applies the substitution embodied in the inert set
The result of flattening is *almost function-free*. See
Note [Almost function-free] in TcRnTypes.
Because flattening 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:
......@@ -1575,7 +1620,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 { traceFlat "Following inert tyvar"
(ppr mode <+>
ppr tv <+>
equals <+>
......
......@@ -1343,59 +1343,61 @@ improveLocalFunEqs work_ev inerts fam_tc args fsk
|| not (isImprovable work_ev)
= return ()
| not (null improvement_eqns)
= do { traceTcS "interactFunEq improvements: " $
vcat [ text "Eqns:" <+> ppr improvement_eqns
, text "Candidates:" <+> ppr funeqs_for_tc
, text "Inert eqs:" <+> ppr ieqs ]
; emitFunDepDeriveds improvement_eqns }
| otherwise
= return ()
= do { eqns <- improvement_eqns
; if not (null eqns)
then do { traceTcS "interactFunEq improvements: " $
vcat [ text "Eqns:" <+> ppr eqns
, text "Candidates:" <+> ppr funeqs_for_tc
, text "Inert eqs:" <+> ppr (inert_eqs inerts) ]
; emitFunDepDeriveds eqns }
else return () }
where
ieqs = inert_eqs inerts
funeqs = inert_funeqs inerts
funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
rhs = lookupFlattenTyVar ieqs fsk
work_loc = ctEvLoc work_ev
work_pred = ctEvPred work_ev
fam_inj_info = tyConInjectivityInfo fam_tc
--------------------
improvement_eqns :: [FunDepEqn CtLoc]
improvement_eqns :: TcS [FunDepEqn CtLoc]
improvement_eqns
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
= -- Try built-in families, notably for arithmethic
concatMap (do_one_built_in ops) funeqs_for_tc
do { rhs <- rewriteTyVar fsk
; concatMapM (do_one_built_in ops rhs) funeqs_for_tc }
| Injective injective_args <- fam_inj_info
= -- Try improvement from type families with injectivity annotations
concatMap (do_one_injective injective_args) funeqs_for_tc
do { rhs <- rewriteTyVar fsk
; concatMapM (do_one_injective injective_args rhs) funeqs_for_tc }
| otherwise
= []
= return []
--------------------
do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = inert_ev })
= mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs
(lookupFlattenTyVar ieqs ifsk))
do_one_built_in ops rhs (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = inert_ev })
= do { inert_rhs <- rewriteTyVar ifsk
; return $ mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs inert_rhs) }
do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
do_one_built_in _ _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
--------------------
-- See Note [Type inference for type families with injectivity]
do_one_injective inj_args (CFunEqCan { cc_tyargs = inert_args
, cc_fsk = ifsk, cc_ev = inert_ev })
do_one_injective inj_args rhs (CFunEqCan { cc_tyargs = inert_args
, cc_fsk = ifsk, cc_ev = inert_ev })
| isImprovable inert_ev
, rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
= mk_fd_eqns inert_ev $
[ Pair arg iarg
| (arg, iarg, True) <- zip3 args inert_args inj_args ]
= do { inert_rhs <- rewriteTyVar ifsk
; return $ if rhs `tcEqType` inert_rhs
then mk_fd_eqns inert_ev $
[ Pair arg iarg
| (arg, iarg, True) <- zip3 args inert_args inj_args ]
else [] }
| otherwise
= []
= return []
do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
do_one_injective _ _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
--------------------
mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn CtLoc]
......@@ -1870,6 +1872,63 @@ See
* Note [Evidence for quantified constraints] in Predicate
* Note [Equality superclasses in quantified constraints]
in TcCanonical
Note [Flatten when discharging CFunEqCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We have the following scenario (#16512):
type family LV (as :: [Type]) (b :: Type) = (r :: Type) | r -> as b where
LV (a ': as) b = a -> LV as b
[WD] w1 :: LV as0 (a -> b) ~ fmv1 (CFunEqCan)
[WD] w2 :: fmv1 ~ (a -> fmv2) (CTyEqCan)
[WD] w3 :: LV as0 b ~ fmv2 (CFunEqCan)
We start with w1. Because LV is injective, we wish to see if the RHS of the
equation matches the RHS of the CFunEqCan. The RHS of a CFunEqCan is always an
fmv, so we "look through" to get (a -> fmv2). Then we run tcUnifyTyWithTFs.
That performs the match, but it allows a type family application (such as the
LV in the RHS of the equation) to match with anything. (See "Injective type
families" by Stolarek et al., HS'15, Fig. 2) The matching succeeds, which
means we can improve as0 (and b, but that's not interesting here). However,
because the RHS of w1 can't see through fmv2 (we have no way of looking up a
LHS of a CFunEqCan from its RHS, and this use case isn't compelling enough),
we invent a new unification variable here. We thus get (as0 := a : as1).
Rewriting:
[WD] w1 :: LV (a : as1) (a -> b) ~ fmv1
[WD] w2 :: fmv1 ~ (a -> fmv2)
[WD] w3 :: LV (a : as1) b ~ fmv2
We can now reduce both CFunEqCans, using the equation for LV. We get
[WD] w2 :: (a -> LV as1 (a -> b)) ~ (a -> a -> LV as1 b)
Now we decompose (and flatten) to
[WD] w4 :: LV as1 (a -> b) ~ fmv3
[WD] w5 :: fmv3 ~ (a -> fmv1)
[WD] w6 :: LV as1 b ~ fmv4
which is exactly where we started. These goals really are insoluble, but
we would prefer not to loop. We thus need to find a way to bump the reduction
depth, so that we can detect the loop and abort.
The key observation is that we are performing a reduction. We thus wish
to bump the level when discharging a CFunEqCan. Where does this bumped
level go, though? It can't just go on the reduct, as that's a type. Instead,
it must go on any CFunEqCans produced after flattening. We thus flatten
when discharging, making sure that the level is bumped in the new
fun-eqs. The flattening happens in reduce_top_fun_eq and the level
is bumped when setting up the FlatM monad in TcFlatten.runFlatten.
(This bumping will happen for call sites other than this one, but that
makes sense -- any constraints emitted by the flattener are offshoots
the work item and should have a higher level. We don't have any test
cases that require the bumping in this other cases, but it's convenient
and causes no harm to bump at every flatten.)
Test case: typecheck/should_fail/T16512a
-}
--------------------
......@@ -1898,6 +1957,7 @@ reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
-> TcS (StopOrContinue Ct)
-- We have found an applicable top-level axiom: use it to reduce
-- Precondition: fsk is not free in rhs_ty
-- ax_co :: F tys ~ rhs_ty, where F tys is the LHS of the old_ev
reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
| not (isDerived old_ev) -- Precondition of shortCutReduction
, Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
......@@ -1912,7 +1972,11 @@ reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
= ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
, ppr old_ev $$ ppr rhs_ty )
-- Guaranteed by Note [FunEq occurs-check principle]
do { dischargeFunEq old_ev fsk ax_co rhs_ty
do { (rhs_xi, flatten_co) <- flatten FM_FlattenAll old_ev rhs_ty
-- flatten_co :: rhs_xi ~ rhs_ty
-- See Note [Flatten when discharging CFunEqCan]
; let total_co = ax_co `mkTcTransCo` mkTcSymCo flatten_co
; dischargeFunEq old_ev fsk total_co rhs_xi
; traceTcS "doTopReactFunEq" $
vcat [ text "old_ev:" <+> ppr old_ev
, nest 2 (text ":=") <+> ppr ax_co ]
......@@ -1926,16 +1990,16 @@ improveTopFunEqs ev fam_tc args fsk
= return ()
| otherwise
= do { ieqs <- getInertEqs
; fam_envs <- getFamInstEnvs
; eqns <- improve_top_fun_eqs fam_envs fam_tc args
(lookupFlattenTyVar ieqs fsk)
; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
= do { fam_envs <- getFamInstEnvs
; rhs <- rewriteTyVar fsk
; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs
; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs
, ppr eqns ])
; mapM_ (unifyDerived loc Nominal) eqns }
where
loc = ctEvLoc ev -- ToDo: this location is wrong; it should be FunDepOrigin2
-- See #14778
loc = bumpCtLocDepth (ctEvLoc ev)
-- ToDo: this location is wrong; it should be FunDepOrigin2
-- See #14778
improve_top_fun_eqs :: FamInstEnvs
-> TyCon -> [TcType] -> TcType
......
......@@ -1990,13 +1990,10 @@ zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
; return (WC { wc_simple = simple', wc_impl = implic' }) }
zonkSimples :: Cts -> TcM Cts
zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
zonkSimples cts = do { cts' <- mapBagM zonkCt cts
; traceTc "zonkSimples done:" (ppr cts')
; return cts' }
zonkCt' :: Ct -> TcM Ct
zonkCt' ct = zonkCt ct
{- Note [zonkCt behaviour]
~~~~~~~~~~~~~~~~~~~~~~~~~~
zonkCt tries to maintain the canonical form of a Ct. For example,
......@@ -2035,15 +2032,12 @@ zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
; args' <- mapM zonkTcType args
; return $ ct { cc_ev = ev', cc_tyargs = args' } }
zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
= do { ev' <- zonkCtEvidence ev
; tv_ty' <- zonkTcTyVar tv
; case getTyVar_maybe tv_ty' of
Just tv' -> do { rhs' <- zonkTcType rhs
; return ct { cc_ev = ev'
, cc_tyvar = tv'
, cc_rhs = rhs' } }
Nothing -> return (mkNonCanonical ev') }
zonkCt (CTyEqCan { cc_ev = ev })
= mkNonCanonical <$> zonkCtEvidence ev
-- CTyEqCan has some delicate invariants that may be violated by
-- zonking (documented with the Ct type) , so we don't want to create
-- a CTyEqCan here. Besides, this will be canonicalized again anyway,
-- so there is very little benefit in keeping the CTyEqCan constructor.
zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
= do { ev' <- zonkCtEvidence ev
......
......@@ -79,7 +79,7 @@ module TcSMonad (
-- Inert CTyEqCans
EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
lookupFlattenTyVar, lookupInertTyVar,
lookupInertTyVar,
-- Inert solved dictionaries
addSolvedDict, lookupSolvedDict,
......@@ -233,7 +233,7 @@ It's very important to process equalities /first/:
* (Kick-out) We want to apply this priority scheme to kicked-out
constraints too (see the call to extendWorkListCt in kick_out_rewritable
E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
homo-kinded when kicked out, and hence we want to priotitise it.
homo-kinded when kicked out, and hence we want to prioritise it.
* (Derived equalities) Originally we tried to postpone processing
Derived equalities, in the hope that we might never need to deal
......@@ -257,6 +257,7 @@ So we arrange to put these particular class constraints in the wl_eqs.
NB: since we do not currently apply the substitution to the
inert_solved_dicts, the knot-tying still seems a bit fragile.
But this makes it better.
-}
-- See Note [WorkList priorities]
......@@ -763,8 +764,7 @@ The InertCans represents a collection of constraints with the following properti
to the CTyEqCan equalities (modulo canRewrite of course;
eg a wanted cannot rewrite a given)
* CTyEqCan equalities: see Note [Applying the inert substitution]
in TcFlatten
* CTyEqCan equalities: see Note [inert_eqs: the inert equalities]
Note [EqualCtList invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1519,25 +1519,6 @@ lookupInertTyVar ieqs tv
Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _ ) -> Just rhs
_ -> Nothing
lookupFlattenTyVar :: InertEqs -> TcTyVar -> TcType
-- See Note [lookupFlattenTyVar]
lookupFlattenTyVar ieqs ftv
= lookupInertTyVar ieqs ftv `orElse` mkTyVarTy ftv
{- Note [lookupFlattenTyVar]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have an injective function F and
inert_funeqs: F t1 ~ fsk1
F t2 ~ fsk2
inert_eqs: fsk1 ~ fsk2
We never rewrite the RHS (cc_fsk) of a CFunEqCan. But we /do/ want to
get the [D] t1 ~ t2 from the injectiveness of F. So we look up the
cc_fsk of CFunEqCans in the inert_eqs when trying to find derived
equalities arising from injectivity.
-}
{- *********************************************************************
* *
Inert instances: inert_insts
......@@ -1723,7 +1704,7 @@ kick_out_rewritable new_fr new_tv
kicked_out :: WorkList
-- NB: use extendWorkList to ensure that kicked-out equalities get priority
-- See Note [Prioritise equality constraints] (Kick-out).
-- See Note [Prioritise equalities] (Kick-out).
-- The irreds may include non-canonical (hetero-kinded) equality
-- constraints, which perhaps may have become soluble after new_tv
-- is substituted; ditto the dictionaries, which may include (a~b)
......@@ -3289,6 +3270,7 @@ dischargeFunEq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
-- - co :: F tys ~ xi
-- - fmv/fsk `notElem` xi
-- - fmv not filled (for Wanteds)
-- - xi is flattened (and obeys Note [Almost function-free] in TcRnTypes)
--
-- Then for [W] or [WD], we actually fill in the fmv:
-- set fmv := xi,
......@@ -3568,11 +3550,12 @@ checkReductionDepth loc ty
wrapErrTcS $
solverDepthErrorTcS loc ty }
matchFam :: TyCon -> [Type] -> TcS (Maybe (Coercion, TcType))
matchFam :: TyCon -> [Type] -> TcS (Maybe (CoercionN, TcType))
-- Given (F tys) return (ty, co), where co :: F tys ~N ty
matchFam tycon args = wrapTcS $ matchFamTcM tycon args
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, TcType))
-- Given (F tys) return (ty, co), where co :: F tys ~ ty
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (CoercionN, TcType))
-- Given (F tys) return (ty, co), where co :: F tys ~N ty
matchFamTcM tycon args
= do { fam_envs <- FamInst.tcGetFamInstEnvs
; let match_fam_result
......
......@@ -81,7 +81,7 @@ module TcType (
hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck,
checkValidClsArgs, hasTyVarHead,
isRigidTy,
isRigidTy, isAlmostFunctionFree,
---------------------------------
-- Misc type manipulators
......@@ -2057,6 +2057,24 @@ isRigidTy ty
| isForAllTy ty = True
| otherwise = False
-- | Is this type *almost function-free*? See Note [Almost function-free]
-- in TcRnTypes
isAlmostFunctionFree :: TcType -> Bool
isAlmostFunctionFree ty | Just ty' <- tcView ty = isAlmostFunctionFree ty'
isAlmostFunctionFree (TyVarTy {}) = True
isAlmostFunctionFree (AppTy ty1 ty2) = isAlmostFunctionFree ty1 &&
isAlmostFunctionFree ty2
isAlmostFunctionFree (TyConApp tc args)
| isTypeFamilyTyCon tc = False
| otherwise = all isAlmostFunctionFree args
isAlmostFunctionFree (ForAllTy bndr _) = isAlmostFunctionFree (binderType bndr)
isAlmostFunctionFree (FunTy _ ty1 ty2) = isAlmostFunctionFree ty1 &&
isAlmostFunctionFree ty2
isAlmostFunctionFree (LitTy {}) = True
isAlmostFunctionFree (CastTy ty _) = isAlmostFunctionFree ty
isAlmostFunctionFree (CoercionTy {}) = True
{-
************************************************************************
* *
......
......@@ -2027,11 +2027,12 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
-- See Note [Ver