Make a smart mkAppTyM
[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 ErrUtils
23 import Inst
24 import Outputable
25 import PrelNames
26 import TcDerivUtils
27 import TcEnv
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, checkConstraints)
38 import Unify (tcUnifyTy)
39 import Util
40 import Var
41 import VarSet
42
43 import Control.Monad
44 import Control.Monad.Trans.Class (lift)
45 import Control.Monad.Trans.Reader (ask)
46 import Data.List
47 import Data.Maybe
48
49 ----------------------
50
51 inferConstraints :: DerivSpecMechanism
52 -> DerivM ([ThetaOrigin], [TyVar], [TcType])
53 -- inferConstraints figures out the constraints needed for the
54 -- instance declaration generated by a 'deriving' clause on a
55 -- data type declaration. It also returns the new in-scope type
56 -- variables and instance types, in case they were changed due to
57 -- the presence of functor-like constraints.
58 -- See Note [Inferring the instance context]
59
60 -- e.g. inferConstraints
61 -- C Int (T [a]) -- Class and inst_tys
62 -- :RTList a -- Rep tycon and its arg tys
63 -- where T [a] ~R :RTList a
64 --
65 -- Generate a sufficiently large set of constraints that typechecking the
66 -- generated method definitions should succeed. This set will be simplified
67 -- before being used in the instance declaration
68 inferConstraints mechanism
69 = do { DerivEnv { denv_tc = tc
70 , denv_tc_args = tc_args
71 , denv_cls = main_cls
72 , denv_cls_tys = cls_tys } <- ask
73 ; wildcard <- isStandaloneWildcardDeriv
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 (mkDerivOrigin wildcard)
88 TypeLevel [] [] [] $
89 substTheta cls_subst (classSCTheta main_cls) ]
90 cls_subst = ASSERT( equalLength cls_tvs inst_tys )
91 zipTvSubst cls_tvs inst_tys
92
93 ; (inferred_constraints, tvs', inst_tys') <- infer_constraints
94 ; lift $ traceTc "inferConstraints" $ vcat
95 [ ppr main_cls <+> ppr inst_tys'
96 , ppr inferred_constraints
97 ]
98 ; return ( sc_constraints ++ inferred_constraints
99 , tvs', inst_tys' ) }
100
101 -- | Like 'inferConstraints', but used only in the case of deriving strategies
102 -- where the constraints are inferred by inspecting the fields of each data
103 -- constructor (i.e., stock- and newtype-deriving).
104 inferConstraintsDataConArgs :: TcType -> [TcType]
105 -> DerivM ([ThetaOrigin], [TyVar], [TcType])
106 inferConstraintsDataConArgs inst_ty inst_tys
107 = do DerivEnv { denv_tvs = tvs
108 , denv_rep_tc = rep_tc
109 , denv_rep_tc_args = rep_tc_args
110 , denv_cls = main_cls
111 , denv_cls_tys = cls_tys } <- ask
112 wildcard <- isStandaloneWildcardDeriv
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 wildcard
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', _) = substTyVarBndrs 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 = tcTypeKind 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 = tcTypeKind 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 deriv_origin 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 . tcTypeKind) rep_tc_args
236 = [ mk_cls_pred deriv_origin 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 deriv_origin = mkDerivOrigin wildcard
251
252 if -- Generic constraints are easy
253 | is_generic
254 -> return ([], tvs, inst_tys)
255
256 -- Generic1 needs Functor
257 -- See Note [Getting base classes]
258 | is_generic1
259 -> ASSERT( rep_tc_tvs `lengthExceeds` 0 )
260 -- Generic1 has a single kind variable
261 ASSERT( cls_tys `lengthIs` 1 )
262 do { functorClass <- lift $ tcLookupClass functorClassName
263 ; pure $ con_arg_constraints
264 $ get_gen1_constraints functorClass }
265
266 -- The others are a bit more complicated
267 | otherwise
268 -> -- See the comment with all_rep_tc_args for an explanation of
269 -- this assertion
270 ASSERT2( equalLength rep_tc_tvs all_rep_tc_args
271 , ppr main_cls <+> ppr rep_tc
272 $$ ppr rep_tc_tvs $$ ppr all_rep_tc_args )
273 do { let (arg_constraints, tvs', inst_tys')
274 = con_arg_constraints get_std_constrained_tys
275 ; lift $ traceTc "inferConstraintsDataConArgs" $ vcat
276 [ ppr main_cls <+> ppr inst_tys'
277 , ppr arg_constraints
278 ]
279 ; return ( stupid_constraints ++ extra_constraints
280 ++ arg_constraints
281 , tvs', inst_tys') }
282
283 typeToTypeKind :: Kind
284 typeToTypeKind = liftedTypeKind `mkFunTy` liftedTypeKind
285
286 -- | Like 'inferConstraints', but used only in the case of @DeriveAnyClass@,
287 -- which gathers its constraints based on the type signatures of the class's
288 -- methods instead of the types of the data constructor's field.
289 --
290 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
291 -- for an explanation of how these constraints are used to determine the
292 -- derived instance context.
293 inferConstraintsDAC :: [TcType] -> DerivM ([ThetaOrigin], [TyVar], [TcType])
294 inferConstraintsDAC inst_tys
295 = do { DerivEnv { denv_tvs = tvs
296 , denv_cls = cls } <- ask
297 ; wildcard <- isStandaloneWildcardDeriv
298
299 ; let gen_dms = [ (sel_id, dm_ty)
300 | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ]
301
302 cls_tvs = classTyVars cls
303
304 do_one_meth :: (Id, Type) -> TcM ThetaOrigin
305 -- (Id,Type) are the selector Id and the generic default method type
306 -- NB: the latter is /not/ quantified over the class variables
307 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
308 do_one_meth (sel_id, gen_dm_ty)
309 = do { let (sel_tvs, _cls_pred, meth_ty)
310 = tcSplitMethodTy (varType sel_id)
311 meth_ty' = substTyWith sel_tvs inst_tys meth_ty
312 (meth_tvs, meth_theta, meth_tau)
313 = tcSplitNestedSigmaTys meth_ty'
314
315 gen_dm_ty' = substTyWith cls_tvs inst_tys gen_dm_ty
316 (dm_tvs, dm_theta, dm_tau)
317 = tcSplitNestedSigmaTys gen_dm_ty'
318 tau_eq = mkPrimEqPred meth_tau dm_tau
319 ; return (mkThetaOrigin (mkDerivOrigin wildcard) TypeLevel
320 meth_tvs dm_tvs meth_theta (tau_eq:dm_theta)) }
321
322 ; theta_origins <- lift $ mapM do_one_meth gen_dms
323 ; return (theta_origins, tvs, inst_tys) }
324
325 {- Note [Inferring the instance context]
326 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
327 There are two sorts of 'deriving', as represented by the two constructors
328 for DerivContext:
329
330 * InferContext mb_wildcard: This can either be:
331 - The deriving clause for a data type.
332 (e.g, data T a = T1 a deriving( Eq ))
333 In this case, mb_wildcard = Nothing.
334 - A standalone declaration with an extra-constraints wildcard
335 (e.g., deriving instance _ => Eq (Foo a))
336 In this case, mb_wildcard = Just loc, where loc is the location
337 of the extra-constraints wildcard.
338
339 Here we must infer an instance context,
340 and generate instance declaration
341 instance Eq a => Eq (T a) where ...
342
343 * SupplyContext theta: standalone deriving
344 deriving instance Eq a => Eq (T a)
345 Here we only need to fill in the bindings;
346 the instance context (theta) is user-supplied
347
348 For the InferContext case, 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 '#'. Parentheses 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 or standalone deriving with an
541 -- extra-constraints wildcard (InferContext)
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 emit_wanted_constraints :: [TyVar] -> [PredOrigin] -> TcM ()
642 emit_wanted_constraints metas_to_be preds
643 = do { -- We instantiate metas_to_be with fresh meta type
644 -- variables. Currently, these can only be type variables
645 -- quantified in generic default type signatures.
646 -- See Note [Gathering and simplifying constraints for
647 -- DeriveAnyClass]
648 (meta_subst, _meta_tvs) <- newMetaTyVars metas_to_be
649
650 -- Now make a constraint for each of the instantiated predicates
651 ; let wanted_subst = skol_subst `unionTCvSubst` meta_subst
652 mk_wanted_ct (PredOrigin wanted orig t_or_k)
653 = do { ev <- newWanted orig (Just t_or_k) $
654 substTyUnchecked wanted_subst wanted
655 ; return (mkNonCanonical ev) }
656 ; cts <- mapM mk_wanted_ct preds
657
658 -- And emit them into the monad
659 ; emitSimples (listToCts cts) }
660
661 -- Create the implications we need to solve. For stock and newtype
662 -- deriving, these implication constraints will be simple class
663 -- constraints like (C a, Ord b).
664 -- But with DeriveAnyClass, we make an implication constraint.
665 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
666 mk_wanteds :: ThetaOrigin -> TcM WantedConstraints
667 mk_wanteds (ThetaOrigin { to_anyclass_skols = ac_skols
668 , to_anyclass_metas = ac_metas
669 , to_anyclass_givens = ac_givens
670 , to_wanted_origins = preds })
671 = do { ac_given_evs <- mapM mk_given_ev ac_givens
672 ; (_, wanteds)
673 <- captureConstraints $
674 checkConstraints skol_info ac_skols ac_given_evs $
675 -- The checkConstraints bumps the TcLevel, and
676 -- wraps the wanted constraints in an implication,
677 -- when (but only when) necessary
678 emit_wanted_constraints ac_metas preds
679 ; pure wanteds }
680
681 -- See [STEP DAC BUILD]
682 -- Generate the implication constraints, one for each method, to solve
683 -- with the skolemized variables. Start "one level down" because
684 -- we are going to wrap the result in an implication with tvs_skols,
685 -- in step [DAC RESIDUAL]
686 ; (tc_lvl, wanteds) <- pushTcLevelM $
687 mapM mk_wanteds thetas
688
689 ; traceTc "simplifyDeriv inputs" $
690 vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ]
691
692 -- See [STEP DAC SOLVE]
693 -- Simplify the constraints, starting at the same level at which
694 -- they are generated (c.f. the call to runTcSWithEvBinds in
695 -- simplifyInfer)
696 ; solved_wanteds <- setTcLevel tc_lvl $
697 runTcSDeriveds $
698 solveWantedsAndDrop $
699 unionsWC wanteds
700
701 -- It's not yet zonked! Obviously zonk it before peering at it
702 ; solved_wanteds <- zonkWC solved_wanteds
703
704 -- See [STEP DAC HOIST]
705 -- Split the resulting constraints into bad and good constraints,
706 -- building an @unsolved :: WantedConstraints@ representing all
707 -- the constraints we can't just shunt to the predicates.
708 -- See Note [Exotic derived instance contexts]
709 ; let residual_simple = approximateWC True solved_wanteds
710 (bad, good) = partitionBagWith get_good residual_simple
711
712 get_good :: Ct -> Either Ct PredType
713 get_good ct | validDerivPred skol_set p
714 , isWantedCt ct
715 = Right p
716 -- TODO: This is wrong
717 -- NB re 'isWantedCt': residual_wanted may contain
718 -- unsolved CtDerived and we stick them into the
719 -- bad set so that reportUnsolved may decide what
720 -- to do with them
721 | otherwise
722 = Left ct
723 where p = ctPred ct
724
725 ; traceTc "simplifyDeriv outputs" $
726 vcat [ ppr tvs_skols, ppr residual_simple, ppr good, ppr bad ]
727
728 -- Return the good unsolved constraints (unskolemizing on the way out.)
729 ; let min_theta = mkMinimalBySCs id (bagToList good)
730 -- An important property of mkMinimalBySCs (used above) is that in
731 -- addition to removing constraints that are made redundant by
732 -- superclass relationships, it also removes _duplicate_
733 -- constraints.
734 -- See Note [Gathering and simplifying constraints for
735 -- DeriveAnyClass]
736 subst_skol = zipTvSubst tvs_skols $ mkTyVarTys tvs
737 -- The reverse substitution (sigh)
738
739 -- See [STEP DAC RESIDUAL]
740 ; min_theta_vars <- mapM newEvVar min_theta
741 ; (leftover_implic, _)
742 <- buildImplicationFor tc_lvl skol_info tvs_skols
743 min_theta_vars solved_wanteds
744 -- This call to simplifyTop is purely for error reporting
745 -- See Note [Error reporting for deriving clauses]
746 -- See also Note [Exotic derived instance contexts], which are caught
747 -- in this line of code.
748 ; simplifyTopImplic leftover_implic
749
750 ; return (substTheta subst_skol min_theta) }
751
752 {-
753 Note [Overlap and deriving]
754 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
755 Consider some overlapping instances:
756 instance Show a => Show [a] where ..
757 instance Show [Char] where ...
758
759 Now a data type with deriving:
760 data T a = MkT [a] deriving( Show )
761
762 We want to get the derived instance
763 instance Show [a] => Show (T a) where...
764 and NOT
765 instance Show a => Show (T a) where...
766 so that the (Show (T Char)) instance does the Right Thing
767
768 It's very like the situation when we're inferring the type
769 of a function
770 f x = show [x]
771 and we want to infer
772 f :: Show [a] => a -> String
773
774 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
775 the context for the derived instance.
776 Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
777
778 Note [Gathering and simplifying constraints for DeriveAnyClass]
779 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
780 DeriveAnyClass works quite differently from stock and newtype deriving in
781 the way it gathers and simplifies constraints to be used in a derived
782 instance's context. Stock and newtype deriving gather constraints by looking
783 at the data constructors of the data type for which we are deriving an
784 instance. But DeriveAnyClass doesn't need to know about a data type's
785 definition at all!
786
787 To see why, consider this example of DeriveAnyClass:
788
789 class Foo a where
790 bar :: forall b. Ix b => a -> b -> String
791 default bar :: (Show a, Ix c) => a -> c -> String
792 bar x y = show x ++ show (range (y,y))
793
794 baz :: Eq a => a -> a -> Bool
795 default baz :: (Ord a, Show a) => a -> a -> Bool
796 baz x y = compare x y == EQ
797
798 Because 'bar' and 'baz' have default signatures, this generates a top-level
799 definition for these generic default methods
800
801 $gdm_bar :: forall a. Foo a
802 => forall c. (Show a, Ix c)
803 => a -> c -> String
804 $gdm_bar x y = show x ++ show (range (y,y))
805
806 (and similarly for baz). Now consider a 'deriving' clause
807 data Maybe s = ... deriving Foo
808
809 This derives an instance of the form:
810 instance (CX) => Foo (Maybe s) where
811 bar = $gdm_bar
812 baz = $gdm_baz
813
814 Now it is GHC's job to fill in a suitable instance context (CX). If
815 GHC were typechecking the binding
816 bar = $gdm bar
817 it would
818 * skolemise the expected type of bar
819 * instantiate the type of $gdm_bar with meta-type variables
820 * build an implication constraint
821
822 [STEP DAC BUILD]
823 So that's what we do. We build the constraint (call it C1)
824
825 forall[2] b. Ix b => (Show (Maybe s), Ix cc,
826 Maybe s -> b -> String
827 ~ Maybe s -> cc -> String)
828
829 Here:
830 * The level of this forall constraint is forall[2], because we are later
831 going to wrap it in a forall[1] in [STEP DAC RESIDUAL]
832
833 * The 'b' comes from the quantified type variable in the expected type
834 of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
835 variable that comes from instantiating the quantified type variable 'c' in
836 $gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
837
838 * The (Ix b) constraint comes from the context of bar's type
839 (i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc)
840 constraints come from the context of $gdm_bar's type
841 (i.e., 'to_anyclass_givens' in 'ThetaOrigin').
842
843 * The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String)
844 comes from marrying up the instantiated type of $gdm_bar with the specified
845 type of bar. Notice that the type variables from the instance, 's' in this
846 case, are global to this constraint.
847
848 Note that it is vital that we instantiate the `c` in $gdm_bar's type with a new
849 unification variable for each iteration of simplifyDeriv. If we re-use the same
850 unification variable across multiple iterations, then bad things can happen,
851 such as Trac #14933.
852
853 Similarly for 'baz', givng the constraint C2
854
855 forall[2]. Eq (Maybe s) => (Ord a, Show a,
856 Maybe s -> Maybe s -> Bool
857 ~ Maybe s -> Maybe s -> Bool)
858
859 In this case baz has no local quantification, so the implication
860 constraint has no local skolems and there are no unification
861 variables.
862
863 [STEP DAC SOLVE]
864 We can combine these two implication constraints into a single
865 constraint (C1, C2), and simplify, unifying cc:=b, to get:
866
867 forall[2] b. Ix b => Show a
868 /\
869 forall[2]. Eq (Maybe s) => (Ord a, Show a)
870
871 [STEP DAC HOIST]
872 Let's call that (C1', C2'). Now we need to hoist the unsolved
873 constraints out of the implications to become our candidate for
874 (CX). That is done by approximateWC, which will return:
875
876 (Show a, Ord a, Show a)
877
878 Now we can use mkMinimalBySCs to remove superclasses and duplicates, giving
879
880 (Show a, Ord a)
881
882 And that's what GHC uses for CX.
883
884 [STEP DAC RESIDUAL]
885 In this case we have solved all the leftover constraints, but what if
886 we don't? Simple! We just form the final residual constraint
887
888 forall[1] s. CX => (C1',C2')
889
890 and simplify that. In simple cases it'll succeed easily, because CX
891 literally contains the constraints in C1', C2', but if there is anything
892 more complicated it will be reported in a civilised way.
893
894 Note [Error reporting for deriving clauses]
895 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
896 A suprisingly tricky aspect of deriving to get right is reporting sensible
897 error messages. In particular, if simplifyDeriv reaches a constraint that it
898 cannot solve, which might include:
899
900 1. Insoluble constraints
901 2. "Exotic" constraints (See Note [Exotic derived instance contexts])
902
903 Then we report an error immediately in simplifyDeriv.
904
905 Another possible choice is to punt and let another part of the typechecker
906 (e.g., simplifyInstanceContexts) catch the errors. But this tends to lead
907 to worse error messages, so we do it directly in simplifyDeriv.
908
909 simplifyDeriv checks for errors in a clever way. If the deriving machinery
910 infers the context (Foo a)--that is, if this instance is to be generated:
911
912 instance Foo a => ...
913
914 Then we form an implication of the form:
915
916 forall a. Foo a => <residual_wanted_constraints>
917
918 And pass it to the simplifier. If the context (Foo a) is enough to discharge
919 all the constraints in <residual_wanted_constraints>, then everything is
920 hunky-dory. But if <residual_wanted_constraints> contains, say, an insoluble
921 constraint, then (Foo a) won't be able to solve it, causing GHC to error.
922
923 Note [Exotic derived instance contexts]
924 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
925 In a 'derived' instance declaration, we *infer* the context. It's a
926 bit unclear what rules we should apply for this; the Haskell report is
927 silent. Obviously, constraints like (Eq a) are fine, but what about
928 data T f a = MkT (f a) deriving( Eq )
929 where we'd get an Eq (f a) constraint. That's probably fine too.
930
931 One could go further: consider
932 data T a b c = MkT (Foo a b c) deriving( Eq )
933 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
934
935 Notice that this instance (just) satisfies the Paterson termination
936 conditions. Then we *could* derive an instance decl like this:
937
938 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
939 even though there is no instance for (C Int a), because there just
940 *might* be an instance for, say, (C Int Bool) at a site where we
941 need the equality instance for T's.
942
943 However, this seems pretty exotic, and it's quite tricky to allow
944 this, and yet give sensible error messages in the (much more common)
945 case where we really want that instance decl for C.
946
947 So for now we simply require that the derived instance context
948 should have only type-variable constraints.
949
950 Here is another example:
951 data Fix f = In (f (Fix f)) deriving( Eq )
952 Here, if we are prepared to allow -XUndecidableInstances we
953 could derive the instance
954 instance Eq (f (Fix f)) => Eq (Fix f)
955 but this is so delicate that I don't think it should happen inside
956 'deriving'. If you want this, write it yourself!
957
958 NB: if you want to lift this condition, make sure you still meet the
959 termination conditions! If not, the deriving mechanism generates
960 larger and larger constraints. Example:
961 data Succ a = S a
962 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
963
964 Note the lack of a Show instance for Succ. First we'll generate
965 instance (Show (Succ a), Show a) => Show (Seq a)
966 and then
967 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
968 and so on. Instead we want to complain of no instance for (Show (Succ a)).
969
970 The bottom line
971 ~~~~~~~~~~~~~~~
972 Allow constraints which consist only of type variables, with no repeats.
973 -}