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