never executed always true always false
1 {-# LANGUAGE DerivingStrategies #-}
2
3 {-
4
5 Describes predicates as they are considered by the solver.
6
7 -}
8
9 module GHC.Core.Predicate (
10 Pred(..), classifyPredType,
11 isPredTy, isEvVarType,
12
13 -- Equality predicates
14 EqRel(..), eqRelRole,
15 isEqPrimPred, isEqPred,
16 getEqPredTys, getEqPredTys_maybe, getEqPredRole,
17 predTypeEqRel,
18 mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
19 mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
20
21 -- Special predicates
22 SpecialPred(..), specialPredTyCon,
23
24 -- Class predicates
25 mkClassPred, isDictTy,
26 isClassPred, isEqPredClass, isCTupleClass,
27 getClassPredTys, getClassPredTys_maybe,
28 classMethodTy, classMethodInstTy,
29
30 -- Implicit parameters
31 isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass,
32 isCallStackTy, isCallStackPred, isCallStackPredTy,
33
34 -- Evidence variables
35 DictId, isEvVar, isDictId
36 ) where
37
38 import GHC.Prelude
39
40 import GHC.Core.Type
41 import GHC.Core.Class
42 import GHC.Core.TyCon
43 import GHC.Core.TyCon.RecWalk
44 import GHC.Types.Var
45 import GHC.Core.Coercion
46 import GHC.Core.Multiplicity ( scaledThing )
47
48 import GHC.Builtin.Names
49 import GHC.Builtin.Types.Prim ( concretePrimTyCon )
50
51 import GHC.Utils.Outputable
52 import GHC.Utils.Misc
53 import GHC.Utils.Panic
54 import GHC.Data.FastString( FastString )
55
56
57 -- | A predicate in the solver. The solver tries to prove Wanted predicates
58 -- from Given ones.
59 data Pred
60
61 -- | A typeclass predicate.
62 = ClassPred Class [Type]
63
64 -- | A type equality predicate.
65 | EqPred EqRel Type Type
66
67 -- | An irreducible predicate.
68 | IrredPred PredType
69
70 -- | A quantified predicate.
71 --
72 -- See Note [Quantified constraints] in GHC.Tc.Solver.Canonical
73 | ForAllPred [TyVar] [PredType] PredType
74
75 -- | A special predicate, used internally in GHC.
76 --
77 -- The meaning of the type argument is dictated by the 'SpecialPred'
78 -- specified in the first agument; see the documentation of 'SpecialPred' for more info.
79 --
80 -- Example: @Concrete# rep@, used for representation-polymorphism checks
81 -- within GHC. See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.
82 -- (This is the only example currently. More to come: see GHC ticket #20000.)
83 | SpecialPred SpecialPred Type
84
85 -- NB: There is no TuplePred case
86 -- Tuple predicates like (Eq a, Ord b) are just treated
87 -- as ClassPred, as if we had a tuple class with two superclasses
88 -- class (c1, c2) => (%,%) c1 c2
89
90 classifyPredType :: PredType -> Pred
91 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
92 Just (tc, [_, _, ty1, ty2])
93 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
94 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
95
96 Just (tc, [_ki, ty])
97 | tc `hasKey` concretePrimTyConKey
98 -> SpecialPred ConcretePrimPred ty
99
100 Just (tc, tys)
101 | Just clas <- tyConClass_maybe tc
102 -> ClassPred clas tys
103
104 _ | (tvs, rho) <- splitForAllTyCoVars ev_ty
105 , (theta, pred) <- splitFunTys rho
106 , not (null tvs && null theta)
107 -> ForAllPred tvs (map scaledThing theta) pred
108
109 | otherwise
110 -> IrredPred ev_ty
111
112 -- --------------------- Dictionary types ---------------------------------
113
114 mkClassPred :: Class -> [Type] -> PredType
115 mkClassPred clas tys = mkTyConApp (classTyCon clas) tys
116
117 isDictTy :: Type -> Bool
118 isDictTy = isClassPred
119
120 getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
121 getClassPredTys ty = case getClassPredTys_maybe ty of
122 Just (clas, tys) -> (clas, tys)
123 Nothing -> pprPanic "getClassPredTys" (ppr ty)
124
125 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
126 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
127 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
128 _ -> Nothing
129
130 classMethodTy :: Id -> Type
131 -- Takes a class selector op :: forall a. C a => meth_ty
132 -- and returns the type of its method, meth_ty
133 -- The selector can be a superclass selector, in which case
134 -- you get back a superclass
135 classMethodTy sel_id
136 = funResultTy $ -- meth_ty
137 dropForAlls $ -- C a => meth_ty
138 varType sel_id -- forall a. C n => meth_ty
139
140 classMethodInstTy :: Id -> [Type] -> Type
141 -- Takes a class selector op :: forall a b. C a b => meth_ty
142 -- and the types [ty1, ty2] at which it is instantiated,
143 -- returns the instantiated type of its method, meth_ty[t1/a,t2/b]
144 -- The selector can be a superclass selector, in which case
145 -- you get back a superclass
146 classMethodInstTy sel_id arg_tys
147 = funResultTy $
148 piResultTys (varType sel_id) arg_tys
149
150 -- --------------------- Equality predicates ---------------------------------
151
152 -- | A choice of equality relation. This is separate from the type 'Role'
153 -- because 'Phantom' does not define a (non-trivial) equality relation.
154 data EqRel = NomEq | ReprEq
155 deriving (Eq, Ord)
156
157 instance Outputable EqRel where
158 ppr NomEq = text "nominal equality"
159 ppr ReprEq = text "representational equality"
160
161 eqRelRole :: EqRel -> Role
162 eqRelRole NomEq = Nominal
163 eqRelRole ReprEq = Representational
164
165 getEqPredTys :: PredType -> (Type, Type)
166 getEqPredTys ty
167 = case splitTyConApp_maybe ty of
168 Just (tc, [_, _, ty1, ty2])
169 | tc `hasKey` eqPrimTyConKey
170 || tc `hasKey` eqReprPrimTyConKey
171 -> (ty1, ty2)
172 _ -> pprPanic "getEqPredTys" (ppr ty)
173
174 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
175 getEqPredTys_maybe ty
176 = case splitTyConApp_maybe ty of
177 Just (tc, [_, _, ty1, ty2])
178 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
179 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
180 _ -> Nothing
181
182 getEqPredRole :: PredType -> Role
183 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
184
185 -- | Get the equality relation relevant for a pred type.
186 predTypeEqRel :: PredType -> EqRel
187 predTypeEqRel ty
188 | Just (tc, _) <- splitTyConApp_maybe ty
189 , tc `hasKey` eqReprPrimTyConKey
190 = ReprEq
191 | otherwise
192 = NomEq
193
194 -- --------------------- Special predicates ----------------------------------
195
196 -- | 'SpecialPred' describes all the special predicates
197 -- that are currently used in GHC.
198 --
199 -- These are different from the special typeclasses
200 -- (such as `KnownNat`, `Typeable`, `Coercible`, ...), as special predicates
201 -- can't be expressed as typeclasses, as they hold evidence of a different kind.
202 data SpecialPred
203 -- | A @Concrete#@ predicate, to check for representation polymorphism.
204 --
205 -- When the first argument to the 'SpecialPred' data constructor of 'Pred'
206 -- is 'ConcretePrimPred', the second argument is the type we are inspecting
207 -- to decide whether it is concrete. That is, it refers to the
208 -- second argument of the 'Concrete#' 'TyCon'. Recall that this 'TyCon' has kind
209 --
210 -- > forall k. k -> TupleRep '[]
211 --
212 -- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete for further details.
213 = ConcretePrimPred
214 deriving stock Eq
215
216 instance Outputable SpecialPred where
217 ppr ConcretePrimPred = text "Concrete#"
218
219 -- | Obtain the 'TyCon' associated with a special predicate.
220 specialPredTyCon :: SpecialPred -> TyCon
221 specialPredTyCon ConcretePrimPred = concretePrimTyCon
222
223 {-------------------------------------------
224 Predicates on PredType
225 --------------------------------------------}
226
227 {-
228 Note [Evidence for quantified constraints]
229 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
230 The superclass mechanism in GHC.Tc.Solver.Canonical.makeSuperClasses risks
231 taking a quantified constraint like
232 (forall a. C a => a ~ b)
233 and generate superclass evidence
234 (forall a. C a => a ~# b)
235
236 This is a funny thing: neither isPredTy nor isCoVarType are true
237 of it. So we are careful not to generate it in the first place:
238 see Note [Equality superclasses in quantified constraints]
239 in GHC.Tc.Solver.Canonical.
240 -}
241
242 isEvVarType :: Type -> Bool
243 -- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
244 -- (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2)
245 -- See Note [Types for coercions, predicates, and evidence] in GHC.Core.TyCo.Rep
246 -- See Note [Evidence for quantified constraints]
247 isEvVarType ty = isCoVarType ty || isPredTy ty
248
249 isEqPredClass :: Class -> Bool
250 -- True of (~) and (~~)
251 isEqPredClass cls = cls `hasKey` eqTyConKey
252 || cls `hasKey` heqTyConKey
253
254 isClassPred, isEqPred, isEqPrimPred :: PredType -> Bool
255 isClassPred ty = case tyConAppTyCon_maybe ty of
256 Just tyCon | isClassTyCon tyCon -> True
257 _ -> False
258
259 isEqPred ty -- True of (a ~ b) and (a ~~ b)
260 -- ToDo: should we check saturation?
261 | Just tc <- tyConAppTyCon_maybe ty
262 , Just cls <- tyConClass_maybe tc
263 = isEqPredClass cls
264 | otherwise
265 = False
266
267 isEqPrimPred ty = isCoVarType ty
268 -- True of (a ~# b) (a ~R# b)
269
270 isCTupleClass :: Class -> Bool
271 isCTupleClass cls = isTupleTyCon (classTyCon cls)
272
273
274 {- *********************************************************************
275 * *
276 Implicit parameters
277 * *
278 ********************************************************************* -}
279
280 isIPTyCon :: TyCon -> Bool
281 isIPTyCon tc = tc `hasKey` ipClassKey
282 -- Class and its corresponding TyCon have the same Unique
283
284 isIPClass :: Class -> Bool
285 isIPClass cls = cls `hasKey` ipClassKey
286
287 isIPLikePred :: Type -> Bool
288 -- See Note [Local implicit parameters]
289 isIPLikePred = is_ip_like_pred initIPRecTc
290
291
292 is_ip_like_pred :: RecTcChecker -> Type -> Bool
293 is_ip_like_pred rec_clss ty
294 | Just (tc, tys) <- splitTyConApp_maybe ty
295 , Just rec_clss' <- if isTupleTyCon tc -- Tuples never cause recursion
296 then Just rec_clss
297 else checkRecTc rec_clss tc
298 , Just cls <- tyConClass_maybe tc
299 = isIPClass cls || has_ip_super_classes rec_clss' cls tys
300
301 | otherwise
302 = False -- Includes things like (D []) where D is
303 -- a Constraint-ranged family; #7785
304
305 hasIPSuperClasses :: Class -> [Type] -> Bool
306 -- See Note [Local implicit parameters]
307 hasIPSuperClasses = has_ip_super_classes initIPRecTc
308
309 has_ip_super_classes :: RecTcChecker -> Class -> [Type] -> Bool
310 has_ip_super_classes rec_clss cls tys
311 = any ip_ish (classSCSelIds cls)
312 where
313 -- Check that the type of a superclass determines its value
314 -- sc_sel_id :: forall a b. C a b -> <superclass type>
315 ip_ish sc_sel_id = is_ip_like_pred rec_clss $
316 classMethodInstTy sc_sel_id tys
317
318 initIPRecTc :: RecTcChecker
319 initIPRecTc = setRecTcMaxBound 1 initRecTc
320
321 -- --------------------- CallStack predicates ---------------------------------
322
323 isCallStackPredTy :: Type -> Bool
324 -- True of HasCallStack, or IP "blah" CallStack
325 isCallStackPredTy ty
326 | Just (tc, tys) <- splitTyConApp_maybe ty
327 , Just cls <- tyConClass_maybe tc
328 , Just {} <- isCallStackPred cls tys
329 = True
330 | otherwise
331 = False
332
333 -- | Is a 'PredType' a 'CallStack' implicit parameter?
334 --
335 -- If so, return the name of the parameter.
336 isCallStackPred :: Class -> [Type] -> Maybe FastString
337 isCallStackPred cls tys
338 | [ty1, ty2] <- tys
339 , isIPClass cls
340 , isCallStackTy ty2
341 = isStrLitTy ty1
342 | otherwise
343 = Nothing
344
345 -- | Is a type a 'CallStack'?
346 isCallStackTy :: Type -> Bool
347 isCallStackTy ty
348 | Just tc <- tyConAppTyCon_maybe ty
349 = tc `hasKey` callStackTyConKey
350 | otherwise
351 = False
352
353
354 {- Note [Local implicit parameters]
355 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
356 The function isIPLikePred tells if this predicate, or any of its
357 superclasses, is an implicit parameter.
358
359 Why are implicit parameters special? Unlike normal classes, we can
360 have local instances for implicit parameters, in the form of
361 let ?x = True in ...
362 So in various places we must be careful not to assume that any value
363 of the right type will do; we must carefully look for the innermost binding.
364 So isIPLikePred checks whether this is an implicit parameter, or has
365 a superclass that is an implicit parameter.
366
367 Several wrinkles
368
369 * We must be careful with superclasses, as #18649 showed. Haskell
370 doesn't allow an implicit parameter as a superclass
371 class (?x::a) => C a where ...
372 but with a constraint tuple we might have
373 (% Eq a, ?x::Int %)
374 and /its/ superclasses, namely (Eq a) and (?x::Int), /do/ include an
375 implicit parameter.
376
377 With ConstraintKinds this can apply to /any/ class, e.g.
378 class sc => C sc where ...
379 Then (C (?x::Int)) has (?x::Int) as a superclass. So we must
380 instantiate and check each superclass, one by one, in
381 hasIPSuperClasses.
382
383 * With -XRecursiveSuperClasses, the superclass hunt can go on forever,
384 so we need a RecTcChecker to cut it off.
385
386 * Another apparent additional complexity involves type families. For
387 example, consider
388 type family D (v::*->*) :: Constraint
389 type instance D [] = ()
390 f :: D v => v Char -> Int
391 If we see a call (f "foo"), we'll pass a "dictionary"
392 () |> (g :: () ~ D [])
393 and it's good to specialise f at this dictionary.
394
395 So the question is: can an implicit parameter "hide inside" a
396 type-family constraint like (D a). Well, no. We don't allow
397 type instance D Maybe = ?x:Int
398 Hence the umbrella 'otherwise' case in is_ip_like_pred. See #7785.
399
400 Small worries (Sept 20):
401 * I don't see what stops us having that 'type instance'. Indeed I
402 think nothing does.
403 * I'm a little concerned about type variables; such a variable might
404 be instantiated to an implicit parameter. I don't think this
405 matters in the cases for which isIPLikePred is used, and it's pretty
406 obscure anyway.
407 * The superclass hunt stops when it encounters the same class again,
408 but in principle we could have the same class, differently instantiated,
409 and the second time it could have an implicit parameter
410 I'm going to treat these as problems for another day. They are all exotic. -}
411
412 {- *********************************************************************
413 * *
414 Evidence variables
415 * *
416 ********************************************************************* -}
417
418 isEvVar :: Var -> Bool
419 isEvVar var = isEvVarType (varType var)
420
421 isDictId :: Id -> Bool
422 isDictId id = isDictTy (varType id)