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