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