Refactor TcDeriv and TcGenDeriv
[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 Class
17 import DataCon
18 import DynFlags
19 import ErrUtils
20 import Inst
21 import Outputable
22 import PrelNames
23 import TcDerivUtils
24 import TcEnv
25 import TcErrors (reportAllUnsolved)
26 import TcGenFunctor
27 import TcGenGenerics
28 import TcMType
29 import TcRnMonad
30 import TcType
31 import TyCon
32 import Type
33 import TcSimplify
34 import TcValidity (validDerivPred)
35 import TcUnify (buildImplicationFor)
36 import Unify (tcUnifyTy)
37 import Util
38 import VarSet
39
40 import Control.Monad
41 import Data.List
42 import Data.Maybe
43
44 ----------------------
45
46 inferConstraints :: [TyVar] -> Class -> [TcType] -> TcType
47 -> TyCon -> [TcType]
48 -> (ThetaOrigin -> [TyVar] -> [TcType] -> TcM a)
49 -> TcM a
50 -- inferConstraints figures out the constraints needed for the
51 -- instance declaration generated by a 'deriving' clause on a
52 -- data type declaration. It also returns the new in-scope type
53 -- variables and instance types, in case they were changed due to
54 -- the presence of functor-like constraints.
55 -- See Note [Inferring the instance context]
56
57 -- e.g. inferConstraints
58 -- C Int (T [a]) -- Class and inst_tys
59 -- :RTList a -- Rep tycon and its arg tys
60 -- where T [a] ~R :RTList a
61 --
62 -- Generate a sufficiently large set of constraints that typechecking the
63 -- generated method definitions should succeed. This set will be simplified
64 -- before being used in the instance declaration
65 inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
66 | is_generic -- Generic constraints are easy
67 = mkTheta [] tvs inst_tys
68
69 | is_generic1 -- Generic1 needs Functor
70 = ASSERT( length rep_tc_tvs > 0 ) -- See Note [Getting base classes]
71 ASSERT( length cls_tys == 1 ) -- Generic1 has a single kind variable
72 do { functorClass <- tcLookupClass functorClassName
73 ; con_arg_constraints (get_gen1_constraints functorClass) mkTheta }
74
75 | otherwise -- The others are a bit more complicated
76 = ASSERT2( equalLength rep_tc_tvs all_rep_tc_args
77 , ppr main_cls <+> ppr rep_tc
78 $$ ppr rep_tc_tvs $$ ppr all_rep_tc_args )
79 con_arg_constraints get_std_constrained_tys
80 $ \arg_constraints tvs' inst_tys' ->
81 do { traceTc "inferConstraints" $ vcat
82 [ ppr main_cls <+> ppr inst_tys'
83 , ppr arg_constraints
84 ]
85 ; mkTheta (stupid_constraints ++ extra_constraints
86 ++ sc_constraints ++ arg_constraints)
87 tvs' inst_tys' }
88 where
89 tc_binders = tyConBinders rep_tc
90 choose_level bndr
91 | isNamedTyConBinder bndr = KindLevel
92 | otherwise = TypeLevel
93 t_or_ks = map choose_level tc_binders ++ repeat TypeLevel
94 -- want to report *kind* errors when possible
95
96 -- Constraints arising from the arguments of each constructor
97 con_arg_constraints :: (CtOrigin -> TypeOrKind
98 -> Type
99 -> [(ThetaOrigin, Maybe TCvSubst)])
100 -> (ThetaOrigin -> [TyVar] -> [TcType] -> TcM a)
101 -> TcM a
102 con_arg_constraints get_arg_constraints mkTheta
103 = let (predss, mbSubsts) = unzip
104 [ preds_and_mbSubst
105 | data_con <- tyConDataCons rep_tc
106 , (arg_n, arg_t_or_k, arg_ty)
107 <- zip3 [1..] t_or_ks $
108 dataConInstOrigArgTys data_con all_rep_tc_args
109 -- No constraints for unlifted types
110 -- See Note [Deriving and unboxed types]
111 , not (isUnliftedType arg_ty)
112 , let orig = DerivOriginDC data_con arg_n
113 , preds_and_mbSubst <- get_arg_constraints orig arg_t_or_k arg_ty
114 ]
115 preds = concat predss
116 -- If the constraints require a subtype to be of kind (* -> *)
117 -- (which is the case for functor-like constraints), then we
118 -- explicitly unify the subtype's kinds with (* -> *).
119 -- See Note [Inferring the instance context]
120 subst = foldl' composeTCvSubst
121 emptyTCvSubst (catMaybes mbSubsts)
122 unmapped_tvs = filter (\v -> v `notElemTCvSubst` subst
123 && not (v `isInScope` subst)) tvs
124 (subst', _) = mapAccumL substTyVarBndr subst unmapped_tvs
125 preds' = substThetaOrigin subst' preds
126 inst_tys' = substTys subst' inst_tys
127 tvs' = tyCoVarsOfTypesWellScoped inst_tys'
128 in mkTheta preds' tvs' inst_tys'
129
130 is_generic = main_cls `hasKey` genClassKey
131 is_generic1 = main_cls `hasKey` gen1ClassKey
132 -- is_functor_like: see Note [Inferring the instance context]
133 is_functor_like = typeKind inst_ty `tcEqKind` typeToTypeKind
134 || is_generic1 -- Technically, Generic1 requires a type of
135 -- kind (k -> *), not (* -> *), but we still
136 -- label it "functor-like" to make sure
137 -- all_rep_tc_args has all the necessary type
138 -- variables it needs to function.
139
140 get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
141 -> [(ThetaOrigin, Maybe TCvSubst)]
142 get_gen1_constraints functor_cls orig t_or_k ty
143 = mk_functor_like_constraints orig t_or_k functor_cls $
144 get_gen1_constrained_tys last_tv ty
145
146 get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type
147 -> [(ThetaOrigin, Maybe TCvSubst)]
148 get_std_constrained_tys orig t_or_k ty
149 | is_functor_like = mk_functor_like_constraints orig t_or_k main_cls $
150 deepSubtypesContaining last_tv ty
151 | otherwise = [( [mk_cls_pred orig t_or_k main_cls ty]
152 , Nothing )]
153
154 mk_functor_like_constraints :: CtOrigin -> TypeOrKind
155 -> Class -> [Type]
156 -> [(ThetaOrigin, Maybe TCvSubst)]
157 -- 'cls' is usually main_cls (Functor or Traversable etc), but if
158 -- main_cls = Generic1, then 'cls' can be Functor; see get_gen1_constraints
159 --
160 -- For each type, generate two constraints, [cls ty, kind(ty) ~ (*->*)],
161 -- and a kind substitution that results from unifying kind(ty) with * -> *.
162 -- If the unification is successful, it will ensure that the resulting
163 -- instance is well kinded. If not, the second constraint will result
164 -- in an error message which points out the kind mismatch.
165 -- See Note [Inferring the instance context]
166 mk_functor_like_constraints orig t_or_k cls
167 = map $ \ty -> let ki = typeKind ty in
168 ( [ mk_cls_pred orig t_or_k cls ty
169 , mkPredOrigin orig KindLevel
170 (mkPrimEqPred ki typeToTypeKind) ]
171 , tcUnifyTy ki typeToTypeKind
172 )
173
174 rep_tc_tvs = tyConTyVars rep_tc
175 last_tv = last rep_tc_tvs
176 all_rep_tc_args | is_functor_like = rep_tc_args ++ [mkTyVarTy last_tv]
177 | otherwise = rep_tc_args
178
179 -- Constraints arising from superclasses
180 -- See Note [Superclasses of derived instance]
181 cls_tvs = classTyVars main_cls
182 inst_tys = cls_tys ++ [inst_ty]
183 sc_constraints = ASSERT2( equalLength cls_tvs inst_tys, ppr main_cls <+> ppr rep_tc)
184 mkThetaOrigin DerivOrigin TypeLevel $
185 substTheta cls_subst (classSCTheta main_cls)
186 cls_subst = ASSERT( equalLength cls_tvs inst_tys )
187 zipTvSubst cls_tvs inst_tys
188
189 -- Stupid constraints
190 stupid_constraints = mkThetaOrigin DerivOrigin TypeLevel $
191 substTheta tc_subst (tyConStupidTheta rep_tc)
192 tc_subst = ASSERT( equalLength rep_tc_tvs all_rep_tc_args )
193 zipTvSubst rep_tc_tvs all_rep_tc_args
194
195 -- Extra Data constraints
196 -- The Data class (only) requires that for
197 -- instance (...) => Data (T t1 t2)
198 -- IF t1:*, t2:*
199 -- THEN (Data t1, Data t2) are among the (...) constraints
200 -- Reason: when the IF holds, we generate a method
201 -- dataCast2 f = gcast2 f
202 -- and we need the Data constraints to typecheck the method
203 extra_constraints
204 | main_cls `hasKey` dataClassKey
205 , all (isLiftedTypeKind . typeKind) rep_tc_args
206 = [ mk_cls_pred DerivOrigin t_or_k main_cls ty
207 | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
208 | otherwise
209 = []
210
211 mk_cls_pred orig t_or_k cls ty -- Don't forget to apply to cls_tys' too
212 = mkPredOrigin orig t_or_k (mkClassPred cls (cls_tys' ++ [ty]))
213 cls_tys' | is_generic1 = [] -- In the awkward Generic1 case, cls_tys'
214 -- should be empty, since we are applying the
215 -- class Functor.
216 | otherwise = cls_tys
217
218 typeToTypeKind :: Kind
219 typeToTypeKind = liftedTypeKind `mkFunTy` liftedTypeKind
220
221 {-
222 Note [Inferring the instance context]
223 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
224 There are two sorts of 'deriving':
225
226 * InferTheta: the deriving clause for a data type
227 data T a = T1 a deriving( Eq )
228 Here we must infer an instance context,
229 and generate instance declaration
230 instance Eq a => Eq (T a) where ...
231
232 * CheckTheta: standalone deriving
233 deriving instance Eq a => Eq (T a)
234 Here we only need to fill in the bindings;
235 the instance context is user-supplied
236
237 For a deriving clause (InferTheta) we must figure out the
238 instance context (inferConstraints). Suppose we are inferring
239 the instance context for
240 C t1 .. tn (T s1 .. sm)
241 There are two cases
242
243 * (T s1 .. sm) :: * (the normal case)
244 Then we behave like Eq and guess (C t1 .. tn t)
245 for each data constructor arg of type t. More
246 details below.
247
248 * (T s1 .. sm) :: * -> * (the functor-like case)
249 Then we behave like Functor.
250
251 In both cases we produce a bunch of un-simplified constraints
252 and them simplify them in simplifyInstanceContexts; see
253 Note [Simplifying the instance context].
254
255 In the functor-like case, we may need to unify some kind variables with * in
256 order for the generated instance to be well-kinded. An example from
257 Trac #10524:
258
259 newtype Compose (f :: k2 -> *) (g :: k1 -> k2) (a :: k1)
260 = Compose (f (g a)) deriving Functor
261
262 Earlier in the deriving pipeline, GHC unifies the kind of Compose f g
263 (k1 -> *) with the kind of Functor's argument (* -> *), so k1 := *. But this
264 alone isn't enough, since k2 wasn't unified with *:
265
266 instance (Functor (f :: k2 -> *), Functor (g :: * -> k2)) =>
267 Functor (Compose f g) where ...
268
269 The two Functor constraints are ill-kinded. To ensure this doesn't happen, we:
270
271 1. Collect all of a datatype's subtypes which require functor-like
272 constraints.
273 2. For each subtype, create a substitution by unifying the subtype's kind
274 with (* -> *).
275 3. Compose all the substitutions into one, then apply that substitution to
276 all of the in-scope type variables and the instance types.
277
278 Note [Getting base classes]
279 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
280 Functor and Typeable are defined in package 'base', and that is not available
281 when compiling 'ghc-prim'. So we must be careful that 'deriving' for stuff in
282 ghc-prim does not use Functor or Typeable implicitly via these lookups.
283
284 Note [Deriving and unboxed types]
285 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
286 We have some special hacks to support things like
287 data T = MkT Int# deriving ( Show )
288
289 Specifically, we use TcGenDeriv.box to box the Int# into an Int
290 (which we know how to show), and append a '#'. Parenthesis are not required
291 for unboxed values (`MkT -3#` is a valid expression).
292
293 Note [Superclasses of derived instance]
294 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
295 In general, a derived instance decl needs the superclasses of the derived
296 class too. So if we have
297 data T a = ...deriving( Ord )
298 then the initial context for Ord (T a) should include Eq (T a). Often this is
299 redundant; we'll also generate an Ord constraint for each constructor argument,
300 and that will probably generate enough constraints to make the Eq (T a) constraint
301 be satisfied too. But not always; consider:
302
303 data S a = S
304 instance Eq (S a)
305 instance Ord (S a)
306
307 data T a = MkT (S a) deriving( Ord )
308 instance Num a => Eq (T a)
309
310 The derived instance for (Ord (T a)) must have a (Num a) constraint!
311 Similarly consider:
312 data T a = MkT deriving( Data )
313 Here there *is* no argument field, but we must nevertheless generate
314 a context for the Data instances:
315 instance Typeable a => Data (T a) where ...
316
317 ************************************************************************
318 * *
319 Finding the fixed point of deriving equations
320 * *
321 ************************************************************************
322
323 Note [Simplifying the instance context]
324 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
325 Consider
326
327 data T a b = C1 (Foo a) (Bar b)
328 | C2 Int (T b a)
329 | C3 (T a a)
330 deriving (Eq)
331
332 We want to come up with an instance declaration of the form
333
334 instance (Ping a, Pong b, ...) => Eq (T a b) where
335 x == y = ...
336
337 It is pretty easy, albeit tedious, to fill in the code "...". The
338 trick is to figure out what the context for the instance decl is,
339 namely Ping, Pong and friends.
340
341 Let's call the context reqd for the T instance of class C at types
342 (a,b, ...) C (T a b). Thus:
343
344 Eq (T a b) = (Ping a, Pong b, ...)
345
346 Now we can get a (recursive) equation from the data decl. This part
347 is done by inferConstraints.
348
349 Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1
350 u Eq (T b a) u Eq Int -- From C2
351 u Eq (T a a) -- From C3
352
353
354 Foo and Bar may have explicit instances for Eq, in which case we can
355 just substitute for them. Alternatively, either or both may have
356 their Eq instances given by deriving clauses, in which case they
357 form part of the system of equations.
358
359 Now all we need do is simplify and solve the equations, iterating to
360 find the least fixpoint. This is done by simplifyInstanceConstraints.
361 Notice that the order of the arguments can
362 switch around, as here in the recursive calls to T.
363
364 Let's suppose Eq (Foo a) = Eq a, and Eq (Bar b) = Ping b.
365
366 We start with:
367
368 Eq (T a b) = {} -- The empty set
369
370 Next iteration:
371 Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1
372 u Eq (T b a) u Eq Int -- From C2
373 u Eq (T a a) -- From C3
374
375 After simplification:
376 = Eq a u Ping b u {} u {} u {}
377 = Eq a u Ping b
378
379 Next iteration:
380
381 Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1
382 u Eq (T b a) u Eq Int -- From C2
383 u Eq (T a a) -- From C3
384
385 After simplification:
386 = Eq a u Ping b
387 u (Eq b u Ping a)
388 u (Eq a u Ping a)
389
390 = Eq a u Ping b u Eq b u Ping a
391
392 The next iteration gives the same result, so this is the fixpoint. We
393 need to make a canonical form of the RHS to ensure convergence. We do
394 this by simplifying the RHS to a form in which
395
396 - the classes constrain only tyvars
397 - the list is sorted by tyvar (major key) and then class (minor key)
398 - no duplicates, of course
399
400 Note [Deterministic simplifyInstanceContexts]
401 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
402 Canonicalisation uses nonDetCmpType which is nondeterministic. Sorting
403 with nonDetCmpType puts the returned lists in a nondeterministic order.
404 If we were to return them, we'd get class constraints in
405 nondeterministic order.
406
407 Consider:
408
409 data ADT a b = Z a b deriving Eq
410
411 The generated code could be either:
412
413 instance (Eq a, Eq b) => Eq (Z a b) where
414
415 Or:
416
417 instance (Eq b, Eq a) => Eq (Z a b) where
418
419 To prevent the order from being nondeterministic we only
420 canonicalize when comparing and return them in the same order as
421 simplifyDeriv returned them.
422 See also Note [nonDetCmpType nondeterminism]
423 -}
424
425
426 simplifyInstanceContexts :: [DerivSpec ThetaOrigin] -> TcM [DerivSpec ThetaType]
427 -- Used only for deriving clauses (InferTheta)
428 -- not for standalone deriving
429 -- See Note [Simplifying the instance context]
430
431 simplifyInstanceContexts [] = return []
432
433 simplifyInstanceContexts infer_specs
434 = do { traceTc "simplifyInstanceContexts" $ vcat (map pprDerivSpec infer_specs)
435 ; iterate_deriv 1 initial_solutions }
436 where
437 ------------------------------------------------------------------
438 -- The initial solutions for the equations claim that each
439 -- instance has an empty context; this solution is certainly
440 -- in canonical form.
441 initial_solutions :: [ThetaType]
442 initial_solutions = [ [] | _ <- infer_specs ]
443
444 ------------------------------------------------------------------
445 -- iterate_deriv calculates the next batch of solutions,
446 -- compares it with the current one; finishes if they are the
447 -- same, otherwise recurses with the new solutions.
448 -- It fails if any iteration fails
449 iterate_deriv :: Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
450 iterate_deriv n current_solns
451 | n > 20 -- Looks as if we are in an infinite loop
452 -- This can happen if we have -XUndecidableInstances
453 -- (See TcSimplify.tcSimplifyDeriv.)
454 = pprPanic "solveDerivEqns: probable loop"
455 (vcat (map pprDerivSpec infer_specs) $$ ppr current_solns)
456 | otherwise
457 = do { -- Extend the inst info from the explicit instance decls
458 -- with the current set of solutions, and simplify each RHS
459 inst_specs <- zipWithM newDerivClsInst current_solns infer_specs
460 ; new_solns <- checkNoErrs $
461 extendLocalInstEnv inst_specs $
462 mapM gen_soln infer_specs
463
464 ; if (current_solns `eqSolution` new_solns) then
465 return [ spec { ds_theta = soln }
466 | (spec, soln) <- zip infer_specs current_solns ]
467 else
468 iterate_deriv (n+1) new_solns }
469
470 eqSolution a b = eqListBy (eqListBy eqType) (canSolution a) (canSolution b)
471 -- Canonicalise for comparison
472 -- See Note [Deterministic simplifyInstanceContexts]
473 canSolution = map (sortBy nonDetCmpType)
474 ------------------------------------------------------------------
475 gen_soln :: DerivSpec ThetaOrigin -> TcM ThetaType
476 gen_soln (DS { ds_loc = loc, ds_tvs = tyvars
477 , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
478 = setSrcSpan loc $
479 addErrCtxt (derivInstCtxt the_pred) $
480 do { theta <- simplifyDeriv the_pred tyvars deriv_rhs
481 -- checkValidInstance tyvars theta clas inst_tys
482 -- Not necessary; see Note [Exotic derived instance contexts]
483
484 ; traceTc "TcDeriv" (ppr deriv_rhs $$ ppr theta)
485 -- Claim: the result instance declaration is guaranteed valid
486 -- Hence no need to call:
487 -- checkValidInstance tyvars theta clas inst_tys
488 ; return theta }
489 where
490 the_pred = mkClassPred clas inst_tys
491
492 derivInstCtxt :: PredType -> MsgDoc
493 derivInstCtxt pred
494 = text "When deriving the instance for" <+> parens (ppr pred)
495
496 {-
497 ***********************************************************************************
498 * *
499 * Simplify derived constraints
500 * *
501 ***********************************************************************************
502 -}
503
504 -- | Given @instance (wanted) => C inst_ty@, simplify 'wanted' as much
505 -- as possible. Fail if not possible.
506 simplifyDeriv :: PredType -- ^ @C inst_ty@, head of the instance we are
507 -- deriving. Only used for SkolemInfo.
508 -> [TyVar] -- ^ The tyvars bound by @inst_ty@.
509 -> ThetaOrigin -- ^ @wanted@ constraints, i.e. @['PredOrigin']@.
510 -> TcM ThetaType -- ^ Needed constraints (after simplification),
511 -- i.e. @['PredType']@.
512 simplifyDeriv pred tvs theta
513 = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
514 -- The constraint solving machinery
515 -- expects *TcTyVars* not TyVars.
516 -- We use *non-overlappable* (vanilla) skolems
517 -- See Note [Overlap and deriving]
518
519 ; let skol_set = mkVarSet tvs_skols
520 skol_info = DerivSkol pred
521 doc = text "deriving" <+> parens (ppr pred)
522 mk_ct (PredOrigin t o t_or_k)
523 = newWanted o (Just t_or_k) (substTy skol_subst t)
524
525 -- Generate the wanted constraints with the skolemized variables
526 ; (wanted, tclvl) <- pushTcLevelM (mapM mk_ct theta)
527
528 ; traceTc "simplifyDeriv inputs" $
529 vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
530 -- Simplify the constraints
531 ; residual_wanted <- simplifyWantedsTcM wanted
532 -- Result is zonked
533
534 -- Split the resulting constraints into bad and good constraints,
535 -- building an @unsolved :: WantedConstraints@ representing all
536 -- the constraints we can't just shunt to the predicates.
537 -- See Note [Exotic derived instance contexts]
538 ; let residual_simple = wc_simple residual_wanted
539 (bad, good) = partitionBagWith get_good residual_simple
540 unsolved = residual_wanted { wc_simple = bad }
541
542 -- See Note [Exotic derived instance contexts]
543
544 get_good :: Ct -> Either Ct PredType
545 get_good ct | validDerivPred skol_set p
546 , isWantedCt ct
547 = Right p
548 -- NB re 'isWantedCt': residual_wanted may contain
549 -- unsolved CtDerived and we stick them into the
550 -- bad set so that reportUnsolved may decide what
551 -- to do with them
552 | otherwise
553 = Left ct
554 where p = ctPred ct
555
556 ; traceTc "simplifyDeriv outputs" $
557 vcat [ ppr tvs_skols, ppr residual_simple, ppr good, ppr bad ]
558
559 -- If we are deferring type errors, simply ignore any insoluble
560 -- constraints. They'll come up again when we typecheck the
561 -- generated instance declaration
562 ; defer <- goptM Opt_DeferTypeErrors
563 ; (implic, _) <- buildImplicationFor tclvl skol_info tvs_skols [] unsolved
564 -- The buildImplicationFor is just to bind the skolems,
565 -- in case they are mentioned in error messages
566 -- See Trac #11347
567 -- Report the (bad) unsolved constraints
568 ; unless defer (reportAllUnsolved (mkImplicWC implic))
569
570
571 -- Return the good unsolved constraints (unskolemizing on the way out.)
572 ; let min_theta = mkMinimalBySCs (bagToList good)
573 subst_skol = zipTvSubst tvs_skols $ mkTyVarTys tvs
574 -- The reverse substitution (sigh)
575 ; return (substTheta subst_skol min_theta) }
576
577 {-
578 Note [Overlap and deriving]
579 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
580 Consider some overlapping instances:
581 data Show a => Show [a] where ..
582 data Show [Char] where ...
583
584 Now a data type with deriving:
585 data T a = MkT [a] deriving( Show )
586
587 We want to get the derived instance
588 instance Show [a] => Show (T a) where...
589 and NOT
590 instance Show a => Show (T a) where...
591 so that the (Show (T Char)) instance does the Right Thing
592
593 It's very like the situation when we're inferring the type
594 of a function
595 f x = show [x]
596 and we want to infer
597 f :: Show [a] => a -> String
598
599 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
600 the context for the derived instance.
601 Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
602
603 Note [Exotic derived instance contexts]
604 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
605 In a 'derived' instance declaration, we *infer* the context. It's a
606 bit unclear what rules we should apply for this; the Haskell report is
607 silent. Obviously, constraints like (Eq a) are fine, but what about
608 data T f a = MkT (f a) deriving( Eq )
609 where we'd get an Eq (f a) constraint. That's probably fine too.
610
611 One could go further: consider
612 data T a b c = MkT (Foo a b c) deriving( Eq )
613 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
614
615 Notice that this instance (just) satisfies the Paterson termination
616 conditions. Then we *could* derive an instance decl like this:
617
618 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
619 even though there is no instance for (C Int a), because there just
620 *might* be an instance for, say, (C Int Bool) at a site where we
621 need the equality instance for T's.
622
623 However, this seems pretty exotic, and it's quite tricky to allow
624 this, and yet give sensible error messages in the (much more common)
625 case where we really want that instance decl for C.
626
627 So for now we simply require that the derived instance context
628 should have only type-variable constraints.
629
630 Here is another example:
631 data Fix f = In (f (Fix f)) deriving( Eq )
632 Here, if we are prepared to allow -XUndecidableInstances we
633 could derive the instance
634 instance Eq (f (Fix f)) => Eq (Fix f)
635 but this is so delicate that I don't think it should happen inside
636 'deriving'. If you want this, write it yourself!
637
638 NB: if you want to lift this condition, make sure you still meet the
639 termination conditions! If not, the deriving mechanism generates
640 larger and larger constraints. Example:
641 data Succ a = S a
642 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
643
644 Note the lack of a Show instance for Succ. First we'll generate
645 instance (Show (Succ a), Show a) => Show (Seq a)
646 and then
647 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
648 and so on. Instead we want to complain of no instance for (Show (Succ a)).
649
650 The bottom line
651 ~~~~~~~~~~~~~~~
652 Allow constraints which consist only of type variables, with no repeats.
653 -}