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