never executed always true always false
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5 -}
6
7
8 {-# LANGUAGE MultiWayIf #-}
9
10 -- | Functions for inferring (and simplifying) the context for derived instances.
11 module GHC.Tc.Deriv.Infer
12 ( inferConstraints
13 , simplifyInstanceContexts
14 )
15 where
16
17 import GHC.Prelude
18
19 import GHC.Data.Bag
20 import GHC.Types.Basic
21 import GHC.Core.Class
22 import GHC.Core.DataCon
23 import GHC.Utils.Error
24 import GHC.Tc.Utils.Instantiate
25 import GHC.Utils.Outputable
26 import GHC.Utils.Panic
27 import GHC.Utils.Panic.Plain
28 import GHC.Data.Pair
29 import GHC.Builtin.Names
30 import GHC.Tc.Deriv.Utils
31 import GHC.Tc.Utils.Env
32 import GHC.Tc.Deriv.Generate
33 import GHC.Tc.Deriv.Functor
34 import GHC.Tc.Deriv.Generics
35 import GHC.Tc.Utils.TcMType
36 import GHC.Tc.Utils.Monad
37 import GHC.Tc.Types.Origin
38 import GHC.Tc.Types.Constraint
39 import GHC.Core.Predicate
40 import GHC.Tc.Utils.TcType
41 import GHC.Core.TyCon
42 import GHC.Core.TyCo.Ppr (pprTyVars)
43 import GHC.Core.Type
44 import GHC.Tc.Solver
45 import GHC.Tc.Validity (validDerivPred)
46 import GHC.Tc.Utils.Unify (buildImplicationFor, checkConstraints)
47 import GHC.Builtin.Types (typeToTypeKind)
48 import GHC.Core.Unify (tcUnifyTy)
49 import GHC.Utils.Misc
50 import GHC.Types.Var
51 import GHC.Types.Var.Set
52
53 import Control.Monad
54 import Control.Monad.Trans.Class (lift)
55 import Control.Monad.Trans.Reader (ask)
56 import Data.List (sortBy)
57 import Data.Maybe
58
59 ----------------------
60
61 inferConstraints :: DerivSpecMechanism
62 -> DerivM ([ThetaOrigin], [TyVar], [TcType])
63 -- inferConstraints figures out the constraints needed for the
64 -- instance declaration generated by a 'deriving' clause on a
65 -- data type declaration. It also returns the new in-scope type
66 -- variables and instance types, in case they were changed due to
67 -- the presence of functor-like constraints.
68 -- See Note [Inferring the instance context]
69
70 -- e.g. inferConstraints
71 -- C Int (T [a]) -- Class and inst_tys
72 -- :RTList a -- Rep tycon and its arg tys
73 -- where T [a] ~R :RTList a
74 --
75 -- Generate a sufficiently large set of constraints that typechecking the
76 -- generated method definitions should succeed. This set will be simplified
77 -- before being used in the instance declaration
78 inferConstraints mechanism
79 = do { DerivEnv { denv_tvs = tvs
80 , denv_cls = main_cls
81 , denv_inst_tys = inst_tys } <- ask
82 ; wildcard <- isStandaloneWildcardDeriv
83 ; let infer_constraints :: DerivM ([ThetaOrigin], [TyVar], [TcType])
84 infer_constraints =
85 case mechanism of
86 DerivSpecStock{dsm_stock_dit = dit}
87 -> inferConstraintsStock dit
88 DerivSpecAnyClass
89 -> infer_constraints_simple inferConstraintsAnyclass
90 DerivSpecNewtype { dsm_newtype_dit =
91 DerivInstTys{dit_cls_tys = cls_tys}
92 , dsm_newtype_rep_ty = rep_ty }
93 -> infer_constraints_simple $
94 inferConstraintsCoerceBased cls_tys rep_ty
95 DerivSpecVia { dsm_via_cls_tys = cls_tys
96 , dsm_via_ty = via_ty }
97 -> infer_constraints_simple $
98 inferConstraintsCoerceBased cls_tys via_ty
99
100 -- Most deriving strategies do not need to do anything special to
101 -- the type variables and arguments to the class in the derived
102 -- instance, so they can pass through unchanged. The exception to
103 -- this rule is stock deriving. See
104 -- Note [Inferring the instance context].
105 infer_constraints_simple
106 :: DerivM [ThetaOrigin]
107 -> DerivM ([ThetaOrigin], [TyVar], [TcType])
108 infer_constraints_simple infer_thetas = do
109 thetas <- infer_thetas
110 pure (thetas, tvs, inst_tys)
111
112 -- Constraints arising from superclasses
113 -- See Note [Superclasses of derived instance]
114 cls_tvs = classTyVars main_cls
115 sc_constraints = assertPpr (equalLength cls_tvs inst_tys)
116 (ppr main_cls <+> ppr inst_tys)
117 [ mkThetaOrigin (mkDerivOrigin wildcard)
118 TypeLevel [] [] [] $
119 substTheta cls_subst (classSCTheta main_cls) ]
120 cls_subst = assert (equalLength cls_tvs inst_tys) $
121 zipTvSubst cls_tvs inst_tys
122
123 ; (inferred_constraints, tvs', inst_tys') <- infer_constraints
124 ; lift $ traceTc "inferConstraints" $ vcat
125 [ ppr main_cls <+> ppr inst_tys'
126 , ppr inferred_constraints
127 ]
128 ; return ( sc_constraints ++ inferred_constraints
129 , tvs', inst_tys' ) }
130
131 -- | Like 'inferConstraints', but used only in the case of the @stock@ deriving
132 -- strategy. The constraints are inferred by inspecting the fields of each data
133 -- constructor. In this example:
134 --
135 -- > data Foo = MkFoo Int Char deriving Show
136 --
137 -- We would infer the following constraints ('ThetaOrigin's):
138 --
139 -- > (Show Int, Show Char)
140 --
141 -- Note that this function also returns the type variables ('TyVar's) and
142 -- class arguments ('TcType's) for the resulting instance. This is because
143 -- when deriving 'Functor'-like classes, we must sometimes perform kind
144 -- substitutions to ensure the resulting instance is well kinded, which may
145 -- affect the type variables and class arguments. In this example:
146 --
147 -- > newtype Compose (f :: k -> Type) (g :: Type -> k) (a :: Type) =
148 -- > Compose (f (g a)) deriving stock Functor
149 --
150 -- We must unify @k@ with @Type@ in order for the resulting 'Functor' instance
151 -- to be well kinded, so we return @[]@/@[Type, f, g]@ for the
152 -- 'TyVar's/'TcType's, /not/ @[k]@/@[k, f, g]@.
153 -- See Note [Inferring the instance context].
154 inferConstraintsStock :: DerivInstTys
155 -> DerivM ([ThetaOrigin], [TyVar], [TcType])
156 inferConstraintsStock (DerivInstTys { dit_cls_tys = cls_tys
157 , dit_tc = tc
158 , dit_tc_args = tc_args
159 , dit_rep_tc = rep_tc
160 , dit_rep_tc_args = rep_tc_args })
161 = do DerivEnv { denv_tvs = tvs
162 , denv_cls = main_cls
163 , denv_inst_tys = inst_tys } <- ask
164 wildcard <- isStandaloneWildcardDeriv
165
166 let inst_ty = mkTyConApp tc tc_args
167 tc_binders = tyConBinders rep_tc
168 choose_level bndr
169 | isNamedTyConBinder bndr = KindLevel
170 | otherwise = TypeLevel
171 t_or_ks = map choose_level tc_binders ++ repeat TypeLevel
172 -- want to report *kind* errors when possible
173
174 -- Constraints arising from the arguments of each constructor
175 con_arg_constraints
176 :: (CtOrigin -> TypeOrKind
177 -> Type
178 -> [([PredOrigin], Maybe TCvSubst)])
179 -> ([ThetaOrigin], [TyVar], [TcType])
180 con_arg_constraints get_arg_constraints
181 = let (predss, mbSubsts) = unzip
182 [ preds_and_mbSubst
183 | data_con <- tyConDataCons rep_tc
184 , (arg_n, arg_t_or_k, arg_ty)
185 <- zip3 [1..] t_or_ks $
186 dataConInstOrigArgTys data_con all_rep_tc_args
187 -- No constraints for unlifted types
188 -- See Note [Deriving and unboxed types]
189 , not (isUnliftedType (irrelevantMult arg_ty))
190 , let orig = DerivOriginDC data_con arg_n wildcard
191 , preds_and_mbSubst
192 <- get_arg_constraints orig arg_t_or_k (irrelevantMult arg_ty)
193 ]
194 preds = concat predss
195 -- If the constraints require a subtype to be of kind
196 -- (* -> *) (which is the case for functor-like
197 -- constraints), then we explicitly unify the subtype's
198 -- kinds with (* -> *).
199 -- See Note [Inferring the instance context]
200 subst = foldl' composeTCvSubst
201 emptyTCvSubst (catMaybes mbSubsts)
202 unmapped_tvs = filter (\v -> v `notElemTCvSubst` subst
203 && not (v `isInScope` subst)) tvs
204 (subst', _) = substTyVarBndrs subst unmapped_tvs
205 preds' = map (substPredOrigin subst') preds
206 inst_tys' = substTys subst' inst_tys
207 tvs' = tyCoVarsOfTypesWellScoped inst_tys'
208 in ([mkThetaOriginFromPreds preds'], tvs', inst_tys')
209
210 is_generic = main_cls `hasKey` genClassKey
211 is_generic1 = main_cls `hasKey` gen1ClassKey
212 -- is_functor_like: see Note [Inferring the instance context]
213 is_functor_like = tcTypeKind inst_ty `tcEqKind` typeToTypeKind
214 || is_generic1
215
216 get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
217 -> [([PredOrigin], Maybe TCvSubst)]
218 get_gen1_constraints functor_cls orig t_or_k ty
219 = mk_functor_like_constraints orig t_or_k functor_cls $
220 get_gen1_constrained_tys last_tv ty
221
222 get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type
223 -> [([PredOrigin], Maybe TCvSubst)]
224 get_std_constrained_tys orig t_or_k ty
225 | is_functor_like
226 = mk_functor_like_constraints orig t_or_k main_cls $
227 deepSubtypesContaining last_tv ty
228 | otherwise
229 = [( [mk_cls_pred orig t_or_k main_cls ty]
230 , Nothing )]
231
232 mk_functor_like_constraints :: CtOrigin -> TypeOrKind
233 -> Class -> [Type]
234 -> [([PredOrigin], Maybe TCvSubst)]
235 -- 'cls' is usually main_cls (Functor or Traversable etc), but if
236 -- main_cls = Generic1, then 'cls' can be Functor; see
237 -- get_gen1_constraints
238 --
239 -- For each type, generate two constraints,
240 -- [cls ty, kind(ty) ~ (*->*)], and a kind substitution that results
241 -- from unifying kind(ty) with * -> *. If the unification is
242 -- successful, it will ensure that the resulting instance is well
243 -- kinded. If not, the second constraint will result in an error
244 -- message which points out the kind mismatch.
245 -- See Note [Inferring the instance context]
246 mk_functor_like_constraints orig t_or_k cls
247 = map $ \ty -> let ki = tcTypeKind ty in
248 ( [ mk_cls_pred orig t_or_k cls ty
249 , mkPredOrigin orig KindLevel
250 (mkPrimEqPred ki typeToTypeKind) ]
251 , tcUnifyTy ki typeToTypeKind
252 )
253
254 rep_tc_tvs = tyConTyVars rep_tc
255 last_tv = last rep_tc_tvs
256 -- When we first gather up the constraints to solve, most of them
257 -- contain rep_tc_tvs, i.e., the type variables from the derived
258 -- datatype's type constructor. We don't want these type variables
259 -- to appear in the final instance declaration, so we must
260 -- substitute each type variable with its counterpart in the derived
261 -- instance. rep_tc_args lists each of these counterpart types in
262 -- the same order as the type variables.
263 all_rep_tc_args = tyConInstArgTys rep_tc rep_tc_args
264
265 -- Stupid constraints
266 stupid_constraints
267 = [ mkThetaOrigin deriv_origin TypeLevel [] [] [] $
268 substTheta tc_subst (tyConStupidTheta rep_tc) ]
269 tc_subst = -- See the comment with all_rep_tc_args for an
270 -- explanation of this assertion
271 assert (equalLength rep_tc_tvs all_rep_tc_args) $
272 zipTvSubst rep_tc_tvs all_rep_tc_args
273
274 -- Extra Data constraints
275 -- The Data class (only) requires that for
276 -- instance (...) => Data (T t1 t2)
277 -- IF t1:*, t2:*
278 -- THEN (Data t1, Data t2) are among the (...) constraints
279 -- Reason: when the IF holds, we generate a method
280 -- dataCast2 f = gcast2 f
281 -- and we need the Data constraints to typecheck the method
282 extra_constraints = [mkThetaOriginFromPreds constrs]
283 where
284 constrs
285 | main_cls `hasKey` dataClassKey
286 , all (isLiftedTypeKind . tcTypeKind) rep_tc_args
287 = [ mk_cls_pred deriv_origin t_or_k main_cls ty
288 | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
289 | otherwise
290 = []
291
292 mk_cls_pred orig t_or_k cls ty
293 -- Don't forget to apply to cls_tys' too
294 = mkPredOrigin orig t_or_k (mkClassPred cls (cls_tys' ++ [ty]))
295 cls_tys' | is_generic1 = []
296 -- In the awkward Generic1 case, cls_tys' should be
297 -- empty, since we are applying the class Functor.
298
299 | otherwise = cls_tys
300
301 deriv_origin = mkDerivOrigin wildcard
302
303 if -- Generic constraints are easy
304 | is_generic
305 -> return ([], tvs, inst_tys)
306
307 -- Generic1 needs Functor
308 -- See Note [Getting base classes]
309 | is_generic1
310 -> assert (rep_tc_tvs `lengthExceeds` 0) $
311 -- Generic1 has a single kind variable
312 assert (cls_tys `lengthIs` 1) $
313 do { functorClass <- lift $ tcLookupClass functorClassName
314 ; pure $ con_arg_constraints
315 $ get_gen1_constraints functorClass }
316
317 -- The others are a bit more complicated
318 | otherwise
319 -> -- See the comment with all_rep_tc_args for an explanation of
320 -- this assertion
321 assertPpr (equalLength rep_tc_tvs all_rep_tc_args)
322 ( ppr main_cls <+> ppr rep_tc
323 $$ ppr rep_tc_tvs $$ ppr all_rep_tc_args) $
324 do { let (arg_constraints, tvs', inst_tys')
325 = con_arg_constraints get_std_constrained_tys
326 ; lift $ traceTc "inferConstraintsStock" $ vcat
327 [ ppr main_cls <+> ppr inst_tys'
328 , ppr arg_constraints
329 ]
330 ; return ( stupid_constraints ++ extra_constraints
331 ++ arg_constraints
332 , tvs', inst_tys') }
333
334 -- | Like 'inferConstraints', but used only in the case of @DeriveAnyClass@,
335 -- which gathers its constraints based on the type signatures of the class's
336 -- methods instead of the types of the data constructor's field.
337 --
338 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
339 -- for an explanation of how these constraints are used to determine the
340 -- derived instance context.
341 inferConstraintsAnyclass :: DerivM [ThetaOrigin]
342 inferConstraintsAnyclass
343 = do { DerivEnv { denv_cls = cls
344 , denv_inst_tys = inst_tys } <- ask
345 ; wildcard <- isStandaloneWildcardDeriv
346
347 ; let gen_dms = [ (sel_id, dm_ty)
348 | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ]
349
350 cls_tvs = classTyVars cls
351
352 do_one_meth :: (Id, Type) -> TcM ThetaOrigin
353 -- (Id,Type) are the selector Id and the generic default method type
354 -- NB: the latter is /not/ quantified over the class variables
355 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
356 do_one_meth (sel_id, gen_dm_ty)
357 = do { let (sel_tvs, _cls_pred, meth_ty)
358 = tcSplitMethodTy (varType sel_id)
359 meth_ty' = substTyWith sel_tvs inst_tys meth_ty
360 (meth_tvs, meth_theta, meth_tau)
361 = tcSplitNestedSigmaTys meth_ty'
362
363 gen_dm_ty' = substTyWith cls_tvs inst_tys gen_dm_ty
364 (dm_tvs, dm_theta, dm_tau)
365 = tcSplitNestedSigmaTys gen_dm_ty'
366 tau_eq = mkPrimEqPred meth_tau dm_tau
367 ; return (mkThetaOrigin (mkDerivOrigin wildcard) TypeLevel
368 meth_tvs dm_tvs meth_theta (tau_eq:dm_theta)) }
369
370 ; lift $ mapM do_one_meth gen_dms }
371
372 -- Like 'inferConstraints', but used only for @GeneralizedNewtypeDeriving@ and
373 -- @DerivingVia@. Since both strategies generate code involving 'coerce', the
374 -- inferred constraints set up the scaffolding needed to typecheck those uses
375 -- of 'coerce'. In this example:
376 --
377 -- > newtype Age = MkAge Int deriving newtype Num
378 --
379 -- We would infer the following constraints ('ThetaOrigin's):
380 --
381 -- > (Num Int, Coercible Age Int)
382 inferConstraintsCoerceBased :: [Type] -> Type
383 -> DerivM [ThetaOrigin]
384 inferConstraintsCoerceBased cls_tys rep_ty = do
385 DerivEnv { denv_tvs = tvs
386 , denv_cls = cls
387 , denv_inst_tys = inst_tys } <- ask
388 sa_wildcard <- isStandaloneWildcardDeriv
389 let -- The following functions are polymorphic over the representation
390 -- type, since we might either give it the underlying type of a
391 -- newtype (for GeneralizedNewtypeDeriving) or a @via@ type
392 -- (for DerivingVia).
393 rep_tys ty = cls_tys ++ [ty]
394 rep_pred ty = mkClassPred cls (rep_tys ty)
395 rep_pred_o ty = mkPredOrigin deriv_origin TypeLevel (rep_pred ty)
396 -- rep_pred is the representation dictionary, from where
397 -- we are going to get all the methods for the final
398 -- dictionary
399 deriv_origin = mkDerivOrigin sa_wildcard
400
401 -- Next we collect constraints for the class methods
402 -- If there are no methods, we don't need any constraints
403 -- Otherwise we need (C rep_ty), for the representation methods,
404 -- and constraints to coerce each individual method
405 meth_preds :: Type -> [PredOrigin]
406 meth_preds ty
407 | null meths = [] -- No methods => no constraints
408 -- (#12814)
409 | otherwise = rep_pred_o ty : coercible_constraints ty
410 meths = classMethods cls
411 coercible_constraints ty
412 = [ mkPredOrigin (DerivOriginCoerce meth t1 t2 sa_wildcard)
413 TypeLevel (mkReprPrimEqPred t1 t2)
414 | meth <- meths
415 , let (Pair t1 t2) = mkCoerceClassMethEqn cls tvs
416 inst_tys ty meth ]
417
418 all_thetas :: Type -> [ThetaOrigin]
419 all_thetas ty = [mkThetaOriginFromPreds $ meth_preds ty]
420
421 pure (all_thetas rep_ty)
422
423 {- Note [Inferring the instance context]
424 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
425 There are two sorts of 'deriving', as represented by the two constructors
426 for DerivContext:
427
428 * InferContext mb_wildcard: This can either be:
429 - The deriving clause for a data type.
430 (e.g, data T a = T1 a deriving( Eq ))
431 In this case, mb_wildcard = Nothing.
432 - A standalone declaration with an extra-constraints wildcard
433 (e.g., deriving instance _ => Eq (Foo a))
434 In this case, mb_wildcard = Just loc, where loc is the location
435 of the extra-constraints wildcard.
436
437 Here we must infer an instance context,
438 and generate instance declaration
439 instance Eq a => Eq (T a) where ...
440
441 * SupplyContext theta: standalone deriving
442 deriving instance Eq a => Eq (T a)
443 Here we only need to fill in the bindings;
444 the instance context (theta) is user-supplied
445
446 For the InferContext case, we must figure out the
447 instance context (inferConstraintsStock). Suppose we are inferring
448 the instance context for
449 C t1 .. tn (T s1 .. sm)
450 There are two cases
451
452 * (T s1 .. sm) :: * (the normal case)
453 Then we behave like Eq and guess (C t1 .. tn t)
454 for each data constructor arg of type t. More
455 details below.
456
457 * (T s1 .. sm) :: * -> * (the functor-like case)
458 Then we behave like Functor.
459
460 In both cases we produce a bunch of un-simplified constraints
461 and them simplify them in simplifyInstanceContexts; see
462 Note [Simplifying the instance context].
463
464 In the functor-like case, we may need to unify some kind variables with * in
465 order for the generated instance to be well-kinded. An example from #10524:
466
467 newtype Compose (f :: k2 -> *) (g :: k1 -> k2) (a :: k1)
468 = Compose (f (g a)) deriving Functor
469
470 Earlier in the deriving pipeline, GHC unifies the kind of Compose f g
471 (k1 -> *) with the kind of Functor's argument (* -> *), so k1 := *. But this
472 alone isn't enough, since k2 wasn't unified with *:
473
474 instance (Functor (f :: k2 -> *), Functor (g :: * -> k2)) =>
475 Functor (Compose f g) where ...
476
477 The two Functor constraints are ill-kinded. To ensure this doesn't happen, we:
478
479 1. Collect all of a datatype's subtypes which require functor-like
480 constraints.
481 2. For each subtype, create a substitution by unifying the subtype's kind
482 with (* -> *).
483 3. Compose all the substitutions into one, then apply that substitution to
484 all of the in-scope type variables and the instance types.
485
486 Note [Getting base classes]
487 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
488 Functor and Typeable are defined in package 'base', and that is not available
489 when compiling 'ghc-prim'. So we must be careful that 'deriving' for stuff in
490 ghc-prim does not use Functor or Typeable implicitly via these lookups.
491
492 Note [Deriving and unboxed types]
493 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
494 We have some special hacks to support things like
495 data T = MkT Int# deriving ( Show )
496
497 Specifically, we use GHC.Tc.Deriv.Generate.box to box the Int# into an Int
498 (which we know how to show), and append a '#'. Parentheses are not required
499 for unboxed values (`MkT -3#` is a valid expression).
500
501 Note [Superclasses of derived instance]
502 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
503 In general, a derived instance decl needs the superclasses of the derived
504 class too. So if we have
505 data T a = ...deriving( Ord )
506 then the initial context for Ord (T a) should include Eq (T a). Often this is
507 redundant; we'll also generate an Ord constraint for each constructor argument,
508 and that will probably generate enough constraints to make the Eq (T a) constraint
509 be satisfied too. But not always; consider:
510
511 data S a = S
512 instance Eq (S a)
513 instance Ord (S a)
514
515 data T a = MkT (S a) deriving( Ord )
516 instance Num a => Eq (T a)
517
518 The derived instance for (Ord (T a)) must have a (Num a) constraint!
519 Similarly consider:
520 data T a = MkT deriving( Data )
521 Here there *is* no argument field, but we must nevertheless generate
522 a context for the Data instances:
523 instance Typeable a => Data (T a) where ...
524
525
526 ************************************************************************
527 * *
528 Finding the fixed point of deriving equations
529 * *
530 ************************************************************************
531
532 Note [Simplifying the instance context]
533 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
534 Consider
535
536 data T a b = C1 (Foo a) (Bar b)
537 | C2 Int (T b a)
538 | C3 (T a a)
539 deriving (Eq)
540
541 We want to come up with an instance declaration of the form
542
543 instance (Ping a, Pong b, ...) => Eq (T a b) where
544 x == y = ...
545
546 It is pretty easy, albeit tedious, to fill in the code "...". The
547 trick is to figure out what the context for the instance decl is,
548 namely Ping, Pong and friends.
549
550 Let's call the context reqd for the T instance of class C at types
551 (a,b, ...) C (T a b). Thus:
552
553 Eq (T a b) = (Ping a, Pong b, ...)
554
555 Now we can get a (recursive) equation from the data decl. This part
556 is done by inferConstraintsStock.
557
558 Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1
559 u Eq (T b a) u Eq Int -- From C2
560 u Eq (T a a) -- From C3
561
562
563 Foo and Bar may have explicit instances for Eq, in which case we can
564 just substitute for them. Alternatively, either or both may have
565 their Eq instances given by deriving clauses, in which case they
566 form part of the system of equations.
567
568 Now all we need do is simplify and solve the equations, iterating to
569 find the least fixpoint. This is done by simplifyInstanceConstraints.
570 Notice that the order of the arguments can
571 switch around, as here in the recursive calls to T.
572
573 Let's suppose Eq (Foo a) = Eq a, and Eq (Bar b) = Ping b.
574
575 We start with:
576
577 Eq (T a b) = {} -- The empty set
578
579 Next iteration:
580 Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1
581 u Eq (T b a) u Eq Int -- From C2
582 u Eq (T a a) -- From C3
583
584 After simplification:
585 = Eq a u Ping b u {} u {} u {}
586 = Eq a u Ping b
587
588 Next iteration:
589
590 Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1
591 u Eq (T b a) u Eq Int -- From C2
592 u Eq (T a a) -- From C3
593
594 After simplification:
595 = Eq a u Ping b
596 u (Eq b u Ping a)
597 u (Eq a u Ping a)
598
599 = Eq a u Ping b u Eq b u Ping a
600
601 The next iteration gives the same result, so this is the fixpoint. We
602 need to make a canonical form of the RHS to ensure convergence. We do
603 this by simplifying the RHS to a form in which
604
605 - the classes constrain only tyvars
606 - the list is sorted by tyvar (major key) and then class (minor key)
607 - no duplicates, of course
608
609 Note [Deterministic simplifyInstanceContexts]
610 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
611 Canonicalisation uses nonDetCmpType which is nondeterministic. Sorting
612 with nonDetCmpType puts the returned lists in a nondeterministic order.
613 If we were to return them, we'd get class constraints in
614 nondeterministic order.
615
616 Consider:
617
618 data ADT a b = Z a b deriving Eq
619
620 The generated code could be either:
621
622 instance (Eq a, Eq b) => Eq (Z a b) where
623
624 Or:
625
626 instance (Eq b, Eq a) => Eq (Z a b) where
627
628 To prevent the order from being nondeterministic we only
629 canonicalize when comparing and return them in the same order as
630 simplifyDeriv returned them.
631 See also Note [nonDetCmpType nondeterminism]
632 -}
633
634
635 simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]]
636 -> TcM [DerivSpec ThetaType]
637 -- Used only for deriving clauses or standalone deriving with an
638 -- extra-constraints wildcard (InferContext)
639 -- See Note [Simplifying the instance context]
640
641 simplifyInstanceContexts [] = return []
642
643 simplifyInstanceContexts infer_specs
644 = do { traceTc "simplifyInstanceContexts" $ vcat (map pprDerivSpec infer_specs)
645 ; iterate_deriv 1 initial_solutions }
646 where
647 ------------------------------------------------------------------
648 -- The initial solutions for the equations claim that each
649 -- instance has an empty context; this solution is certainly
650 -- in canonical form.
651 initial_solutions :: [ThetaType]
652 initial_solutions = [ [] | _ <- infer_specs ]
653
654 ------------------------------------------------------------------
655 -- iterate_deriv calculates the next batch of solutions,
656 -- compares it with the current one; finishes if they are the
657 -- same, otherwise recurses with the new solutions.
658 -- It fails if any iteration fails
659 iterate_deriv :: Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
660 iterate_deriv n current_solns
661 | n > 20 -- Looks as if we are in an infinite loop
662 -- This can happen if we have -XUndecidableInstances
663 -- (See GHC.Tc.Solver.tcSimplifyDeriv.)
664 = pprPanic "solveDerivEqns: probable loop"
665 (vcat (map pprDerivSpec infer_specs) $$ ppr current_solns)
666 | otherwise
667 = do { -- Extend the inst info from the explicit instance decls
668 -- with the current set of solutions, and simplify each RHS
669 inst_specs <- zipWithM newDerivClsInst current_solns infer_specs
670 ; new_solns <- checkNoErrs $
671 extendLocalInstEnv inst_specs $
672 mapM gen_soln infer_specs
673
674 ; if (current_solns `eqSolution` new_solns) then
675 return [ spec { ds_theta = soln }
676 | (spec, soln) <- zip infer_specs current_solns ]
677 else
678 iterate_deriv (n+1) new_solns }
679
680 eqSolution a b = eqListBy (eqListBy eqType) (canSolution a) (canSolution b)
681 -- Canonicalise for comparison
682 -- See Note [Deterministic simplifyInstanceContexts]
683 canSolution = map (sortBy nonDetCmpType)
684 ------------------------------------------------------------------
685 gen_soln :: DerivSpec [ThetaOrigin] -> TcM ThetaType
686 gen_soln (DS { ds_loc = loc, ds_tvs = tyvars
687 , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
688 = setSrcSpan loc $
689 addErrCtxt (derivInstCtxt the_pred) $
690 do { theta <- simplifyDeriv the_pred tyvars deriv_rhs
691 -- checkValidInstance tyvars theta clas inst_tys
692 -- Not necessary; see Note [Exotic derived instance contexts]
693
694 ; traceTc "GHC.Tc.Deriv" (ppr deriv_rhs $$ ppr theta)
695 -- Claim: the result instance declaration is guaranteed valid
696 -- Hence no need to call:
697 -- checkValidInstance tyvars theta clas inst_tys
698 ; return theta }
699 where
700 the_pred = mkClassPred clas inst_tys
701
702 derivInstCtxt :: PredType -> SDoc
703 derivInstCtxt pred
704 = text "When deriving the instance for" <+> parens (ppr pred)
705
706 {-
707 ***********************************************************************************
708 * *
709 * Simplify derived constraints
710 * *
711 ***********************************************************************************
712 -}
713
714 -- | Given @instance (wanted) => C inst_ty@, simplify 'wanted' as much
715 -- as possible. Fail if not possible.
716 simplifyDeriv :: PredType -- ^ @C inst_ty@, head of the instance we are
717 -- deriving. Only used for SkolemInfo.
718 -> [TyVar] -- ^ The tyvars bound by @inst_ty@.
719 -> [ThetaOrigin] -- ^ Given and wanted constraints
720 -> TcM ThetaType -- ^ Needed constraints (after simplification),
721 -- i.e. @['PredType']@.
722 simplifyDeriv pred tvs thetas
723 = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
724 -- The constraint solving machinery
725 -- expects *TcTyVars* not TyVars.
726 -- We use *non-overlappable* (vanilla) skolems
727 -- See Note [Overlap and deriving]
728
729 ; let skol_set = mkVarSet tvs_skols
730 skol_info = DerivSkol pred
731 doc = text "deriving" <+> parens (ppr pred)
732
733 mk_given_ev :: PredType -> TcM EvVar
734 mk_given_ev given =
735 let given_pred = substTy skol_subst given
736 in newEvVar given_pred
737
738 emit_wanted_constraints :: [TyVar] -> [PredOrigin] -> TcM ()
739 emit_wanted_constraints metas_to_be preds
740 = do { -- We instantiate metas_to_be with fresh meta type
741 -- variables. Currently, these can only be type variables
742 -- quantified in generic default type signatures.
743 -- See Note [Gathering and simplifying constraints for
744 -- DeriveAnyClass]
745 (meta_subst, _meta_tvs) <- newMetaTyVars metas_to_be
746
747 -- Now make a constraint for each of the instantiated predicates
748 ; let wanted_subst = skol_subst `unionTCvSubst` meta_subst
749 mk_wanted_ct (PredOrigin wanted orig t_or_k)
750 = do { ev <- newWanted orig (Just t_or_k) $
751 substTyUnchecked wanted_subst wanted
752 ; return (mkNonCanonical ev) }
753 ; cts <- mapM mk_wanted_ct preds
754
755 -- And emit them into the monad
756 ; emitSimples (listToCts cts) }
757
758 -- Create the implications we need to solve. For stock and newtype
759 -- deriving, these implication constraints will be simple class
760 -- constraints like (C a, Ord b).
761 -- But with DeriveAnyClass, we make an implication constraint.
762 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
763 mk_wanteds :: ThetaOrigin -> TcM WantedConstraints
764 mk_wanteds (ThetaOrigin { to_anyclass_skols = ac_skols
765 , to_anyclass_metas = ac_metas
766 , to_anyclass_givens = ac_givens
767 , to_wanted_origins = preds })
768 = do { ac_given_evs <- mapM mk_given_ev ac_givens
769 ; (_, wanteds)
770 <- captureConstraints $
771 checkConstraints skol_info ac_skols ac_given_evs $
772 -- The checkConstraints bumps the TcLevel, and
773 -- wraps the wanted constraints in an implication,
774 -- when (but only when) necessary
775 emit_wanted_constraints ac_metas preds
776 ; pure wanteds }
777
778 -- See [STEP DAC BUILD]
779 -- Generate the implication constraints, one for each method, to solve
780 -- with the skolemized variables. Start "one level down" because
781 -- we are going to wrap the result in an implication with tvs_skols,
782 -- in step [DAC RESIDUAL]
783 ; (tc_lvl, wanteds) <- pushTcLevelM $
784 mapM mk_wanteds thetas
785
786 ; traceTc "simplifyDeriv inputs" $
787 vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ]
788
789 -- See [STEP DAC SOLVE]
790 -- Simplify the constraints, starting at the same level at which
791 -- they are generated (c.f. the call to runTcSWithEvBinds in
792 -- simplifyInfer)
793 ; solved_wanteds <- setTcLevel tc_lvl $
794 runTcSDeriveds $
795 solveWantedsAndDrop $
796 unionsWC wanteds
797
798 -- It's not yet zonked! Obviously zonk it before peering at it
799 ; solved_wanteds <- zonkWC solved_wanteds
800
801 -- See [STEP DAC HOIST]
802 -- From the simplified constraints extract a subset 'good' that will
803 -- become the context 'min_theta' for the derived instance.
804 ; let residual_simple = approximateWC True solved_wanteds
805 good = mapMaybeBag get_good residual_simple
806
807 -- Returns @Just p@ (where @p@ is the type of the Ct) if a Ct is
808 -- suitable to be inferred in the context of a derived instance.
809 -- Returns @Nothing@ if the Ct is too exotic.
810 -- See Note [Exotic derived instance contexts] for what
811 -- constitutes an exotic constraint.
812 get_good :: Ct -> Maybe PredType
813 get_good ct | validDerivPred skol_set p
814 , isWantedCt ct
815 = Just p
816 -- TODO: This is wrong
817 -- NB re 'isWantedCt': residual_wanted may contain
818 -- unsolved CtDerived and we stick them into the
819 -- bad set so that reportUnsolved may decide what
820 -- to do with them
821 | otherwise
822 = Nothing
823 where p = ctPred ct
824
825 ; traceTc "simplifyDeriv outputs" $
826 vcat [ ppr tvs_skols, ppr residual_simple, ppr good ]
827
828 -- Return the good unsolved constraints (unskolemizing on the way out.)
829 ; let min_theta = mkMinimalBySCs id (bagToList good)
830 -- An important property of mkMinimalBySCs (used above) is that in
831 -- addition to removing constraints that are made redundant by
832 -- superclass relationships, it also removes _duplicate_
833 -- constraints.
834 -- See Note [Gathering and simplifying constraints for
835 -- DeriveAnyClass]
836 subst_skol = zipTvSubst tvs_skols $ mkTyVarTys tvs
837 -- The reverse substitution (sigh)
838
839 -- See [STEP DAC RESIDUAL]
840 -- Ensure that min_theta is enough to solve /all/ the constraints in
841 -- solved_wanteds, by solving the implication constraint
842 --
843 -- forall tvs. min_theta => solved_wanteds
844 ; min_theta_vars <- mapM newEvVar min_theta
845 ; (leftover_implic, _)
846 <- buildImplicationFor tc_lvl skol_info tvs_skols
847 min_theta_vars solved_wanteds
848 -- This call to simplifyTop is purely for error reporting
849 -- See Note [Error reporting for deriving clauses]
850 -- See also Note [Exotic derived instance contexts], which are caught
851 -- in this line of code.
852 ; simplifyTopImplic leftover_implic
853
854 ; return (substTheta subst_skol min_theta) }
855
856 {-
857 Note [Overlap and deriving]
858 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
859 Consider some overlapping instances:
860 instance Show a => Show [a] where ..
861 instance Show [Char] where ...
862
863 Now a data type with deriving:
864 data T a = MkT [a] deriving( Show )
865
866 We want to get the derived instance
867 instance Show [a] => Show (T a) where...
868 and NOT
869 instance Show a => Show (T a) where...
870 so that the (Show (T Char)) instance does the Right Thing
871
872 It's very like the situation when we're inferring the type
873 of a function
874 f x = show [x]
875 and we want to infer
876 f :: Show [a] => a -> String
877
878 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
879 the context for the derived instance.
880 Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
881
882 Note [Gathering and simplifying constraints for DeriveAnyClass]
883 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
884 DeriveAnyClass works quite differently from stock and newtype deriving in
885 the way it gathers and simplifies constraints to be used in a derived
886 instance's context. Stock and newtype deriving gather constraints by looking
887 at the data constructors of the data type for which we are deriving an
888 instance. But DeriveAnyClass doesn't need to know about a data type's
889 definition at all!
890
891 To see why, consider this example of DeriveAnyClass:
892
893 class Foo a where
894 bar :: forall b. Ix b => a -> b -> String
895 default bar :: (Show a, Ix c) => a -> c -> String
896 bar x y = show x ++ show (range (y,y))
897
898 baz :: Eq a => a -> a -> Bool
899 default baz :: (Ord a, Show a) => a -> a -> Bool
900 baz x y = compare x y == EQ
901
902 Because 'bar' and 'baz' have default signatures, this generates a top-level
903 definition for these generic default methods
904
905 $gdm_bar :: forall a. Foo a
906 => forall c. (Show a, Ix c)
907 => a -> c -> String
908 $gdm_bar x y = show x ++ show (range (y,y))
909
910 (and similarly for baz). Now consider a 'deriving' clause
911 data Maybe s = ... deriving Foo
912
913 This derives an instance of the form:
914 instance (CX) => Foo (Maybe s) where
915 bar = $gdm_bar
916 baz = $gdm_baz
917
918 Now it is GHC's job to fill in a suitable instance context (CX). If
919 GHC were typechecking the binding
920 bar = $gdm bar
921 it would
922 * skolemise the expected type of bar
923 * instantiate the type of $gdm_bar with meta-type variables
924 * build an implication constraint
925
926 [STEP DAC BUILD]
927 So that's what we do. We build the constraint (call it C1)
928
929 forall[2] b. Ix b => (Show (Maybe s), Ix cc,
930 Maybe s -> b -> String
931 ~ Maybe s -> cc -> String)
932
933 Here:
934 * The level of this forall constraint is forall[2], because we are later
935 going to wrap it in a forall[1] in [STEP DAC RESIDUAL]
936
937 * The 'b' comes from the quantified type variable in the expected type
938 of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
939 variable that comes from instantiating the quantified type variable 'c' in
940 $gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
941
942 * The (Ix b) constraint comes from the context of bar's type
943 (i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc)
944 constraints come from the context of $gdm_bar's type
945 (i.e., 'to_anyclass_givens' in 'ThetaOrigin').
946
947 * The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String)
948 comes from marrying up the instantiated type of $gdm_bar with the specified
949 type of bar. Notice that the type variables from the instance, 's' in this
950 case, are global to this constraint.
951
952 Note that it is vital that we instantiate the `c` in $gdm_bar's type with a new
953 unification variable for each iteration of simplifyDeriv. If we re-use the same
954 unification variable across multiple iterations, then bad things can happen,
955 such as #14933.
956
957 Similarly for 'baz', giving the constraint C2
958
959 forall[2]. Eq (Maybe s) => (Ord a, Show a,
960 Maybe s -> Maybe s -> Bool
961 ~ Maybe s -> Maybe s -> Bool)
962
963 In this case baz has no local quantification, so the implication
964 constraint has no local skolems and there are no unification
965 variables.
966
967 [STEP DAC SOLVE]
968 We can combine these two implication constraints into a single
969 constraint (C1, C2), and simplify, unifying cc:=b, to get:
970
971 forall[2] b. Ix b => Show a
972 /\
973 forall[2]. Eq (Maybe s) => (Ord a, Show a)
974
975 [STEP DAC HOIST]
976 Let's call that (C1', C2'). Now we need to hoist the unsolved
977 constraints out of the implications to become our candidate for
978 (CX). That is done by approximateWC, which will return:
979
980 (Show a, Ord a, Show a)
981
982 Now we can use mkMinimalBySCs to remove superclasses and duplicates, giving
983
984 (Show a, Ord a)
985
986 And that's what GHC uses for CX.
987
988 [STEP DAC RESIDUAL]
989 In this case we have solved all the leftover constraints, but what if
990 we don't? Simple! We just form the final residual constraint
991
992 forall[1] s. CX => (C1',C2')
993
994 and simplify that. In simple cases it'll succeed easily, because CX
995 literally contains the constraints in C1', C2', but if there is anything
996 more complicated it will be reported in a civilised way.
997
998 Note [Error reporting for deriving clauses]
999 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1000 A surprisingly tricky aspect of deriving to get right is reporting sensible
1001 error messages. In particular, if simplifyDeriv reaches a constraint that it
1002 cannot solve, which might include:
1003
1004 1. Insoluble constraints
1005 2. "Exotic" constraints (See Note [Exotic derived instance contexts])
1006
1007 Then we report an error immediately in simplifyDeriv.
1008
1009 Another possible choice is to punt and let another part of the typechecker
1010 (e.g., simplifyInstanceContexts) catch the errors. But this tends to lead
1011 to worse error messages, so we do it directly in simplifyDeriv.
1012
1013 simplifyDeriv checks for errors in a clever way. If the deriving machinery
1014 infers the context (Foo a)--that is, if this instance is to be generated:
1015
1016 instance Foo a => ...
1017
1018 Then we form an implication of the form:
1019
1020 forall a. Foo a => <residual_wanted_constraints>
1021
1022 And pass it to the simplifier. If the context (Foo a) is enough to discharge
1023 all the constraints in <residual_wanted_constraints>, then everything is
1024 hunky-dory. But if <residual_wanted_constraints> contains, say, an insoluble
1025 constraint, then (Foo a) won't be able to solve it, causing GHC to error.
1026
1027 Note [Exotic derived instance contexts]
1028 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1029 In a 'derived' instance declaration, we *infer* the context. It's a
1030 bit unclear what rules we should apply for this; the Haskell report is
1031 silent. Obviously, constraints like (Eq a) are fine, but what about
1032 data T f a = MkT (f a) deriving( Eq )
1033 where we'd get an Eq (f a) constraint. That's probably fine too.
1034
1035 One could go further: consider
1036 data T a b c = MkT (Foo a b c) deriving( Eq )
1037 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
1038
1039 Notice that this instance (just) satisfies the Paterson termination
1040 conditions. Then we *could* derive an instance decl like this:
1041
1042 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
1043 even though there is no instance for (C Int a), because there just
1044 *might* be an instance for, say, (C Int Bool) at a site where we
1045 need the equality instance for T's.
1046
1047 However, this seems pretty exotic, and it's quite tricky to allow
1048 this, and yet give sensible error messages in the (much more common)
1049 case where we really want that instance decl for C.
1050
1051 So for now we simply require that the derived instance context
1052 should have only type-variable constraints.
1053
1054 Here is another example:
1055 data Fix f = In (f (Fix f)) deriving( Eq )
1056 Here, if we are prepared to allow -XUndecidableInstances we
1057 could derive the instance
1058 instance Eq (f (Fix f)) => Eq (Fix f)
1059 but this is so delicate that I don't think it should happen inside
1060 'deriving'. If you want this, write it yourself!
1061
1062 NB: if you want to lift this condition, make sure you still meet the
1063 termination conditions! If not, the deriving mechanism generates
1064 larger and larger constraints. Example:
1065 data Succ a = S a
1066 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
1067
1068 Note the lack of a Show instance for Succ. First we'll generate
1069 instance (Show (Succ a), Show a) => Show (Seq a)
1070 and then
1071 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
1072 and so on. Instead we want to complain of no instance for (Show (Succ a)).
1073
1074 The bottom line
1075 ~~~~~~~~~~~~~~~
1076 Allow constraints which consist only of type variables, with no repeats.
1077 -}