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