never executed always true always false
1 {-# LANGUAGE DerivingStrategies #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
4 {-# LANGUAGE PatternSynonyms #-}
5
6 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
7
8 -- | Utility types used within the constraint solver
9 module GHC.Tc.Solver.Types (
10 -- Inert CDictCans
11 DictMap, emptyDictMap, findDictsByClass, addDict, addDictCt,
12 addDictsByClass, delDict, foldDicts, filterDicts, findDict,
13 dictsToBag, partitionDicts,
14
15 FunEqMap, emptyFunEqs, foldFunEqs, findFunEq, insertFunEq,
16 findFunEqsByTyCon,
17
18 TcAppMap, emptyTcAppMap, isEmptyTcAppMap,
19 insertTcApp, alterTcApp, filterTcAppMap,
20 tcAppMapToBag, foldTcAppMap,
21
22 EqualCtList, pattern EqualCtList,
23 equalCtListToList, filterEqualCtList, unitEqualCtList,
24 listToEqualCtList, addToEqualCtList,
25 ) where
26
27 import GHC.Prelude
28
29 import GHC.Tc.Types.Constraint
30 import GHC.Tc.Types.Origin
31 import GHC.Tc.Utils.TcType
32
33 import GHC.Core.Class
34 import GHC.Core.Map.Type
35 import GHC.Core.Predicate
36 import GHC.Core.TyCon
37 import GHC.Core.TyCon.Env
38
39 import GHC.Data.Bag
40 import GHC.Data.Maybe
41 import GHC.Data.TrieMap
42 import GHC.Utils.Outputable
43 import GHC.Utils.Panic
44
45 import Data.Foldable
46 import Data.List.NonEmpty ( NonEmpty(..), nonEmpty, cons )
47 import qualified Data.List.NonEmpty as NE
48
49 {- *********************************************************************
50 * *
51 TcAppMap
52 * *
53 ************************************************************************
54
55 Note [Use loose types in inert set]
56 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
57 Whenever we are looking up an inert dictionary (CDictCan) or function
58 equality (CEqCan), we use a TcAppMap, which uses the Unique of the
59 class/type family tycon and then a trie which maps the arguments. This
60 trie does *not* need to match the kinds of the arguments; this Note
61 explains why.
62
63 Consider the types ty0 = (T ty1 ty2 ty3 ty4) and ty0' = (T ty1' ty2' ty3' ty4'),
64 where ty4 and ty4' have different kinds. Let's further assume that both types
65 ty0 and ty0' are well-typed. Because the kind of T is closed, it must be that
66 one of the ty1..ty3 does not match ty1'..ty3' (and that the kind of the fourth
67 argument to T is dependent on whichever one changed). Since we are matching
68 all arguments, during the inert-set lookup, we know that ty1..ty3 do indeed
69 match ty1'..ty3'. Therefore, the kind of ty4 and ty4' must match, too --
70 without ever looking at it.
71
72 Accordingly, we use LooseTypeMap, which skips the kind check when looking
73 up a type. I (Richard E) believe this is just an optimization, and that
74 looking at kinds would be harmless.
75
76 -}
77
78 type TcAppMap a = DTyConEnv (ListMap LooseTypeMap a)
79 -- Indexed by tycon then the arg types, using "loose" matching, where
80 -- we don't require kind equality. This allows, for example, (a |> co)
81 -- to match (a).
82 -- See Note [Use loose types in inert set]
83 -- Used for types and classes; hence UniqDFM
84 -- See Note [foldTM determinism] in GHC.Data.TrieMap for why we use DTyConEnv here
85
86 isEmptyTcAppMap :: TcAppMap a -> Bool
87 isEmptyTcAppMap m = isEmptyDTyConEnv m
88
89 emptyTcAppMap :: TcAppMap a
90 emptyTcAppMap = emptyDTyConEnv
91
92 findTcApp :: TcAppMap a -> TyCon -> [Type] -> Maybe a
93 findTcApp m tc tys = do { tys_map <- lookupDTyConEnv m tc
94 ; lookupTM tys tys_map }
95
96 delTcApp :: TcAppMap a -> TyCon -> [Type] -> TcAppMap a
97 delTcApp m tc tys = adjustDTyConEnv (deleteTM tys) m tc
98
99 insertTcApp :: TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
100 insertTcApp m tc tys ct = alterDTyConEnv alter_tm m tc
101 where
102 alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
103
104 alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
105 alterTcApp m tc tys upd = alterDTyConEnv alter_tm m tc
106 where
107 alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
108 alter_tm m_elt = Just (alterTM tys upd (m_elt `orElse` emptyTM))
109
110 filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
111 filterTcAppMap f m = mapMaybeDTyConEnv one_tycon m
112 where
113 one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
114 one_tycon tm
115 | isEmptyTM filtered_tm = Nothing
116 | otherwise = Just filtered_tm
117 where
118 filtered_tm = filterTM f tm
119
120 tcAppMapToBag :: TcAppMap a -> Bag a
121 tcAppMapToBag m = foldTcAppMap consBag m emptyBag
122
123 foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
124 foldTcAppMap k m z = foldDTyConEnv (foldTM k) z m
125
126 {- *********************************************************************
127 * *
128 DictMap
129 * *
130 ********************************************************************* -}
131
132 type DictMap a = TcAppMap a
133
134 emptyDictMap :: DictMap a
135 emptyDictMap = emptyTcAppMap
136
137 findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
138 findDict m loc cls tys
139 | hasIPSuperClasses cls tys -- See Note [Tuples hiding implicit parameters]
140 = Nothing
141
142 | Just {} <- isCallStackPred cls tys
143 , isPushCallStackOrigin (ctLocOrigin loc)
144 = Nothing -- See Note [Solving CallStack constraints]
145
146 | otherwise
147 = findTcApp m (classTyCon cls) tys
148
149 findDictsByClass :: DictMap a -> Class -> Bag a
150 findDictsByClass m cls
151 | Just tm <- lookupDTyConEnv m (classTyCon cls) = foldTM consBag tm emptyBag
152 | otherwise = emptyBag
153
154 delDict :: DictMap a -> Class -> [Type] -> DictMap a
155 delDict m cls tys = delTcApp m (classTyCon cls) tys
156
157 addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
158 addDict m cls tys item = insertTcApp m (classTyCon cls) tys item
159
160 addDictCt :: DictMap Ct -> TyCon -> [Type] -> Ct -> DictMap Ct
161 -- Like addDict, but combines [W] and [D] to [WD]
162 -- See Note [KeepBoth] in GHC.Tc.Solver.Interact
163 addDictCt m tc tys new_ct = alterTcApp m tc tys xt_ct
164 where
165 new_ct_ev = ctEvidence new_ct
166
167 xt_ct :: Maybe Ct -> Maybe Ct
168 xt_ct (Just old_ct)
169 | CtWanted { ctev_nosh = WOnly } <- old_ct_ev
170 , CtDerived {} <- new_ct_ev
171 = Just (old_ct { cc_ev = old_ct_ev { ctev_nosh = WDeriv }})
172 | CtDerived {} <- old_ct_ev
173 , CtWanted { ctev_nosh = WOnly } <- new_ct_ev
174 = Just (new_ct { cc_ev = new_ct_ev { ctev_nosh = WDeriv }})
175 where
176 old_ct_ev = ctEvidence old_ct
177
178 xt_ct _ = Just new_ct
179
180 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
181 addDictsByClass m cls items
182 = extendDTyConEnv m (classTyCon cls) (foldr add emptyTM items)
183 where
184 add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
185 add ct _ = pprPanic "addDictsByClass" (ppr ct)
186
187 filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
188 filterDicts f m = filterTcAppMap f m
189
190 partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
191 partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDictMap)
192 where
193 k ct (yeses, noes) | f ct = (ct `consBag` yeses, noes)
194 | otherwise = (yeses, add ct noes)
195 add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
196 = addDict m cls tys ct
197 add ct _ = pprPanic "partitionDicts" (ppr ct)
198
199 dictsToBag :: DictMap a -> Bag a
200 dictsToBag = tcAppMapToBag
201
202 foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
203 foldDicts = foldTcAppMap
204
205 {- Note [Tuples hiding implicit parameters]
206 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
207 Consider
208 f,g :: (?x::Int, C a) => a -> a
209 f v = let ?x = 4 in g v
210
211 The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
212 We must /not/ solve this from the Given (?x::Int, C a), because of
213 the intervening binding for (?x::Int). #14218.
214
215 We deal with this by arranging that we always fail when looking up a
216 tuple constraint that hides an implicit parameter. Not that this applies
217 * both to the inert_dicts (lookupInertDict)
218 * and to the solved_dicts (looukpSolvedDict)
219 An alternative would be not to extend these sets with such tuple
220 constraints, but it seemed more direct to deal with the lookup.
221
222 Note [Solving CallStack constraints]
223 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
224 See also Note [Overview of implicit CallStacks] in GHc.Tc.Types.Evidence.
225
226 Suppose f :: HasCallStack => blah. Then
227
228 * Each call to 'f' gives rise to
229 [W] s1 :: IP "callStack" CallStack -- CtOrigin = OccurrenceOf f
230 with a CtOrigin that says "OccurrenceOf f".
231 Remember that HasCallStack is just shorthand for
232 IP "callStack" CallStack
233 See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
234
235 * We cannonicalise such constraints, in GHC.Tc.Solver.Canonical.canClassNC, by
236 pushing the call-site info on the stack, and changing the CtOrigin
237 to record that has been done.
238 Bind: s1 = pushCallStack <site-info> s2
239 [W] s2 :: IP "callStack" CallStack -- CtOrigin = IPOccOrigin
240
241 * Then, and only then, we can solve the constraint from an enclosing
242 Given.
243
244 So we must be careful /not/ to solve 's1' from the Givens. Again,
245 we ensure this by arranging that findDict always misses when looking
246 up such constraints.
247 -}
248
249 {- *********************************************************************
250 * *
251 FunEqMap
252 * *
253 ********************************************************************* -}
254
255 type FunEqMap a = TcAppMap a -- A map whose key is a (TyCon, [Type]) pair
256
257 emptyFunEqs :: TcAppMap a
258 emptyFunEqs = emptyTcAppMap
259
260 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
261 findFunEq m tc tys = findTcApp m tc tys
262
263 findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
264 -- Get inert function equation constraints that have the given tycon
265 -- in their head. Not that the constraints remain in the inert set.
266 -- We use this to check for derived interactions with built-in type-function
267 -- constructors.
268 findFunEqsByTyCon m tc
269 | Just tm <- lookupDTyConEnv m tc = foldTM (:) tm []
270 | otherwise = []
271
272 foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
273 foldFunEqs = foldTcAppMap
274
275 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
276 insertFunEq m tc tys val = insertTcApp m tc tys val
277
278 {- *********************************************************************
279 * *
280 EqualCtList
281 * *
282 ********************************************************************* -}
283
284 {- Note [EqualCtList invariants]
285 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
286 * All are equalities
287 * All these equalities have the same LHS
288 * The list is never empty
289 * No element of the list can rewrite any other
290 * Derived before Wanted
291
292 From the fourth invariant it follows that the list is
293 - A single [G], or
294 - Zero or one [D] or [WD], followed by any number of [W]
295
296 The Wanteds can't rewrite anything which is why we put them last
297 -}
298
299 newtype EqualCtList = MkEqualCtList (NonEmpty Ct)
300 deriving newtype Outputable
301 -- See Note [EqualCtList invariants]
302
303 -- | Pattern synonym for easy unwrapping. NB: unidirectional to
304 -- preserve invariants.
305 pattern EqualCtList :: NonEmpty Ct -> EqualCtList
306 pattern EqualCtList cts <- MkEqualCtList cts
307 {-# COMPLETE EqualCtList #-}
308
309 unitEqualCtList :: Ct -> EqualCtList
310 unitEqualCtList ct = MkEqualCtList (ct :| [])
311
312 addToEqualCtList :: Ct -> EqualCtList -> EqualCtList
313 -- NB: This function maintains the "derived-before-wanted" invariant of EqualCtList,
314 -- but not the others. See Note [EqualCtList invariants]
315 addToEqualCtList ct (MkEqualCtList old_eqs)
316 | isWantedCt ct
317 , eq1 :| eqs <- old_eqs
318 = MkEqualCtList (eq1 :| ct : eqs)
319 | otherwise
320 = MkEqualCtList (ct `cons` old_eqs)
321
322 filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
323 filterEqualCtList pred (MkEqualCtList cts)
324 = fmap MkEqualCtList (nonEmpty $ NE.filter pred cts)
325
326 equalCtListToList :: EqualCtList -> [Ct]
327 equalCtListToList (MkEqualCtList cts) = toList cts
328
329 listToEqualCtList :: [Ct] -> Maybe EqualCtList
330 -- NB: This does not maintain invariants other than having the EqualCtList be
331 -- non-empty
332 listToEqualCtList cts = MkEqualCtList <$> nonEmpty cts