Refactor DeriveAnyClass's instance context inference
[ghc.git] / compiler / typecheck / TcDerivInfer.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Functions for inferring (and simplifying) the context for derived instances.
7 -}
8
9 {-# LANGUAGE CPP #-}
10
11 module TcDerivInfer (inferConstraints, simplifyInstanceContexts) where
12
13 #include "HsVersions.h"
14
15 import Bag
16 import BasicTypes
17 import Class
18 import DataCon
19 -- import DynFlags
20 import ErrUtils
21 import Inst
22 import Outputable
23 import PrelNames
24 import TcDerivUtils
25 import TcEnv
26 -- import TcErrors (reportAllUnsolved)
27 import TcGenFunctor
28 import TcGenGenerics
29 import TcMType
30 import TcRnMonad
31 import TcType
32 import TyCon
33 import Type
34 import TcSimplify
35 import TcValidity (validDerivPred)
36 import TcUnify (buildImplicationFor)
37 import Unify (tcMatchTy, tcUnifyTy)
38 import Util
39 import Var
40 import VarEnv
41 import VarSet
42
43 import Control.Monad
44 import Data.List
45 import Data.Maybe
46
47 ----------------------
48
49 inferConstraints :: [TyVar] -> Class -> [TcType] -> TcType
50 -> TyCon -> [TcType] -> DerivSpecMechanism
51 -> ([ThetaOrigin] -> [TyVar] -> [TcType] -> TcM a)
52 -> TcM a
53 -- inferConstraints figures out the constraints needed for the
54 -- instance declaration generated by a 'deriving' clause on a
55 -- data type declaration. It also returns the new in-scope type
56 -- variables and instance types, in case they were changed due to
57 -- the presence of functor-like constraints.
58 -- See Note [Inferring the instance context]
59
60 -- e.g. inferConstraints
61 -- C Int (T [a]) -- Class and inst_tys
62 -- :RTList a -- Rep tycon and its arg tys
63 -- where T [a] ~R :RTList a
64 --
65 -- Generate a sufficiently large set of constraints that typechecking the
66 -- generated method definitions should succeed. This set will be simplified
67 -- before being used in the instance declaration
68 inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args
69 mechanism thing
70 | is_generic && not is_anyclass -- Generic constraints are easy
71 = thing [mkThetaOriginFromPreds []] tvs inst_tys
72
73 | is_generic1 && not is_anyclass -- Generic1 needs Functor
74 = ASSERT( length rep_tc_tvs > 0 ) -- See Note [Getting base classes]
75 ASSERT( length cls_tys == 1 ) -- Generic1 has a single kind variable
76 do { functorClass <- tcLookupClass functorClassName
77 ; con_arg_constraints (get_gen1_constraints functorClass) thing }
78
79 | otherwise -- The others are a bit more complicated
80 = -- See the comment with all_rep_tc_args for an explanation of
81 -- this assertion
82 ASSERT2( equalLength rep_tc_tvs all_rep_tc_args
83 , ppr main_cls <+> ppr rep_tc
84 $$ ppr rep_tc_tvs $$ ppr all_rep_tc_args )
85 infer_constraints $ \arg_constraints tvs' inst_tys' ->
86 do { traceTc "inferConstraints" $ vcat
87 [ ppr main_cls <+> ppr inst_tys'
88 , ppr arg_constraints
89 ]
90 ; thing (stupid_constraints ++ extra_constraints
91 ++ sc_constraints ++ arg_constraints)
92 tvs' inst_tys' }
93 where
94 is_anyclass = isDerivSpecAnyClass mechanism
95 infer_constraints
96 | is_anyclass = inferConstraintsDAC main_cls tvs inst_tys
97 | otherwise = con_arg_constraints get_std_constrained_tys
98
99 tc_binders = tyConBinders rep_tc
100 choose_level bndr
101 | isNamedTyConBinder bndr = KindLevel
102 | otherwise = TypeLevel
103 t_or_ks = map choose_level tc_binders ++ repeat TypeLevel
104 -- want to report *kind* errors when possible
105
106 -- Constraints arising from the arguments of each constructor
107 con_arg_constraints :: (CtOrigin -> TypeOrKind
108 -> Type
109 -> [([PredOrigin], Maybe TCvSubst)])
110 -> ([ThetaOrigin] -> [TyVar] -> [TcType] -> TcM a)
111 -> TcM a
112 con_arg_constraints get_arg_constraints thing
113 = let (predss, mbSubsts) = unzip
114 [ preds_and_mbSubst
115 | data_con <- tyConDataCons rep_tc
116 , (arg_n, arg_t_or_k, arg_ty)
117 <- zip3 [1..] t_or_ks $
118 dataConInstOrigArgTys data_con all_rep_tc_args
119 -- No constraints for unlifted types
120 -- See Note [Deriving and unboxed types]
121 , not (isUnliftedType arg_ty)
122 , let orig = DerivOriginDC data_con arg_n
123 , preds_and_mbSubst <- get_arg_constraints orig arg_t_or_k arg_ty
124 ]
125 preds = concat predss
126 -- If the constraints require a subtype to be of kind (* -> *)
127 -- (which is the case for functor-like constraints), then we
128 -- explicitly unify the subtype's kinds with (* -> *).
129 -- See Note [Inferring the instance context]
130 subst = foldl' composeTCvSubst
131 emptyTCvSubst (catMaybes mbSubsts)
132 unmapped_tvs = filter (\v -> v `notElemTCvSubst` subst
133 && not (v `isInScope` subst)) tvs
134 (subst', _) = mapAccumL substTyVarBndr subst unmapped_tvs
135 preds' = map (substPredOrigin subst') preds
136 inst_tys' = substTys subst' inst_tys
137 tvs' = tyCoVarsOfTypesWellScoped inst_tys'
138 in thing [mkThetaOriginFromPreds preds'] tvs' inst_tys'
139
140 is_generic = main_cls `hasKey` genClassKey
141 is_generic1 = main_cls `hasKey` gen1ClassKey
142 -- is_functor_like: see Note [Inferring the instance context]
143 is_functor_like = typeKind inst_ty `tcEqKind` typeToTypeKind
144 || is_generic1
145
146 get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
147 -> [([PredOrigin], Maybe TCvSubst)]
148 get_gen1_constraints functor_cls orig t_or_k ty
149 = mk_functor_like_constraints orig t_or_k functor_cls $
150 get_gen1_constrained_tys last_tv ty
151
152 get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type
153 -> [([PredOrigin], Maybe TCvSubst)]
154 get_std_constrained_tys orig t_or_k ty
155 | is_functor_like = mk_functor_like_constraints orig t_or_k main_cls $
156 deepSubtypesContaining last_tv ty
157 | otherwise = [( [mk_cls_pred orig t_or_k main_cls ty]
158 , Nothing )]
159
160 mk_functor_like_constraints :: CtOrigin -> TypeOrKind
161 -> Class -> [Type]
162 -> [([PredOrigin], Maybe TCvSubst)]
163 -- 'cls' is usually main_cls (Functor or Traversable etc), but if
164 -- main_cls = Generic1, then 'cls' can be Functor; see get_gen1_constraints
165 --
166 -- For each type, generate two constraints, [cls ty, kind(ty) ~ (*->*)],
167 -- and a kind substitution that results from unifying kind(ty) with * -> *.
168 -- If the unification is successful, it will ensure that the resulting
169 -- instance is well kinded. If not, the second constraint will result
170 -- in an error message which points out the kind mismatch.
171 -- See Note [Inferring the instance context]
172 mk_functor_like_constraints orig t_or_k cls
173 = map $ \ty -> let ki = typeKind ty in
174 ( [ mk_cls_pred orig t_or_k cls ty
175 , mkPredOrigin orig KindLevel
176 (mkPrimEqPred ki typeToTypeKind) ]
177 , tcUnifyTy ki typeToTypeKind
178 )
179
180 rep_tc_tvs = tyConTyVars rep_tc
181 last_tv = last rep_tc_tvs
182 -- When we first gather up the constraints to solve, most of them contain
183 -- rep_tc_tvs, i.e., the type variables from the derived datatype's type
184 -- constructor. We don't want these type variables to appear in the final
185 -- instance declaration, so we must substitute each type variable with its
186 -- counterpart in the derived instance. rep_tc_args lists each of these
187 -- counterpart types in the same order as the type variables.
188 all_rep_tc_args = rep_tc_args ++ map mkTyVarTy
189 (drop (length rep_tc_args) rep_tc_tvs)
190
191 -- Constraints arising from superclasses
192 -- See Note [Superclasses of derived instance]
193 cls_tvs = classTyVars main_cls
194 inst_tys = cls_tys ++ [inst_ty]
195 sc_constraints = ASSERT2( equalLength cls_tvs inst_tys, ppr main_cls <+> ppr rep_tc)
196 [ mkThetaOrigin DerivOrigin TypeLevel [] [] $
197 substTheta cls_subst (classSCTheta main_cls) ]
198 cls_subst = ASSERT( equalLength cls_tvs inst_tys )
199 zipTvSubst cls_tvs inst_tys
200
201 -- Stupid constraints
202 stupid_constraints = [ mkThetaOrigin DerivOrigin TypeLevel [] [] $
203 substTheta tc_subst (tyConStupidTheta rep_tc) ]
204 tc_subst = -- See the comment with all_rep_tc_args for an explanation of
205 -- this assertion
206 ASSERT( equalLength rep_tc_tvs all_rep_tc_args )
207 zipTvSubst rep_tc_tvs all_rep_tc_args
208
209 -- Extra Data constraints
210 -- The Data class (only) requires that for
211 -- instance (...) => Data (T t1 t2)
212 -- IF t1:*, t2:*
213 -- THEN (Data t1, Data t2) are among the (...) constraints
214 -- Reason: when the IF holds, we generate a method
215 -- dataCast2 f = gcast2 f
216 -- and we need the Data constraints to typecheck the method
217 extra_constraints = [mkThetaOriginFromPreds constrs]
218 where
219 constrs
220 | main_cls `hasKey` dataClassKey
221 , all (isLiftedTypeKind . typeKind) rep_tc_args
222 = [ mk_cls_pred DerivOrigin t_or_k main_cls ty
223 | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
224 | otherwise
225 = []
226
227 mk_cls_pred orig t_or_k cls ty -- Don't forget to apply to cls_tys' too
228 = mkPredOrigin orig t_or_k (mkClassPred cls (cls_tys' ++ [ty]))
229 cls_tys' | is_generic1 = [] -- In the awkward Generic1 case, cls_tys'
230 -- should be empty, since we are applying the
231 -- class Functor.
232 | otherwise = cls_tys
233
234 typeToTypeKind :: Kind
235 typeToTypeKind = liftedTypeKind `mkFunTy` liftedTypeKind
236
237 -- | Like 'inferConstraints', but used only in the case of @DeriveAnyClass@,
238 -- which gathers its constraints based on the type signatures of the class's
239 -- methods instead of the types of the data constructor's field.
240 --
241 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
242 -- for an explanation of how these constraints are used to determine the
243 -- derived instance context.
244 inferConstraintsDAC :: Class -> [TyVar] -> [TcType]
245 -> ([ThetaOrigin] -> [TyVar] -> [TcType] -> TcM a)
246 -> TcM a
247 inferConstraintsDAC cls tvs inst_tys thing =
248 let theta_origins
249 = [ mkThetaOrigin DerivOrigin TypeLevel dm_tvs vanilla_theta' dm_theta'
250 | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls
251 , let vanilla_ty = thdOf3 $ tcSplitMethodTy (varType sel_id)
252 -- See Note [Splitting nested sigma types] in TcTyClsDecls
253 (_, vanilla_theta, vanilla_tau)
254 = tcSplitNestedSigmaTys vanilla_ty
255 (dm_tvs, dm_theta, dm_tau)
256 = tcSplitNestedSigmaTys dm_ty
257
258 -- The class will start out like:
259 --
260 -- class Foo a where
261 -- bar :: a -> String
262 -- default :: Show a => a -> String
263 --
264 -- If we are anyclass-deriving an instance for, say,
265 -- data Wibble, then we want to collect a (Show Wibble)
266 -- constraint, not a (Show a) constraint! So we must first
267 -- substitute the instantiated types into the default type
268 -- signature (e.g., a |-> Wibble).
269 in_scope = mkInScopeSet $ tyCoVarsOfTypes
270 $ mkTyVarTys dm_tvs ++ inst_tys
271 tv_env = zipVarEnv (classTyVars cls) inst_tys
272 subst = mkTvSubst in_scope tv_env
273 dm_theta' = substTheta subst dm_theta
274 dm_tau' = substTy subst dm_tau
275
276 -- The next obstacle to overcome is the fact that the default
277 -- and non-default type signatures scope over different sets of
278 -- type variables. That is, this imagine that this is the
279 -- class you were anyclass-deriving:
280 --
281 -- class Baz f where
282 -- quux :: forall a. Eq a => f a -> f a -> Bool
283 -- default quux :: forall b. (Eq b, Show b)
284 -- => f b -> f b -> Bool
285 --
286 -- We need a way to treat `a` and `b` as the same when
287 -- typechecking a derived Baz instance. So to wrap
288 -- up inferConstraintsDAC, we match up the non-default type
289 -- type signature with the default one, and apply the resulting
290 -- substitution to the non-default type signature.
291 mb_dm_subst = tcMatchTy vanilla_tau dm_tau'
292 -- We can be assured that we'll always get a substitution here
293 -- (i.e., that the type signatures always match up), since we
294 -- checked for this property earlier in checkValidClass.
295 -- See Note [Default method type signatures must align]
296 -- in TcTyClsDecls.
297 dm_subst = fromMaybe
298 (pprPanic "inferConstraintsDAC" $
299 vcat [ text "vanilla_tau" <+> ppr vanilla_tau
300 , text "dm_tau'" <+> ppr dm_tau' ])
301 mb_dm_subst
302 vanilla_theta' = substTheta dm_subst vanilla_theta ]
303 in thing theta_origins tvs inst_tys
304
305 {-
306 Note [Inferring the instance context]
307 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
308 There are two sorts of 'deriving':
309
310 * InferTheta: the deriving clause for a data type
311 data T a = T1 a deriving( Eq )
312 Here we must infer an instance context,
313 and generate instance declaration
314 instance Eq a => Eq (T a) where ...
315
316 * CheckTheta: standalone deriving
317 deriving instance Eq a => Eq (T a)
318 Here we only need to fill in the bindings;
319 the instance context is user-supplied
320
321 For a deriving clause (InferTheta) we must figure out the
322 instance context (inferConstraints). Suppose we are inferring
323 the instance context for
324 C t1 .. tn (T s1 .. sm)
325 There are two cases
326
327 * (T s1 .. sm) :: * (the normal case)
328 Then we behave like Eq and guess (C t1 .. tn t)
329 for each data constructor arg of type t. More
330 details below.
331
332 * (T s1 .. sm) :: * -> * (the functor-like case)
333 Then we behave like Functor.
334
335 In both cases we produce a bunch of un-simplified constraints
336 and them simplify them in simplifyInstanceContexts; see
337 Note [Simplifying the instance context].
338
339 In the functor-like case, we may need to unify some kind variables with * in
340 order for the generated instance to be well-kinded. An example from
341 Trac #10524:
342
343 newtype Compose (f :: k2 -> *) (g :: k1 -> k2) (a :: k1)
344 = Compose (f (g a)) deriving Functor
345
346 Earlier in the deriving pipeline, GHC unifies the kind of Compose f g
347 (k1 -> *) with the kind of Functor's argument (* -> *), so k1 := *. But this
348 alone isn't enough, since k2 wasn't unified with *:
349
350 instance (Functor (f :: k2 -> *), Functor (g :: * -> k2)) =>
351 Functor (Compose f g) where ...
352
353 The two Functor constraints are ill-kinded. To ensure this doesn't happen, we:
354
355 1. Collect all of a datatype's subtypes which require functor-like
356 constraints.
357 2. For each subtype, create a substitution by unifying the subtype's kind
358 with (* -> *).
359 3. Compose all the substitutions into one, then apply that substitution to
360 all of the in-scope type variables and the instance types.
361
362 Note [Getting base classes]
363 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
364 Functor and Typeable are defined in package 'base', and that is not available
365 when compiling 'ghc-prim'. So we must be careful that 'deriving' for stuff in
366 ghc-prim does not use Functor or Typeable implicitly via these lookups.
367
368 Note [Deriving and unboxed types]
369 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
370 We have some special hacks to support things like
371 data T = MkT Int# deriving ( Show )
372
373 Specifically, we use TcGenDeriv.box to box the Int# into an Int
374 (which we know how to show), and append a '#'. Parenthesis are not required
375 for unboxed values (`MkT -3#` is a valid expression).
376
377 Note [Superclasses of derived instance]
378 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
379 In general, a derived instance decl needs the superclasses of the derived
380 class too. So if we have
381 data T a = ...deriving( Ord )
382 then the initial context for Ord (T a) should include Eq (T a). Often this is
383 redundant; we'll also generate an Ord constraint for each constructor argument,
384 and that will probably generate enough constraints to make the Eq (T a) constraint
385 be satisfied too. But not always; consider:
386
387 data S a = S
388 instance Eq (S a)
389 instance Ord (S a)
390
391 data T a = MkT (S a) deriving( Ord )
392 instance Num a => Eq (T a)
393
394 The derived instance for (Ord (T a)) must have a (Num a) constraint!
395 Similarly consider:
396 data T a = MkT deriving( Data )
397 Here there *is* no argument field, but we must nevertheless generate
398 a context for the Data instances:
399 instance Typeable a => Data (T a) where ...
400
401 ************************************************************************
402 * *
403 Finding the fixed point of deriving equations
404 * *
405 ************************************************************************
406
407 Note [Simplifying the instance context]
408 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
409 Consider
410
411 data T a b = C1 (Foo a) (Bar b)
412 | C2 Int (T b a)
413 | C3 (T a a)
414 deriving (Eq)
415
416 We want to come up with an instance declaration of the form
417
418 instance (Ping a, Pong b, ...) => Eq (T a b) where
419 x == y = ...
420
421 It is pretty easy, albeit tedious, to fill in the code "...". The
422 trick is to figure out what the context for the instance decl is,
423 namely Ping, Pong and friends.
424
425 Let's call the context reqd for the T instance of class C at types
426 (a,b, ...) C (T a b). Thus:
427
428 Eq (T a b) = (Ping a, Pong b, ...)
429
430 Now we can get a (recursive) equation from the data decl. This part
431 is done by inferConstraints.
432
433 Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1
434 u Eq (T b a) u Eq Int -- From C2
435 u Eq (T a a) -- From C3
436
437
438 Foo and Bar may have explicit instances for Eq, in which case we can
439 just substitute for them. Alternatively, either or both may have
440 their Eq instances given by deriving clauses, in which case they
441 form part of the system of equations.
442
443 Now all we need do is simplify and solve the equations, iterating to
444 find the least fixpoint. This is done by simplifyInstanceConstraints.
445 Notice that the order of the arguments can
446 switch around, as here in the recursive calls to T.
447
448 Let's suppose Eq (Foo a) = Eq a, and Eq (Bar b) = Ping b.
449
450 We start with:
451
452 Eq (T a b) = {} -- The empty set
453
454 Next iteration:
455 Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1
456 u Eq (T b a) u Eq Int -- From C2
457 u Eq (T a a) -- From C3
458
459 After simplification:
460 = Eq a u Ping b u {} u {} u {}
461 = Eq a u Ping b
462
463 Next iteration:
464
465 Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1
466 u Eq (T b a) u Eq Int -- From C2
467 u Eq (T a a) -- From C3
468
469 After simplification:
470 = Eq a u Ping b
471 u (Eq b u Ping a)
472 u (Eq a u Ping a)
473
474 = Eq a u Ping b u Eq b u Ping a
475
476 The next iteration gives the same result, so this is the fixpoint. We
477 need to make a canonical form of the RHS to ensure convergence. We do
478 this by simplifying the RHS to a form in which
479
480 - the classes constrain only tyvars
481 - the list is sorted by tyvar (major key) and then class (minor key)
482 - no duplicates, of course
483
484 Note [Deterministic simplifyInstanceContexts]
485 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
486 Canonicalisation uses nonDetCmpType which is nondeterministic. Sorting
487 with nonDetCmpType puts the returned lists in a nondeterministic order.
488 If we were to return them, we'd get class constraints in
489 nondeterministic order.
490
491 Consider:
492
493 data ADT a b = Z a b deriving Eq
494
495 The generated code could be either:
496
497 instance (Eq a, Eq b) => Eq (Z a b) where
498
499 Or:
500
501 instance (Eq b, Eq a) => Eq (Z a b) where
502
503 To prevent the order from being nondeterministic we only
504 canonicalize when comparing and return them in the same order as
505 simplifyDeriv returned them.
506 See also Note [nonDetCmpType nondeterminism]
507 -}
508
509
510 simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]]
511 -> TcM [DerivSpec ThetaType]
512 -- Used only for deriving clauses (InferTheta)
513 -- not for standalone deriving
514 -- See Note [Simplifying the instance context]
515
516 simplifyInstanceContexts [] = return []
517
518 simplifyInstanceContexts infer_specs
519 = do { traceTc "simplifyInstanceContexts" $ vcat (map pprDerivSpec infer_specs)
520 ; iterate_deriv 1 initial_solutions }
521 where
522 ------------------------------------------------------------------
523 -- The initial solutions for the equations claim that each
524 -- instance has an empty context; this solution is certainly
525 -- in canonical form.
526 initial_solutions :: [ThetaType]
527 initial_solutions = [ [] | _ <- infer_specs ]
528
529 ------------------------------------------------------------------
530 -- iterate_deriv calculates the next batch of solutions,
531 -- compares it with the current one; finishes if they are the
532 -- same, otherwise recurses with the new solutions.
533 -- It fails if any iteration fails
534 iterate_deriv :: Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
535 iterate_deriv n current_solns
536 | n > 20 -- Looks as if we are in an infinite loop
537 -- This can happen if we have -XUndecidableInstances
538 -- (See TcSimplify.tcSimplifyDeriv.)
539 = pprPanic "solveDerivEqns: probable loop"
540 (vcat (map pprDerivSpec infer_specs) $$ ppr current_solns)
541 | otherwise
542 = do { -- Extend the inst info from the explicit instance decls
543 -- with the current set of solutions, and simplify each RHS
544 inst_specs <- zipWithM newDerivClsInst current_solns infer_specs
545 ; new_solns <- checkNoErrs $
546 extendLocalInstEnv inst_specs $
547 mapM gen_soln infer_specs
548
549 ; if (current_solns `eqSolution` new_solns) then
550 return [ spec { ds_theta = soln }
551 | (spec, soln) <- zip infer_specs current_solns ]
552 else
553 iterate_deriv (n+1) new_solns }
554
555 eqSolution a b = eqListBy (eqListBy eqType) (canSolution a) (canSolution b)
556 -- Canonicalise for comparison
557 -- See Note [Deterministic simplifyInstanceContexts]
558 canSolution = map (sortBy nonDetCmpType)
559 ------------------------------------------------------------------
560 gen_soln :: DerivSpec [ThetaOrigin] -> TcM ThetaType
561 gen_soln (DS { ds_loc = loc, ds_tvs = tyvars
562 , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
563 = setSrcSpan loc $
564 addErrCtxt (derivInstCtxt the_pred) $
565 do { theta <- simplifyDeriv the_pred tyvars deriv_rhs
566 -- checkValidInstance tyvars theta clas inst_tys
567 -- Not necessary; see Note [Exotic derived instance contexts]
568
569 ; traceTc "TcDeriv" (ppr deriv_rhs $$ ppr theta)
570 -- Claim: the result instance declaration is guaranteed valid
571 -- Hence no need to call:
572 -- checkValidInstance tyvars theta clas inst_tys
573 ; return theta }
574 where
575 the_pred = mkClassPred clas inst_tys
576
577 derivInstCtxt :: PredType -> MsgDoc
578 derivInstCtxt pred
579 = text "When deriving the instance for" <+> parens (ppr pred)
580
581 {-
582 ***********************************************************************************
583 * *
584 * Simplify derived constraints
585 * *
586 ***********************************************************************************
587 -}
588
589 -- | Given @instance (wanted) => C inst_ty@, simplify 'wanted' as much
590 -- as possible. Fail if not possible.
591 simplifyDeriv :: PredType -- ^ @C inst_ty@, head of the instance we are
592 -- deriving. Only used for SkolemInfo.
593 -> [TyVar] -- ^ The tyvars bound by @inst_ty@.
594 -> [ThetaOrigin] -- ^ Given and wanted constraints
595 -> TcM ThetaType -- ^ Needed constraints (after simplification),
596 -- i.e. @['PredType']@.
597 simplifyDeriv pred tvs thetas
598 = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
599 -- The constraint solving machinery
600 -- expects *TcTyVars* not TyVars.
601 -- We use *non-overlappable* (vanilla) skolems
602 -- See Note [Overlap and deriving]
603
604 ; let skol_set = mkVarSet tvs_skols
605 skol_info = DerivSkol pred
606 doc = text "deriving" <+> parens (ppr pred)
607
608 mk_given_ev :: PredType -> TcM EvVar
609 mk_given_ev given =
610 let given_pred = substTy skol_subst given
611 in newEvVar given_pred
612
613 mk_wanted_ct :: PredOrigin -> TcM CtEvidence
614 mk_wanted_ct (PredOrigin wanted o t_or_k)
615 = newWanted o (Just t_or_k) (substTyUnchecked skol_subst wanted)
616
617 -- Create the implications we need to solve. For stock and newtype
618 -- deriving, these implication constraints will all be of the form
619 --
620 -- forall . () => <wanted_cts>
621 --
622 -- But with DeriveAnyClass, there might be given constraints as
623 -- well.
624 -- See Note [Gathering and simplifying constraints for
625 -- DeriveAnyClass]
626 mk_implics :: ThetaOrigin -> TcM (Bag Implication)
627 mk_implics (ThetaOrigin { to_tvs = local_tvs
628 , to_givens = givens
629 , to_wanted_origins = wanteds }) = do
630 ((given_evs, wanted_cts), tclvl) <- pushTcLevelM $ do
631 given_cts <- mapM mk_given_ev givens
632 wanted_cts <- mapM mk_wanted_ct wanteds
633 pure (given_cts, wanted_cts)
634 (implic, _) <- buildImplicationFor tclvl skol_info local_tvs
635 given_evs (mkSimpleWC wanted_cts)
636 pure implic
637
638 -- Generate the implication constraints constraints to solve with the
639 -- skolemized variables
640 ; (implics, tclvl) <- pushTcLevelM $ mapM mk_implics thetas
641
642 ; traceTc "simplifyDeriv inputs" $
643 vcat [ pprTyVars tvs $$ ppr thetas $$ ppr implics, doc ]
644 -- Simplify the constraints
645 ; solved_implics <- runTcSDeriveds $ solveWantedsAndDrop
646 $ mkImplicWC
647 $ unionManyBags implics
648
649 -- Split the resulting constraints into bad and good constraints,
650 -- building an @unsolved :: WantedConstraints@ representing all
651 -- the constraints we can't just shunt to the predicates.
652 -- See Note [Exotic derived instance contexts]
653 ; let residual_simple = approximateWC True solved_implics
654 (bad, good) = partitionBagWith get_good residual_simple
655
656 get_good :: Ct -> Either Ct PredType
657 get_good ct | validDerivPred skol_set p
658 , isWantedCt ct
659 = Right p
660 -- TODO: This is wrong
661 -- NB re 'isWantedCt': residual_wanted may contain
662 -- unsolved CtDerived and we stick them into the
663 -- bad set so that reportUnsolved may decide what
664 -- to do with them
665 | otherwise
666 = Left ct
667 where p = ctPred ct
668
669 ; traceTc "simplifyDeriv outputs" $
670 vcat [ ppr tvs_skols, ppr residual_simple, ppr good, ppr bad ]
671
672 -- Return the good unsolved constraints (unskolemizing on the way out.)
673 ; let min_theta = mkMinimalBySCs (bagToList good)
674 -- An important property of mkMinimalBySCs (used above) is that in
675 -- addition to removing constraints that are made redundant by
676 -- superclass relationships, it also removes _duplicate_
677 -- constraints.
678 -- See Note [Gathering and simplifying constraints for
679 -- DeriveAnyClass]
680 subst_skol = zipTvSubst tvs_skols $ mkTyVarTys tvs
681 -- The reverse substitution (sigh)
682
683 ; min_theta_vars <- mapM newEvVar min_theta
684 ; (leftover_implic, _) <- buildImplicationFor tclvl skol_info tvs_skols
685 min_theta_vars solved_implics
686 -- This call to simplifyTop is purely for error reporting
687 -- See Note [Error reporting for deriving clauses]
688 -- See also Note [Exotic derived instance contexts], which are caught
689 -- in this line of code.
690 ; _ <- simplifyTop $ mkImplicWC leftover_implic
691
692 ; return (substTheta subst_skol min_theta) }
693
694 {-
695 Note [Overlap and deriving]
696 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
697 Consider some overlapping instances:
698 data Show a => Show [a] where ..
699 data Show [Char] where ...
700
701 Now a data type with deriving:
702 data T a = MkT [a] deriving( Show )
703
704 We want to get the derived instance
705 instance Show [a] => Show (T a) where...
706 and NOT
707 instance Show a => Show (T a) where...
708 so that the (Show (T Char)) instance does the Right Thing
709
710 It's very like the situation when we're inferring the type
711 of a function
712 f x = show [x]
713 and we want to infer
714 f :: Show [a] => a -> String
715
716 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
717 the context for the derived instance.
718 Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
719
720 Note [Gathering and simplifying constraints for DeriveAnyClass]
721 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
722 DeriveAnyClass works quite differently from stock and newtype deriving in
723 the way it gathers and simplifies constraints to be used in a derived
724 instance's context. Stock and newtype deriving gather constraints by looking
725 at the data constructors of the data type for which we are deriving an
726 instance. But DeriveAnyClass doesn't need to know about a data type's
727 definition at all!
728
729 To see why, picture this example example of DeriveAnyClass:
730
731 data Maybe a = ... deriving Foo
732
733 class Foo a where
734 bar :: Ix b => a -> b -> String
735 default bar :: (Show a, Ix b) => a -> b -> String
736 bar x _ = show x
737
738 baz :: Eq a => a -> a -> Bool
739 default baz :: (Ord a, Show a) => a -> a -> Bool
740 baz x y = compare x y == EQ
741
742 This derives an instance of the form:
743
744 instance ??? => Foo (Maybe a)
745
746 Because bar and baz have default signatures, GHC fills them in under the hood:
747
748 instance ??? => Foo (Maybe a) where
749 bar = $gdm_bar
750 baz = $gdm_baz
751
752 $gdm_bar :: Show a => a -> String
753 $gdm_bar = show
754
755 $gdm_baz :: (Ord a, Show a) => a -> a -> Bool
756 $gdm_baz x y = compare x y == EQ
757
758 Now it is GHC's job to fill in a suitable ??? (the instance context). It does
759 so by simplifying two sets of constraints: the constraints from the default
760 type signatures (the wanted constraints), and the constraints from the
761 non-default type signatures (the given constraints, which can be used to
762 help further simplify the wanted constraints):
763
764 bar: (Givens: [Ix b], Wanteds: [Show (Maybe a), Ix b])
765 baz: (Givens: [Eq (Maybe a)], Wanteds: [Ord (Maybe a), Show (Maybe a)])
766
767 These are just implication constraints. We can combine them into a single
768 constraint:
769
770 (forall b. Ix b => (Show (Maybe a), Ix b))
771 /\
772 (forall . Eq (Maybe a) => (Ord (Maybe a), Show (Maybe a)))
773
774 After simplification, you get:
775
776 (forall b. Ix b => Show a)
777 /\
778 (forall . Eq (Maybe a) => (Ord a, Show a))
779
780 Now we need to hoist these constraints out of the implications to become our
781 candidate for ???. That is done by approximateWC, which will return:
782
783 (Show a, Ord a, Show a)
784
785 Now we can use mkMinimalBySCs to remove superclasses and duplicates, giving
786
787 (Show a, Ord a)
788
789 And that's what GHC uses for ???.
790
791 Note [Error reporting for deriving clauses]
792 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
793 A suprisingly tricky aspect of deriving to get right is reporting sensible
794 error messages. In particular, if simplifyDeriv reaches a constraint that it
795 cannot solve, which might include:
796
797 1. Insoluble constraints
798 2. "Exotic" constraints (See Note [Exotic derived instance contexts])
799
800 Then we report an error immediately in simplifyDeriv.
801
802 Another possible choice is to punt and let another part of the typechecker
803 (e.g., simplifyInstanceContexts) catch the errors. But this tends to lead
804 to worse error messages, so we do it directly in simplifyDeriv.
805
806 simplifyDeriv checks for errors in a clever way. If the deriving machinery
807 infers the context (Foo a)--that is, if this instance is to be generated:
808
809 instance Foo a => ...
810
811 Then we form an implication of the form:
812
813 forall a. Foo a => <residual_wanted_constraints>
814
815 And pass it to the simplifier. If the context (Foo a) is enough to discharge
816 all the constraints in <residual_wanted_constraints>, then everything is
817 hunky-dory. But if <residual_wanted_constraints> contains, say, an insoluble
818 constraint, then (Foo a) won't be able to solve it, causing GHC to error.
819
820 Note [Exotic derived instance contexts]
821 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
822 In a 'derived' instance declaration, we *infer* the context. It's a
823 bit unclear what rules we should apply for this; the Haskell report is
824 silent. Obviously, constraints like (Eq a) are fine, but what about
825 data T f a = MkT (f a) deriving( Eq )
826 where we'd get an Eq (f a) constraint. That's probably fine too.
827
828 One could go further: consider
829 data T a b c = MkT (Foo a b c) deriving( Eq )
830 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
831
832 Notice that this instance (just) satisfies the Paterson termination
833 conditions. Then we *could* derive an instance decl like this:
834
835 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
836 even though there is no instance for (C Int a), because there just
837 *might* be an instance for, say, (C Int Bool) at a site where we
838 need the equality instance for T's.
839
840 However, this seems pretty exotic, and it's quite tricky to allow
841 this, and yet give sensible error messages in the (much more common)
842 case where we really want that instance decl for C.
843
844 So for now we simply require that the derived instance context
845 should have only type-variable constraints.
846
847 Here is another example:
848 data Fix f = In (f (Fix f)) deriving( Eq )
849 Here, if we are prepared to allow -XUndecidableInstances we
850 could derive the instance
851 instance Eq (f (Fix f)) => Eq (Fix f)
852 but this is so delicate that I don't think it should happen inside
853 'deriving'. If you want this, write it yourself!
854
855 NB: if you want to lift this condition, make sure you still meet the
856 termination conditions! If not, the deriving mechanism generates
857 larger and larger constraints. Example:
858 data Succ a = S a
859 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
860
861 Note the lack of a Show instance for Succ. First we'll generate
862 instance (Show (Succ a), Show a) => Show (Seq a)
863 and then
864 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
865 and so on. Instead we want to complain of no instance for (Show (Succ a)).
866
867 The bottom line
868 ~~~~~~~~~~~~~~~
869 Allow constraints which consist only of type variables, with no repeats.
870 -}