diff options
author | Richard Eisenberg <rae@richarde.dev> | 2020-09-26 15:32:08 -0400 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-09-30 02:50:17 -0400 |
commit | 7c98699f685d8c53fd594b6de22b425ed951174f (patch) | |
tree | 11114a28cecadf9f0f592fcbe05044c6d8a74a1b | |
parent | 9befd94d79a78fd53a28a4ce051a91d2215d069c (diff) | |
download | haskell-7c98699f685d8c53fd594b6de22b425ed951174f.tar.gz |
Omit redundant kind equality check in solver
See updated Note [Use loose types in inert set] in
GHC.Tc.Solver.Monad.
Close #18753.
-rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 34 |
1 files changed, 21 insertions, 13 deletions
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index aaa1a8428a..10c577e723 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -2357,10 +2357,8 @@ lookupFlatCache fam_tc tys lookup_flats flat_cache]) } where lookup_inerts inert_funeqs - | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk, cc_tyargs = xis }) + | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk }) <- findFunEq inert_funeqs fam_tc tys - , tys `eqTypes` xis -- The lookup might find a near-match; see - -- Note [Use loose types in inert set] = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev) | otherwise = Nothing @@ -2377,16 +2375,14 @@ lookupInInerts loc pty | otherwise -- NB: No caching for equalities, IPs, holes, or errors = return Nothing --- | Look up a dictionary inert. NB: the returned 'CtEvidence' might not --- match the input exactly. Note [Use loose types in inert set]. +-- | Look up a dictionary inert. lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence lookupInertDict (IC { inert_dicts = dicts }) loc cls tys = case findDict dicts loc cls tys of Just ct -> Just (ctEvidence ct) _ -> Nothing --- | Look up a solved inert. NB: the returned 'CtEvidence' might not --- match the input exactly. See Note [Use loose types in inert set]. +-- | Look up a solved inert. lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence -- Returns just if exactly this predicate type exists in the solved. lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys @@ -2412,12 +2408,24 @@ foldIrreds k irreds z = foldr k z irreds Note [Use loose types in inert set] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly -solvable from the other. So, we do lookup in the inert set using -loose types, which omit the kind-check. - -We must be careful when using the result of a lookup because it may -not match the requested info exactly! +Whenever we are looking up an inert dictionary (CDictCan) or function +equality (CFunEqCan), we use a TcAppMap, which uses the Unique of the +class/type family tycon and then a trie which maps the arguments. This +trie does *not* need to match the kinds of the arguments; this Note +explains why. + +Consider the types ty0 = (T ty1 ty2 ty3 ty4) and ty0' = (T ty1' ty2' ty3' ty4'), +where ty4 and ty4' have different kinds. Let's further assume that both types +ty0 and ty0' are well-typed. Because the kind of T is closed, it must be that +one of the ty1..ty3 does not match ty1'..ty3' (and that the kind of the fourth +argument to T is dependent on whichever one changed). Since we are matching +all arguments, during the inert-set lookup, we know that ty1..ty3 do indeed +match ty1'..ty3'. Therefore, the kind of ty4 and ty4' must match, too -- +without ever looking at it. + +Accordingly, we use LooseTypeMap, which skips the kind check when looking +up a type. I (Richard E) believe this is just an optimization, and that +looking at kinds would be harmless. -} |