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