1-- (c) The University of Glasgow 2006 2-- 3-- FamInstEnv: Type checked family instance declarations 4 5{-# LANGUAGE CPP, GADTs, ScopedTypeVariables, BangPatterns, TupleSections, 6 DeriveFunctor #-} 7 8{-# OPTIONS_GHC -Wno-incomplete-record-updates #-} 9 10module GHC.Core.FamInstEnv ( 11 FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS, 12 famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon, 13 pprFamInst, pprFamInsts, 14 mkImportedFamInst, 15 16 FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, 17 extendFamInstEnv, extendFamInstEnvList, 18 famInstEnvElts, famInstEnvSize, familyInstances, 19 20 -- * CoAxioms 21 mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom, 22 mkNewTypeCoAxiom, 23 24 FamInstMatch(..), 25 lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon, 26 27 isDominatedBy, apartnessCheck, 28 29 -- Injectivity 30 InjectivityCheckResult(..), 31 lookupFamInstEnvInjectivityConflicts, injectiveBranches, 32 33 -- Normalisation 34 topNormaliseType, topNormaliseType_maybe, 35 normaliseType, normaliseTcApp, 36 topReduceTyFamApp_maybe, reduceTyFamApp_maybe, 37 38 -- Flattening 39 flattenTys 40 ) where 41 42#include "GhclibHsVersions.h" 43 44import GHC.Prelude 45 46import GHC.Core.Unify 47import GHC.Core.Type as Type 48import GHC.Core.TyCo.Rep 49import GHC.Core.TyCon 50import GHC.Core.Coercion 51import GHC.Core.Coercion.Axiom 52import GHC.Types.Var.Set 53import GHC.Types.Var.Env 54import GHC.Types.Name 55import GHC.Types.Unique.DFM 56import GHC.Utils.Outputable 57import GHC.Data.Maybe 58import GHC.Core.Map 59import GHC.Types.Unique 60import GHC.Utils.Misc 61import GHC.Types.Var 62import GHC.Types.SrcLoc 63import GHC.Data.FastString 64import Control.Monad 65import Data.List( mapAccumL ) 66import Data.Array( Array, assocs ) 67 68{- 69************************************************************************ 70* * 71 Type checked family instance heads 72* * 73************************************************************************ 74 75Note [FamInsts and CoAxioms] 76~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 77* CoAxioms and FamInsts are just like 78 DFunIds and ClsInsts 79 80* A CoAxiom is a System-FC thing: it can relate any two types 81 82* A FamInst is a Haskell source-language thing, corresponding 83 to a type/data family instance declaration. 84 - The FamInst contains a CoAxiom, which is the evidence 85 for the instance 86 87 - The LHS of the CoAxiom is always of form F ty1 .. tyn 88 where F is a type family 89-} 90 91data FamInst -- See Note [FamInsts and CoAxioms] 92 = FamInst { fi_axiom :: CoAxiom Unbranched -- The new coercion axiom 93 -- introduced by this family 94 -- instance 95 -- INVARIANT: apart from freshening (see below) 96 -- fi_tvs = cab_tvs of the (single) axiom branch 97 -- fi_cvs = cab_cvs ...ditto... 98 -- fi_tys = cab_lhs ...ditto... 99 -- fi_rhs = cab_rhs ...ditto... 100 101 , fi_flavor :: FamFlavor 102 103 -- Everything below here is a redundant, 104 -- cached version of the two things above 105 -- except that the TyVars are freshened 106 , fi_fam :: Name -- Family name 107 108 -- Used for "rough matching"; same idea as for class instances 109 -- See Note [Rough-match field] in GHC.Core.InstEnv 110 , fi_tcs :: [Maybe Name] -- Top of type args 111 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys 112 113 -- Used for "proper matching"; ditto 114 , fi_tvs :: [TyVar] -- Template tyvars for full match 115 , fi_cvs :: [CoVar] -- Template covars for full match 116 -- Like ClsInsts, these variables are always fresh 117 -- See Note [Template tyvars are fresh] in GHC.Core.InstEnv 118 119 , fi_tys :: [Type] -- The LHS type patterns 120 -- May be eta-reduced; see Note [Eta reduction for data families] 121 -- in GHC.Core.Coercion.Axiom 122 123 , fi_rhs :: Type -- the RHS, with its freshened vars 124 } 125 126data FamFlavor 127 = SynFamilyInst -- A synonym family 128 | DataFamilyInst TyCon -- A data family, with its representation TyCon 129 130{- 131Note [Arity of data families] 132~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 133Data family instances might legitimately be over- or under-saturated. 134 135Under-saturation has two potential causes: 136 U1) Eta reduction. See Note [Eta reduction for data families] in 137 GHC.Core.Coercion.Axiom. 138 U2) When the user has specified a return kind instead of written out patterns. 139 Example: 140 141 data family Sing (a :: k) 142 data instance Sing :: Bool -> Type 143 144 The data family tycon Sing has an arity of 2, the k and the a. But 145 the data instance has only one pattern, Bool (standing in for k). 146 This instance is equivalent to `data instance Sing (a :: Bool)`, but 147 without the last pattern, we have an under-saturated data family instance. 148 On its own, this example is not compelling enough to add support for 149 under-saturation, but U1 makes this feature more compelling. 150 151Over-saturation is also possible: 152 O1) If the data family's return kind is a type variable (see also #12369), 153 an instance might legitimately have more arguments than the family. 154 Example: 155 156 data family Fix :: (Type -> k) -> k 157 data instance Fix f = MkFix1 (f (Fix f)) 158 data instance Fix f x = MkFix2 (f (Fix f x) x) 159 160 In the first instance here, the k in the data family kind is chosen to 161 be Type. In the second, it's (Type -> Type). 162 163 However, we require that any over-saturation is eta-reducible. That is, 164 we require that any extra patterns be bare unrepeated type variables; 165 see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom. 166 Accordingly, the FamInst is never over-saturated. 167 168Why can we allow such flexibility for data families but not for type families? 169Because data families can be decomposed -- that is, they are generative and 170injective. A Type family is neither and so always must be applied to all its 171arguments. 172-} 173 174-- Obtain the axiom of a family instance 175famInstAxiom :: FamInst -> CoAxiom Unbranched 176famInstAxiom = fi_axiom 177 178-- Split the left-hand side of the FamInst 179famInstSplitLHS :: FamInst -> (TyCon, [Type]) 180famInstSplitLHS (FamInst { fi_axiom = axiom, fi_tys = lhs }) 181 = (coAxiomTyCon axiom, lhs) 182 183-- Get the RHS of the FamInst 184famInstRHS :: FamInst -> Type 185famInstRHS = fi_rhs 186 187-- Get the family TyCon of the FamInst 188famInstTyCon :: FamInst -> TyCon 189famInstTyCon = coAxiomTyCon . famInstAxiom 190 191-- Return the representation TyCons introduced by data family instances, if any 192famInstsRepTyCons :: [FamInst] -> [TyCon] 193famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis] 194 195-- Extracts the TyCon for this *data* (or newtype) instance 196famInstRepTyCon_maybe :: FamInst -> Maybe TyCon 197famInstRepTyCon_maybe fi 198 = case fi_flavor fi of 199 DataFamilyInst tycon -> Just tycon 200 SynFamilyInst -> Nothing 201 202dataFamInstRepTyCon :: FamInst -> TyCon 203dataFamInstRepTyCon fi 204 = case fi_flavor fi of 205 DataFamilyInst tycon -> tycon 206 SynFamilyInst -> pprPanic "dataFamInstRepTyCon" (ppr fi) 207 208{- 209************************************************************************ 210* * 211 Pretty printing 212* * 213************************************************************************ 214-} 215 216instance NamedThing FamInst where 217 getName = coAxiomName . fi_axiom 218 219instance Outputable FamInst where 220 ppr = pprFamInst 221 222pprFamInst :: FamInst -> SDoc 223-- Prints the FamInst as a family instance declaration 224-- NB: This function, FamInstEnv.pprFamInst, is used only for internal, 225-- debug printing. See GHC.Core.Ppr.TyThing.pprFamInst for printing for the user 226pprFamInst (FamInst { fi_flavor = flavor, fi_axiom = ax 227 , fi_tvs = tvs, fi_tys = tys, fi_rhs = rhs }) 228 = hang (ppr_tc_sort <+> text "instance" 229 <+> pprCoAxBranchUser (coAxiomTyCon ax) (coAxiomSingleBranch ax)) 230 2 (whenPprDebug debug_stuff) 231 where 232 ppr_tc_sort = case flavor of 233 SynFamilyInst -> text "type" 234 DataFamilyInst tycon 235 | isDataTyCon tycon -> text "data" 236 | isNewTyCon tycon -> text "newtype" 237 | isAbstractTyCon tycon -> text "data" 238 | otherwise -> text "WEIRD" <+> ppr tycon 239 240 debug_stuff = vcat [ text "Coercion axiom:" <+> ppr ax 241 , text "Tvs:" <+> ppr tvs 242 , text "LHS:" <+> ppr tys 243 , text "RHS:" <+> ppr rhs ] 244 245pprFamInsts :: [FamInst] -> SDoc 246pprFamInsts finsts = vcat (map pprFamInst finsts) 247 248{- 249Note [Lazy axiom match] 250~~~~~~~~~~~~~~~~~~~~~~~ 251It is Vitally Important that mkImportedFamInst is *lazy* in its axiom 252parameter. The axiom is loaded lazily, via a forkM, in GHC.IfaceToCore. Sometime 253later, mkImportedFamInst is called using that axiom. However, the axiom 254may itself depend on entities which are not yet loaded as of the time 255of the mkImportedFamInst. Thus, if mkImportedFamInst eagerly looks at the 256axiom, a dependency loop spontaneously appears and GHC hangs. The solution 257is simply for mkImportedFamInst never, ever to look inside of the axiom 258until everything else is good and ready to do so. We can assume that this 259readiness has been achieved when some other code pulls on the axiom in the 260FamInst. Thus, we pattern match on the axiom lazily (in the where clause, 261not in the parameter list) and we assert the consistency of names there 262also. 263-} 264 265-- Make a family instance representation from the information found in an 266-- interface file. In particular, we get the rough match info from the iface 267-- (instead of computing it here). 268mkImportedFamInst :: Name -- Name of the family 269 -> [Maybe Name] -- Rough match info 270 -> CoAxiom Unbranched -- Axiom introduced 271 -> FamInst -- Resulting family instance 272mkImportedFamInst fam mb_tcs axiom 273 = FamInst { 274 fi_fam = fam, 275 fi_tcs = mb_tcs, 276 fi_tvs = tvs, 277 fi_cvs = cvs, 278 fi_tys = tys, 279 fi_rhs = rhs, 280 fi_axiom = axiom, 281 fi_flavor = flavor } 282 where 283 -- See Note [Lazy axiom match] 284 ~(CoAxBranch { cab_lhs = tys 285 , cab_tvs = tvs 286 , cab_cvs = cvs 287 , cab_rhs = rhs }) = coAxiomSingleBranch axiom 288 289 -- Derive the flavor for an imported FamInst rather disgustingly 290 -- Maybe we should store it in the IfaceFamInst? 291 flavor = case splitTyConApp_maybe rhs of 292 Just (tc, _) 293 | Just ax' <- tyConFamilyCoercion_maybe tc 294 , ax' == axiom 295 -> DataFamilyInst tc 296 _ -> SynFamilyInst 297 298{- 299************************************************************************ 300* * 301 FamInstEnv 302* * 303************************************************************************ 304 305Note [FamInstEnv] 306~~~~~~~~~~~~~~~~~ 307A FamInstEnv maps a family name to the list of known instances for that family. 308 309The same FamInstEnv includes both 'data family' and 'type family' instances. 310Type families are reduced during type inference, but not data families; 311the user explains when to use a data family instance by using constructors 312and pattern matching. 313 314Nevertheless it is still useful to have data families in the FamInstEnv: 315 316 - For finding overlaps and conflicts 317 318 - For finding the representation type...see FamInstEnv.topNormaliseType 319 and its call site in GHC.Core.Opt.Simplify 320 321 - In standalone deriving instance Eq (T [Int]) we need to find the 322 representation type for T [Int] 323 324Note [Varying number of patterns for data family axioms] 325~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 326For data families, the number of patterns may vary between instances. 327For example 328 data family T a b 329 data instance T Int a = T1 a | T2 330 data instance T Bool [a] = T3 a 331 332Then we get a data type for each instance, and an axiom: 333 data TInt a = T1 a | T2 334 data TBoolList a = T3 a 335 336 axiom ax7 :: T Int ~ TInt -- Eta-reduced 337 axiom ax8 a :: T Bool [a] ~ TBoolList a 338 339These two axioms for T, one with one pattern, one with two; 340see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom 341 342Note [FamInstEnv determinism] 343~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 344We turn FamInstEnvs into a list in some places that don't directly affect 345the ABI. That happens in family consistency checks and when producing output 346for `:info`. Unfortunately that nondeterminism is nonlocal and it's hard 347to tell what it affects without following a chain of functions. It's also 348easy to accidentally make that nondeterminism affect the ABI. Furthermore 349the envs should be relatively small, so it should be free to use deterministic 350maps here. Testing with nofib and validate detected no difference between 351UniqFM and UniqDFM. 352See Note [Deterministic UniqFM]. 353-} 354 355-- Internally we sometimes index by Name instead of TyCon despite 356-- of what the type says. This is safe since 357-- getUnique (tyCon) == getUniqe (tcName tyCon) 358type FamInstEnv = UniqDFM TyCon FamilyInstEnv -- Maps a family to its instances 359 -- See Note [FamInstEnv] 360 -- See Note [FamInstEnv determinism] 361 362type FamInstEnvs = (FamInstEnv, FamInstEnv) 363 -- External package inst-env, Home-package inst-env 364 365newtype FamilyInstEnv 366 = FamIE [FamInst] -- The instances for a particular family, in any order 367 368instance Outputable FamilyInstEnv where 369 ppr (FamIE fs) = text "FamIE" <+> vcat (map ppr fs) 370 371-- | Index a FamInstEnv by the tyCons name. 372toNameInstEnv :: FamInstEnv -> UniqDFM Name FamilyInstEnv 373toNameInstEnv = unsafeCastUDFMKey 374 375-- | Create a FamInstEnv from Name indices. 376fromNameInstEnv :: UniqDFM Name FamilyInstEnv -> FamInstEnv 377fromNameInstEnv = unsafeCastUDFMKey 378 379-- INVARIANTS: 380-- * The fs_tvs are distinct in each FamInst 381-- of a range value of the map (so we can safely unify them) 382 383emptyFamInstEnvs :: (FamInstEnv, FamInstEnv) 384emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv) 385 386emptyFamInstEnv :: FamInstEnv 387emptyFamInstEnv = emptyUDFM 388 389famInstEnvElts :: FamInstEnv -> [FamInst] 390famInstEnvElts fi = [elt | FamIE elts <- eltsUDFM fi, elt <- elts] 391 -- See Note [FamInstEnv determinism] 392 393famInstEnvSize :: FamInstEnv -> Int 394famInstEnvSize = nonDetStrictFoldUDFM (\(FamIE elt) sum -> sum + length elt) 0 395 -- It's OK to use nonDetStrictFoldUDFM here since we're just computing the 396 -- size. 397 398familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst] 399familyInstances (pkg_fie, home_fie) fam 400 = get home_fie ++ get pkg_fie 401 where 402 get env = case lookupUDFM env fam of 403 Just (FamIE insts) -> insts 404 Nothing -> [] 405 406extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv 407extendFamInstEnvList inst_env fis = foldl' extendFamInstEnv inst_env fis 408 409extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv 410extendFamInstEnv inst_env 411 ins_item@(FamInst {fi_fam = cls_nm}) 412 = fromNameInstEnv $ addToUDFM_C add (toNameInstEnv inst_env) cls_nm (FamIE [ins_item]) 413 where 414 add (FamIE items) _ = FamIE (ins_item:items) 415 416{- 417************************************************************************ 418* * 419 Compatibility 420* * 421************************************************************************ 422 423Note [Apartness] 424~~~~~~~~~~~~~~~~ 425In dealing with closed type families, we must be able to check that one type 426will never reduce to another. This check is called /apartness/. The check 427is always between a target (which may be an arbitrary type) and a pattern. 428Here is how we do it: 429 430apart(target, pattern) = not (unify(flatten(target), pattern)) 431 432where flatten (implemented in flattenTys, below) converts all type-family 433applications into fresh variables. (See Note [Flattening].) 434 435Note [Compatibility] 436~~~~~~~~~~~~~~~~~~~~ 437Two patterns are /compatible/ if either of the following conditions hold: 4381) The patterns are apart. 4392) The patterns unify with a substitution S, and their right hand sides 440equal under that substitution. 441 442For open type families, only compatible instances are allowed. For closed 443type families, the story is slightly more complicated. Consider the following: 444 445type family F a where 446 F Int = Bool 447 F a = Int 448 449g :: Show a => a -> F a 450g x = length (show x) 451 452Should that type-check? No. We need to allow for the possibility that 'a' 453might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int 454only when we can be sure that 'a' is not Int. 455 456To achieve this, after finding a possible match within the equations, we have to 457go back to all previous equations and check that, under the 458substitution induced by the match, other branches are surely apart. (See 459Note [Apartness].) This is similar to what happens with class 460instance selection, when we need to guarantee that there is only a match and 461no unifiers. The exact algorithm is different here because the 462potentially-overlapping group is closed. 463 464As another example, consider this: 465 466type family G x where 467 G Int = Bool 468 G a = Double 469 470type family H y 471-- no instances 472 473Now, we want to simplify (G (H Char)). We can't, because (H Char) might later 474simplify to be Int. So, (G (H Char)) is stuck, for now. 475 476While everything above is quite sound, it isn't as expressive as we'd like. 477Consider this: 478 479type family J a where 480 J Int = Int 481 J a = a 482 483Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if 484b is instantiated with Int, but the RHSs coincide there, so it's all OK. 485 486So, the rule is this: when looking up a branch in a closed type family, we 487find a branch that matches the target, but then we make sure that the target 488is apart from every previous *incompatible* branch. We don't check the 489branches that are compatible with the matching branch, because they are either 490irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). 491 492Note [Compatibility of eta-reduced axioms] 493~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 494In newtype instances of data families we eta-reduce the axioms, 495See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom. This means that 496we sometimes need to test compatibility of two axioms that were eta-reduced to 497different degrees, e.g.: 498 499 500data family D a b c 501newtype instance D a Int c = DInt (Maybe a) 502 -- D a Int ~ Maybe 503 -- lhs = [a, Int] 504newtype instance D Bool Int Char = DIntChar Float 505 -- D Bool Int Char ~ Float 506 -- lhs = [Bool, Int, Char] 507 508These are obviously incompatible. We could detect this by saturating 509(eta-expanding) the shorter LHS with fresh tyvars until the lists are of 510equal length, but instead we can just remove the tail of the longer list, as 511those types will simply unify with the freshly introduced tyvars. 512 513By doing this, in case the LHS are unifiable, the yielded substitution won't 514mention the tyvars that appear in the tail we dropped off, and we might try 515to test equality RHSes of different kinds, but that's fine since this case 516occurs only for data families, where the RHS is a unique tycon and the equality 517fails anyway. 518-} 519 520-- See Note [Compatibility] 521compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool 522compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) 523 (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) 524 = let (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2 525 -- See Note [Compatibility of eta-reduced axioms] 526 in case tcUnifyTysFG (const BindMe) commonlhs1 commonlhs2 of 527 SurelyApart -> True 528 Unifiable subst 529 | Type.substTyAddInScope subst rhs1 `eqType` 530 Type.substTyAddInScope subst rhs2 531 -> True 532 _ -> False 533 534-- | Result of testing two type family equations for injectiviy. 535data InjectivityCheckResult 536 = InjectivityAccepted 537 -- ^ Either RHSs are distinct or unification of RHSs leads to unification of 538 -- LHSs 539 | InjectivityUnified CoAxBranch CoAxBranch 540 -- ^ RHSs unify but LHSs don't unify under that substitution. Relevant for 541 -- closed type families where equation after unification might be 542 -- overlpapped (in which case it is OK if they don't unify). Constructor 543 -- stores axioms after unification. 544 545-- | Check whether two type family axioms don't violate injectivity annotation. 546injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch 547 -> InjectivityCheckResult 548injectiveBranches injectivity 549 ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) 550 ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) 551 -- See Note [Verifying injectivity annotation], case 1. 552 = let getInjArgs = filterByList injectivity 553 in case tcUnifyTyWithTFs True rhs1 rhs2 of -- True = two-way pre-unification 554 Nothing -> InjectivityAccepted 555 -- RHS are different, so equations are injective. 556 -- This is case 1A from Note [Verifying injectivity annotation] 557 Just subst -> -- RHS unify under a substitution 558 let lhs1Subst = Type.substTys subst (getInjArgs lhs1) 559 lhs2Subst = Type.substTys subst (getInjArgs lhs2) 560 -- If LHSs are equal under the substitution used for RHSs then this pair 561 -- of equations does not violate injectivity annotation. If LHSs are not 562 -- equal under that substitution then this pair of equations violates 563 -- injectivity annotation, but for closed type families it still might 564 -- be the case that one LHS after substitution is unreachable. 565 in if eqTypes lhs1Subst lhs2Subst -- check case 1B1 from Note. 566 then InjectivityAccepted 567 else InjectivityUnified ( ax1 { cab_lhs = Type.substTys subst lhs1 568 , cab_rhs = Type.substTy subst rhs1 }) 569 ( ax2 { cab_lhs = Type.substTys subst lhs2 570 , cab_rhs = Type.substTy subst rhs2 }) 571 -- payload of InjectivityUnified used only for check 1B2, only 572 -- for closed type families 573 574-- takes a CoAxiom with unknown branch incompatibilities and computes 575-- the compatibilities 576-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom 577computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch] 578computeAxiomIncomps branches 579 = snd (mapAccumL go [] branches) 580 where 581 go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch) 582 go prev_brs cur_br 583 = (cur_br : prev_brs, new_br) 584 where 585 new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br } 586 587 mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch] 588 mk_incomps prev_brs cur_br 589 = filter (not . compatibleBranches cur_br) prev_brs 590 591{- 592************************************************************************ 593* * 594 Constructing axioms 595 These functions are here because tidyType / tcUnifyTysFG 596 are not available in GHC.Core.Coercion.Axiom 597 598 Also computeAxiomIncomps is too sophisticated for CoAxiom 599* * 600************************************************************************ 601 602Note [Tidy axioms when we build them] 603~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 604Like types and classes, we build axioms fully quantified over all 605their variables, and tidy them when we build them. For example, 606we print out axioms and don't want to print stuff like 607 F k k a b = ... 608Instead we must tidy those kind variables. See #7524. 609 610We could instead tidy when we print, but that makes it harder to get 611things like injectivity errors to come out right. Danger of 612 Type family equation violates injectivity annotation. 613 Kind variable ‘k’ cannot be inferred from the right-hand side. 614 In the type family equation: 615 PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2 616 617Note [Always number wildcard types in CoAxBranch] 618~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 619Consider the following example (from the DataFamilyInstanceLHS test case): 620 621 data family Sing (a :: k) 622 data instance Sing (_ :: MyKind) where 623 SingA :: Sing A 624 SingB :: Sing B 625 626If we're not careful during tidying, then when this program is compiled with 627-ddump-types, we'll get the following information: 628 629 COERCION AXIOMS 630 axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 :: 631 Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _ 632 633It's misleading to have a wildcard type appearing on the RHS like 634that. To avoid this issue, when building a CoAxiom (which is what eventually 635gets printed above), we tidy all the variables in an env that already contains 636'_'. Thus, any variable named '_' will be renamed, giving us the nicer output 637here: 638 639 COERCION AXIOMS 640 axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 :: 641 Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1 642 643Which is at least legal syntax. 644 645See also Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom; note that we 646are tidying (changing OccNames only), not freshening, in accordance with 647that Note. 648-} 649 650-- all axiom roles are Nominal, as this is only used with type families 651mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars 652 -> [TyVar] -- Extra eta tyvars 653 -> [CoVar] -- possibly stale covars 654 -> [Type] -- LHS patterns 655 -> Type -- RHS 656 -> [Role] 657 -> SrcSpan 658 -> CoAxBranch 659mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc 660 = CoAxBranch { cab_tvs = tvs' 661 , cab_eta_tvs = eta_tvs' 662 , cab_cvs = cvs' 663 , cab_lhs = tidyTypes env lhs 664 , cab_roles = roles 665 , cab_rhs = tidyType env rhs 666 , cab_loc = loc 667 , cab_incomps = placeHolderIncomps } 668 where 669 (env1, tvs') = tidyVarBndrs init_tidy_env tvs 670 (env2, eta_tvs') = tidyVarBndrs env1 eta_tvs 671 (env, cvs') = tidyVarBndrs env2 cvs 672 -- See Note [Tidy axioms when we build them] 673 -- See also Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom 674 675 init_occ_env = initTidyOccEnv [mkTyVarOcc "_"] 676 init_tidy_env = mkEmptyTidyEnv init_occ_env 677 -- See Note [Always number wildcard types in CoAxBranch] 678 679-- all of the following code is here to avoid mutual dependencies with 680-- Coercion 681mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched 682mkBranchedCoAxiom ax_name fam_tc branches 683 = CoAxiom { co_ax_unique = nameUnique ax_name 684 , co_ax_name = ax_name 685 , co_ax_tc = fam_tc 686 , co_ax_role = Nominal 687 , co_ax_implicit = False 688 , co_ax_branches = manyBranches (computeAxiomIncomps branches) } 689 690mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched 691mkUnbranchedCoAxiom ax_name fam_tc branch 692 = CoAxiom { co_ax_unique = nameUnique ax_name 693 , co_ax_name = ax_name 694 , co_ax_tc = fam_tc 695 , co_ax_role = Nominal 696 , co_ax_implicit = False 697 , co_ax_branches = unbranched (branch { cab_incomps = [] }) } 698 699mkSingleCoAxiom :: Role -> Name 700 -> [TyVar] -> [TyVar] -> [CoVar] 701 -> TyCon -> [Type] -> Type 702 -> CoAxiom Unbranched 703-- Make a single-branch CoAxiom, including making the branch itself 704-- Used for both type family (Nominal) and data family (Representational) 705-- axioms, hence passing in the Role 706mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty 707 = CoAxiom { co_ax_unique = nameUnique ax_name 708 , co_ax_name = ax_name 709 , co_ax_tc = fam_tc 710 , co_ax_role = role 711 , co_ax_implicit = False 712 , co_ax_branches = unbranched (branch { cab_incomps = [] }) } 713 where 714 branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty 715 (map (const Nominal) tvs) 716 (getSrcSpan ax_name) 717 718-- | Create a coercion constructor (axiom) suitable for the given 719-- newtype 'TyCon'. The 'Name' should be that of a new coercion 720-- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and 721-- the type the appropriate right hand side of the @newtype@, with 722-- the free variables a subset of those 'TyVar's. 723mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched 724mkNewTypeCoAxiom name tycon tvs roles rhs_ty 725 = CoAxiom { co_ax_unique = nameUnique name 726 , co_ax_name = name 727 , co_ax_implicit = True -- See Note [Implicit axioms] in GHC.Core.TyCon 728 , co_ax_role = Representational 729 , co_ax_tc = tycon 730 , co_ax_branches = unbranched (branch { cab_incomps = [] }) } 731 where 732 branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty 733 roles (getSrcSpan name) 734 735{- 736************************************************************************ 737* * 738 Looking up a family instance 739* * 740************************************************************************ 741 742@lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match. 743Multiple matches are only possible in case of type families (not data 744families), and then, it doesn't matter which match we choose (as the 745instances are guaranteed confluent). 746 747We return the matching family instances and the type instance at which it 748matches. For example, if we lookup 'T [Int]' and have a family instance 749 750 data instance T [a] = .. 751 752desugared to 753 754 data :R42T a = .. 755 coe :Co:R42T a :: T [a] ~ :R42T a 756 757we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'. 758-} 759 760-- when matching a type family application, we get a FamInst, 761-- and the list of types the axiom should be applied to 762data FamInstMatch = FamInstMatch { fim_instance :: FamInst 763 , fim_tys :: [Type] 764 , fim_cos :: [Coercion] 765 } 766 -- See Note [Over-saturated matches] 767 768instance Outputable FamInstMatch where 769 ppr (FamInstMatch { fim_instance = inst 770 , fim_tys = tys 771 , fim_cos = cos }) 772 = text "match with" <+> parens (ppr inst) <+> ppr tys <+> ppr cos 773 774lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst] 775lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc 776 = get pkg_ie ++ get home_ie 777 where 778 get ie = case lookupUDFM ie fam_tc of 779 Nothing -> [] 780 Just (FamIE fis) -> fis 781 782lookupFamInstEnv 783 :: FamInstEnvs 784 -> TyCon -> [Type] -- What we are looking for 785 -> [FamInstMatch] -- Successful matches 786-- Precondition: the tycon is saturated (or over-saturated) 787 788lookupFamInstEnv 789 = lookup_fam_inst_env match 790 where 791 match _ _ tpl_tys tys = tcMatchTys tpl_tys tys 792 793lookupFamInstEnvConflicts 794 :: FamInstEnvs 795 -> FamInst -- Putative new instance 796 -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field) 797-- E.g. when we are about to add 798-- f : type instance F [a] = a->a 799-- we do (lookupFamInstConflicts f [b]) 800-- to find conflicting matches 801-- 802-- Precondition: the tycon is saturated (or over-saturated) 803 804lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom }) 805 = lookup_fam_inst_env my_unify envs fam tys 806 where 807 (fam, tys) = famInstSplitLHS fam_inst 808 -- In example above, fam tys' = F [b] 809 810 my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _ 811 = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs, 812 (ppr fam <+> ppr tys) $$ 813 (ppr tpl_tvs <+> ppr tpl_tys) ) 814 -- Unification will break badly if the variables overlap 815 -- They shouldn't because we allocate separate uniques for them 816 if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch 817 then Nothing 818 else Just noSubst 819 -- Note [Family instance overlap conflicts] 820 821 noSubst = panic "lookupFamInstEnvConflicts noSubst" 822 new_branch = coAxiomSingleBranch new_axiom 823 824-------------------------------------------------------------------------------- 825-- Type family injectivity checking bits -- 826-------------------------------------------------------------------------------- 827 828{- Note [Verifying injectivity annotation] 829~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 830 831Injectivity means that the RHS of a type family uniquely determines the LHS (see 832Note [Type inference for type families with injectivity]). The user informs us about 833injectivity using an injectivity annotation and it is GHC's task to verify that 834this annotation is correct w.r.t. type family equations. Whenever we see a new 835equation of a type family we need to make sure that adding this equation to the 836already known equations of a type family does not violate the injectivity annotation 837supplied by the user (see Note [Injectivity annotation]). Of course if the type 838family has no injectivity annotation then no check is required. But if a type 839family has injectivity annotation we need to make sure that the following 840conditions hold: 841 8421. For each pair of *different* equations of a type family, one of the following 843 conditions holds: 844 845 A: RHSs are different. (Check done in GHC.Core.FamInstEnv.injectiveBranches) 846 847 B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution 848 then it must be possible to unify the LHSs under the same substitution. 849 Example: 850 851 type family FunnyId a = r | r -> a 852 type instance FunnyId Int = Int 853 type instance FunnyId a = a 854 855 RHSs of these two equations unify under [ a |-> Int ] substitution. 856 Under this substitution LHSs are equal therefore these equations don't 857 violate injectivity annotation. (Check done in GHC.Core.FamInstEnv.injectiveBranches) 858 859 B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some 860 substitution then either the LHSs unify under the same substitution or 861 the LHS of the latter equation is overlapped by earlier equations. 862 Example 1: 863 864 type family SwapIntChar a = r | r -> a where 865 SwapIntChar Int = Char 866 SwapIntChar Char = Int 867 SwapIntChar a = a 868 869 Say we are checking the last two equations. RHSs unify under [ a |-> 870 Int ] substitution but LHSs don't. So we apply the substitution to LHS 871 of last equation and check whether it is overlapped by any of previous 872 equations. Since it is overlapped by the first equation we conclude 873 that pair of last two equations does not violate injectivity 874 annotation. (Check done in GHC.Tc.Validity.checkValidCoAxiom#gather_conflicts) 875 876 A special case of B is when RHSs unify with an empty substitution ie. they 877 are identical. 878 879 If any of the above two conditions holds we conclude that the pair of 880 equations does not violate injectivity annotation. But if we find a pair 881 of equations where neither of the above holds we report that this pair 882 violates injectivity annotation because for a given RHS we don't have a 883 unique LHS. (Note that (B) actually implies (A).) 884 885 Note that we only take into account these LHS patterns that were declared 886 as injective. 887 8882. If an RHS of a type family equation is a bare type variable then 889 all LHS variables (including implicit kind variables) also have to be bare. 890 In other words, this has to be a sole equation of that type family and it has 891 to cover all possible patterns. So for example this definition will be 892 rejected: 893 894 type family W1 a = r | r -> a 895 type instance W1 [a] = a 896 897 If it were accepted we could call `W1 [W1 Int]`, which would reduce to 898 `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`, 899 which is bogus. Checked FamInst.bareTvInRHSViolated. 900 9013. If the RHS of a type family equation is a type family application then the type 902 family is rejected as not injective. This is checked by FamInst.isTFHeaded. 903 9044. If a LHS type variable that is declared as injective is not mentioned in an 905 injective position in the RHS then the type family is rejected as not 906 injective. "Injective position" means either an argument to a type 907 constructor or argument to a type family on injective position. 908 There are subtleties here. See Note [Coverage condition for injective type families] 909 in GHC.Tc.Instance.Family. 910 911Check (1) must be done for all family instances (transitively) imported. Other 912checks (2-4) should be done just for locally written equations, as they are checks 913involving just a single equation, not about interactions. Doing the other checks for 914imported equations led to #17405, as the behavior of check (4) depends on 915-XUndecidableInstances (see Note [Coverage condition for injective type families] in 916FamInst), which may vary between modules. 917 918See also Note [Injective type families] in GHC.Core.TyCon 919-} 920 921 922-- | Check whether an open type family equation can be added to already existing 923-- instance environment without causing conflicts with supplied injectivity 924-- annotations. Returns list of conflicting axioms (type instance 925-- declarations). 926lookupFamInstEnvInjectivityConflicts 927 :: [Bool] -- injectivity annotation for this type family instance 928 -- INVARIANT: list contains at least one True value 929 -> FamInstEnvs -- all type instances seens so far 930 -> FamInst -- new type instance that we're checking 931 -> [CoAxBranch] -- conflicting instance declarations 932lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie) 933 fam_inst@(FamInst { fi_axiom = new_axiom }) 934 -- See Note [Verifying injectivity annotation]. This function implements 935 -- check (1.B1) for open type families described there. 936 = lookup_inj_fam_conflicts home_ie ++ lookup_inj_fam_conflicts pkg_ie 937 where 938 fam = famInstTyCon fam_inst 939 new_branch = coAxiomSingleBranch new_axiom 940 941 -- filtering function used by `lookup_inj_fam_conflicts` to check whether 942 -- a pair of equations conflicts with the injectivity annotation. 943 isInjConflict (FamInst { fi_axiom = old_axiom }) 944 | InjectivityAccepted <- 945 injectiveBranches injList (coAxiomSingleBranch old_axiom) new_branch 946 = False -- no conflict 947 | otherwise = True 948 949 lookup_inj_fam_conflicts ie 950 | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUDFM ie fam 951 = map (coAxiomSingleBranch . fi_axiom) $ 952 filter isInjConflict insts 953 | otherwise = [] 954 955 956-------------------------------------------------------------------------------- 957-- Type family overlap checking bits -- 958-------------------------------------------------------------------------------- 959 960{- 961Note [Family instance overlap conflicts] 962~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 963- In the case of data family instances, any overlap is fundamentally a 964 conflict (as these instances imply injective type mappings). 965 966- In the case of type family instances, overlap is admitted as long as 967 the right-hand sides of the overlapping rules coincide under the 968 overlap substitution. eg 969 type instance F a Int = a 970 type instance F Int b = b 971 These two overlap on (F Int Int) but then both RHSs are Int, 972 so all is well. We require that they are syntactically equal; 973 anything else would be difficult to test for at this stage. 974-} 975 976------------------------------------------------------------ 977-- Might be a one-way match or a unifier 978type MatchFun = FamInst -- The FamInst template 979 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst 980 -> [Type] -- Target to match against 981 -> Maybe TCvSubst 982 983lookup_fam_inst_env' -- The worker, local to this module 984 :: MatchFun 985 -> FamInstEnv 986 -> TyCon -> [Type] -- What we are looking for 987 -> [FamInstMatch] 988lookup_fam_inst_env' match_fun ie fam match_tys 989 | isOpenFamilyTyCon fam 990 , Just (FamIE insts) <- lookupUDFM ie fam 991 = find insts -- The common case 992 | otherwise = [] 993 where 994 995 find [] = [] 996 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs 997 , fi_tys = tpl_tys }) : rest) 998 -- Fast check for no match, uses the "rough match" fields 999 | instanceCantMatch rough_tcs mb_tcs 1000 = find rest 1001 1002 -- Proper check 1003 | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1 1004 = (FamInstMatch { fim_instance = item 1005 , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 1006 , fim_cos = ASSERT( all (isJust . lookupCoVar subst) tpl_cvs ) 1007 substCoVars subst tpl_cvs 1008 }) 1009 : find rest 1010 1011 -- No match => try next 1012 | otherwise 1013 = find rest 1014 where 1015 (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys 1016 1017 -- Precondition: the tycon is saturated (or over-saturated) 1018 1019 -- Deal with over-saturation 1020 -- See Note [Over-saturated matches] 1021 split_tys tpl_tys 1022 | isTypeFamilyTyCon fam 1023 = pre_rough_split_tys 1024 1025 | otherwise 1026 = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys 1027 rough_tcs = roughMatchTcs match_tys1 1028 in (rough_tcs, match_tys1, match_tys2) 1029 1030 (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys 1031 pre_rough_split_tys 1032 = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2) 1033 1034lookup_fam_inst_env -- The worker, local to this module 1035 :: MatchFun 1036 -> FamInstEnvs 1037 -> TyCon -> [Type] -- What we are looking for 1038 -> [FamInstMatch] -- Successful matches 1039 1040-- Precondition: the tycon is saturated (or over-saturated) 1041 1042lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys 1043 = lookup_fam_inst_env' match_fun home_ie fam tys 1044 ++ lookup_fam_inst_env' match_fun pkg_ie fam tys 1045 1046{- 1047Note [Over-saturated matches] 1048~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1049It's ok to look up an over-saturated type constructor. E.g. 1050 type family F a :: * -> * 1051 type instance F (a,b) = Either (a->b) 1052 1053The type instance gives rise to a newtype TyCon (at a higher kind 1054which you can't do in Haskell!): 1055 newtype FPair a b = FP (Either (a->b)) 1056 1057Then looking up (F (Int,Bool) Char) will return a FamInstMatch 1058 (FPair, [Int,Bool,Char]) 1059The "extra" type argument [Char] just stays on the end. 1060 1061We handle data families and type families separately here: 1062 1063 * For type families, all instances of a type family must have the 1064 same arity, so we can precompute the split between the match_tys 1065 and the overflow tys. This is done in pre_rough_split_tys. 1066 1067 * For data family instances, though, we need to re-split for each 1068 instance, because the breakdown might be different for each 1069 instance. Why? Because of eta reduction; see 1070 Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom. 1071-} 1072 1073-- checks if one LHS is dominated by a list of other branches 1074-- in other words, if an application would match the first LHS, it is guaranteed 1075-- to match at least one of the others. The RHSs are ignored. 1076-- This algorithm is conservative: 1077-- True -> the LHS is definitely covered by the others 1078-- False -> no information 1079-- It is currently (Oct 2012) used only for generating errors for 1080-- inaccessible branches. If these errors go unreported, no harm done. 1081-- This is defined here to avoid a dependency from CoAxiom to Unify 1082isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool 1083isDominatedBy branch branches 1084 = or $ map match branches 1085 where 1086 lhs = coAxBranchLHS branch 1087 match (CoAxBranch { cab_lhs = tys }) 1088 = isJust $ tcMatchTys tys lhs 1089 1090{- 1091************************************************************************ 1092* * 1093 Choosing an axiom application 1094* * 1095************************************************************************ 1096 1097The lookupFamInstEnv function does a nice job for *open* type families, 1098but we also need to handle closed ones when normalising a type: 1099-} 1100 1101reduceTyFamApp_maybe :: FamInstEnvs 1102 -> Role -- Desired role of result coercion 1103 -> TyCon -> [Type] 1104 -> Maybe (Coercion, Type) 1105-- Attempt to do a *one-step* reduction of a type-family application 1106-- but *not* newtypes 1107-- Works on type-synonym families always; data-families only if 1108-- the role we seek is representational 1109-- It does *not* normalise the type arguments first, so this may not 1110-- go as far as you want. If you want normalised type arguments, 1111-- use topReduceTyFamApp_maybe 1112-- 1113-- The TyCon can be oversaturated. 1114-- Works on both open and closed families 1115-- 1116-- Always returns a *homogeneous* coercion -- type family reductions are always 1117-- homogeneous 1118reduceTyFamApp_maybe envs role tc tys 1119 | Phantom <- role 1120 = Nothing 1121 1122 | case role of 1123 Representational -> isOpenFamilyTyCon tc 1124 _ -> isOpenTypeFamilyTyCon tc 1125 -- If we seek a representational coercion 1126 -- (e.g. the call in topNormaliseType_maybe) then we can 1127 -- unwrap data families as well as type-synonym families; 1128 -- otherwise only type-synonym families 1129 , FamInstMatch { fim_instance = FamInst { fi_axiom = ax } 1130 , fim_tys = inst_tys 1131 , fim_cos = inst_cos } : _ <- lookupFamInstEnv envs tc tys 1132 -- NB: Allow multiple matches because of compatible overlap 1133 1134 = let co = mkUnbranchedAxInstCo role ax inst_tys inst_cos 1135 ty = coercionRKind co 1136 in Just (co, ty) 1137 1138 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc 1139 , Just (ind, inst_tys, inst_cos) <- chooseBranch ax tys 1140 = let co = mkAxInstCo role ax ind inst_tys inst_cos 1141 ty = coercionRKind co 1142 in Just (co, ty) 1143 1144 | Just ax <- isBuiltInSynFamTyCon_maybe tc 1145 , Just (coax,ts,ty) <- sfMatchFam ax tys 1146 = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts) 1147 in Just (co, ty) 1148 1149 | otherwise 1150 = Nothing 1151 1152-- The axiom can be oversaturated. (Closed families only.) 1153chooseBranch :: CoAxiom Branched -> [Type] 1154 -> Maybe (BranchIndex, [Type], [Coercion]) -- found match, with args 1155chooseBranch axiom tys 1156 = do { let num_pats = coAxiomNumPats axiom 1157 (target_tys, extra_tys) = splitAt num_pats tys 1158 branches = coAxiomBranches axiom 1159 ; (ind, inst_tys, inst_cos) 1160 <- findBranch (unMkBranches branches) target_tys 1161 ; return ( ind, inst_tys `chkAppend` extra_tys, inst_cos ) } 1162 1163-- The axiom must *not* be oversaturated 1164findBranch :: Array BranchIndex CoAxBranch 1165 -> [Type] 1166 -> Maybe (BranchIndex, [Type], [Coercion]) 1167 -- coercions relate requested types to returned axiom LHS at role N 1168findBranch branches target_tys 1169 = foldr go Nothing (assocs branches) 1170 where 1171 go :: (BranchIndex, CoAxBranch) 1172 -> Maybe (BranchIndex, [Type], [Coercion]) 1173 -> Maybe (BranchIndex, [Type], [Coercion]) 1174 go (index, branch) other 1175 = let (CoAxBranch { cab_tvs = tpl_tvs, cab_cvs = tpl_cvs 1176 , cab_lhs = tpl_lhs 1177 , cab_incomps = incomps }) = branch 1178 in_scope = mkInScopeSet (unionVarSets $ 1179 map (tyCoVarsOfTypes . coAxBranchLHS) incomps) 1180 -- See Note [Flattening] below 1181 flattened_target = flattenTys in_scope target_tys 1182 in case tcMatchTys tpl_lhs target_tys of 1183 Just subst -- matching worked. now, check for apartness. 1184 | apartnessCheck flattened_target branch 1185 -> -- matching worked & we're apart from all incompatible branches. 1186 -- success 1187 ASSERT( all (isJust . lookupCoVar subst) tpl_cvs ) 1188 Just (index, substTyVars subst tpl_tvs, substCoVars subst tpl_cvs) 1189 1190 -- failure. keep looking 1191 _ -> other 1192 1193-- | Do an apartness check, as described in the "Closed Type Families" paper 1194-- (POPL '14). This should be used when determining if an equation 1195-- ('CoAxBranch') of a closed type family can be used to reduce a certain target 1196-- type family application. 1197apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure 1198 -- they're flattened! See Note [Flattening]. 1199 -- (NB: This "flat" is a different 1200 -- "flat" than is used in GHC.Tc.Solver.Flatten.) 1201 -> CoAxBranch -- ^ the candidate equation we wish to use 1202 -- Precondition: this matches the target 1203 -> Bool -- ^ True <=> equation can fire 1204apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps }) 1205 = all (isSurelyApart 1206 . tcUnifyTysFG (const BindMe) flattened_target 1207 . coAxBranchLHS) incomps 1208 where 1209 isSurelyApart SurelyApart = True 1210 isSurelyApart _ = False 1211 1212{- 1213************************************************************************ 1214* * 1215 Looking up a family instance 1216* * 1217************************************************************************ 1218 1219Note [Normalising types] 1220~~~~~~~~~~~~~~~~~~~~~~~~ 1221The topNormaliseType function removes all occurrences of type families 1222and newtypes from the top-level structure of a type. normaliseTcApp does 1223the type family lookup and is fairly straightforward. normaliseType is 1224a little more involved. 1225 1226The complication comes from the fact that a type family might be used in the 1227kind of a variable bound in a forall. We wish to remove this type family 1228application, but that means coming up with a fresh variable (with the new 1229kind). Thus, we need a substitution to be built up as we recur through the 1230type. However, an ordinary TCvSubst just won't do: when we hit a type variable 1231whose kind has changed during normalisation, we need both the new type 1232variable *and* the coercion. We could conjure up a new VarEnv with just this 1233property, but a usable substitution environment already exists: 1234LiftingContexts from the liftCoSubst family of functions, defined in GHC.Core.Coercion. 1235A LiftingContext maps a type variable to a coercion and a coercion variable to 1236a pair of coercions. Let's ignore coercion variables for now. Because the 1237coercion a type variable maps to contains the destination type (via 1238coercionKind), we don't need to store that destination type separately. Thus, 1239a LiftingContext has what we need: a map from type variables to (Coercion, 1240Type) pairs. 1241 1242We also benefit because we can piggyback on the liftCoSubstVarBndr function to 1243deal with binders. However, I had to modify that function to work with this 1244application. Thus, we now have liftCoSubstVarBndrUsing, which takes 1245a function used to process the kind of the binder. We don't wish 1246to lift the kind, but instead normalise it. So, we pass in a callback function 1247that processes the kind of the binder. 1248 1249After that brilliant explanation of all this, I'm sure you've forgotten the 1250dangling reference to coercion variables. What do we do with those? Nothing at 1251all. The point of normalising types is to remove type family applications, but 1252there's no sense in removing these from coercions. We would just get back a 1253new coercion witnessing the equality between the same types as the original 1254coercion. Because coercions are irrelevant anyway, there is no point in doing 1255this. So, whenever we encounter a coercion, we just say that it won't change. 1256That's what the CoercionTy case is doing within normalise_type. 1257 1258Note [Normalisation and type synonyms] 1259~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1260We need to be a bit careful about normalising in the presence of type 1261synonyms (#13035). Suppose S is a type synonym, and we have 1262 S t1 t2 1263If S is family-free (on its RHS) we can just normalise t1 and t2 and 1264reconstruct (S t1' t2'). Expanding S could not reveal any new redexes 1265because type families are saturated. 1266 1267But if S has a type family on its RHS we expand /before/ normalising 1268the args t1, t2. If we normalise t1, t2 first, we'll re-normalise them 1269after expansion, and that can lead to /exponential/ behaviour; see #13035. 1270 1271Notice, though, that expanding first can in principle duplicate t1,t2, 1272which might contain redexes. I'm sure you could conjure up an exponential 1273case by that route too, but it hasn't happened in practice yet! 1274-} 1275 1276topNormaliseType :: FamInstEnvs -> Type -> Type 1277topNormaliseType env ty = case topNormaliseType_maybe env ty of 1278 Just (_co, ty') -> ty' 1279 Nothing -> ty 1280 1281topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type) 1282 1283-- ^ Get rid of *outermost* (or toplevel) 1284-- * type function redex 1285-- * data family redex 1286-- * newtypes 1287-- returning an appropriate Representational coercion. Specifically, if 1288-- topNormaliseType_maybe env ty = Just (co, ty') 1289-- then 1290-- (a) co :: ty ~R ty' 1291-- (b) ty' is not a newtype, and is not a type-family or data-family redex 1292-- 1293-- However, ty' can be something like (Maybe (F ty)), where 1294-- (F ty) is a redex. 1295-- 1296-- Always operates homogeneously: the returned type has the same kind as the 1297-- original type, and the returned coercion is always homogeneous. 1298topNormaliseType_maybe env ty 1299 = do { ((co, mkind_co), nty) <- topNormaliseTypeX stepper combine ty 1300 ; return $ case mkind_co of 1301 MRefl -> (co, nty) 1302 MCo kind_co -> let nty_casted = nty `mkCastTy` mkSymCo kind_co 1303 final_co = mkCoherenceRightCo Representational nty 1304 (mkSymCo kind_co) co 1305 in (final_co, nty_casted) } 1306 where 1307 stepper = unwrapNewTypeStepper' `composeSteppers` tyFamStepper 1308 1309 combine (c1, mc1) (c2, mc2) = (c1 `mkTransCo` c2, mc1 `mkTransMCo` mc2) 1310 1311 unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN) 1312 unwrapNewTypeStepper' rec_nts tc tys 1313 = mapStepResult (, MRefl) $ unwrapNewTypeStepper rec_nts tc tys 1314 1315 -- second coercion below is the kind coercion relating the original type's kind 1316 -- to the normalised type's kind 1317 tyFamStepper :: NormaliseStepper (Coercion, MCoercionN) 1318 tyFamStepper rec_nts tc tys -- Try to step a type/data family 1319 = case topReduceTyFamApp_maybe env tc tys of 1320 Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, MCo res_co) 1321 _ -> NS_Done 1322 1323--------------- 1324normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type) 1325-- See comments on normaliseType for the arguments of this function 1326normaliseTcApp env role tc tys 1327 = initNormM env role (tyCoVarsOfTypes tys) $ 1328 normalise_tc_app tc tys 1329 1330-- See Note [Normalising types] about the LiftingContext 1331normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type) 1332normalise_tc_app tc tys 1333 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys 1334 , not (isFamFreeTyCon tc) -- Expand and try again 1335 = -- A synonym with type families in the RHS 1336 -- Expand and try again 1337 -- See Note [Normalisation and type synonyms] 1338 normalise_type (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys') 1339 1340 | isFamilyTyCon tc 1341 = -- A type-family application 1342 do { env <- getEnv 1343 ; role <- getRole 1344 ; (args_co, ntys, res_co) <- normalise_tc_args tc tys 1345 ; case reduceTyFamApp_maybe env role tc ntys of 1346 Just (first_co, ty') 1347 -> do { (rest_co,nty) <- normalise_type ty' 1348 ; return (assemble_result role nty 1349 (args_co `mkTransCo` first_co `mkTransCo` rest_co) 1350 res_co) } 1351 _ -> -- No unique matching family instance exists; 1352 -- we do not do anything 1353 return (assemble_result role (mkTyConApp tc ntys) args_co res_co) } 1354 1355 | otherwise 1356 = -- A synonym with no type families in the RHS; or data type etc 1357 -- Just normalise the arguments and rebuild 1358 do { (args_co, ntys, res_co) <- normalise_tc_args tc tys 1359 ; role <- getRole 1360 ; return (assemble_result role (mkTyConApp tc ntys) args_co res_co) } 1361 1362 where 1363 assemble_result :: Role -- r, ambient role in NormM monad 1364 -> Type -- nty, result type, possibly of changed kind 1365 -> Coercion -- orig_ty ~r nty, possibly heterogeneous 1366 -> CoercionN -- typeKind(orig_ty) ~N typeKind(nty) 1367 -> (Coercion, Type) -- (co :: orig_ty ~r nty_casted, nty_casted) 1368 -- where nty_casted has same kind as orig_ty 1369 assemble_result r nty orig_to_nty kind_co 1370 = ( final_co, nty_old_kind ) 1371 where 1372 nty_old_kind = nty `mkCastTy` mkSymCo kind_co 1373 final_co = mkCoherenceRightCo r nty (mkSymCo kind_co) orig_to_nty 1374 1375--------------- 1376-- | Try to simplify a type-family application, by *one* step 1377-- If topReduceTyFamApp_maybe env r F tys = Just (co, rhs, res_co) 1378-- then co :: F tys ~R# rhs 1379-- res_co :: typeKind(F tys) ~ typeKind(rhs) 1380-- Type families and data families; always Representational role 1381topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type] 1382 -> Maybe (Coercion, Type, Coercion) 1383topReduceTyFamApp_maybe envs fam_tc arg_tys 1384 | isFamilyTyCon fam_tc -- type families and data families 1385 , Just (co, rhs) <- reduceTyFamApp_maybe envs role fam_tc ntys 1386 = Just (args_co `mkTransCo` co, rhs, res_co) 1387 | otherwise 1388 = Nothing 1389 where 1390 role = Representational 1391 (args_co, ntys, res_co) = initNormM envs role (tyCoVarsOfTypes arg_tys) $ 1392 normalise_tc_args fam_tc arg_tys 1393 1394normalise_tc_args :: TyCon -> [Type] -- tc tys 1395 -> NormM (Coercion, [Type], CoercionN) 1396 -- (co, new_tys), where 1397 -- co :: tc tys ~ tc new_tys; might not be homogeneous 1398 -- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys) 1399normalise_tc_args tc tys 1400 = do { role <- getRole 1401 ; (args_cos, nargs, res_co) <- normalise_args (tyConKind tc) (tyConRolesX role tc) tys 1402 ; return (mkTyConAppCo role tc args_cos, nargs, res_co) } 1403 1404--------------- 1405normaliseType :: FamInstEnvs 1406 -> Role -- desired role of coercion 1407 -> Type -> (Coercion, Type) 1408normaliseType env role ty 1409 = initNormM env role (tyCoVarsOfType ty) $ normalise_type ty 1410 1411normalise_type :: Type -- old type 1412 -> NormM (Coercion, Type) -- (coercion, new type), where 1413 -- co :: old-type ~ new_type 1414-- Normalise the input type, by eliminating *all* type-function redexes 1415-- but *not* newtypes (which are visible to the programmer) 1416-- Returns with Refl if nothing happens 1417-- Does nothing to newtypes 1418-- The returned coercion *must* be *homogeneous* 1419-- See Note [Normalising types] 1420-- Try not to disturb type synonyms if possible 1421 1422normalise_type ty 1423 = go ty 1424 where 1425 go (TyConApp tc tys) = normalise_tc_app tc tys 1426 go ty@(LitTy {}) = do { r <- getRole 1427 ; return (mkReflCo r ty, ty) } 1428 go (AppTy ty1 ty2) = go_app_tys ty1 [ty2] 1429 1430 go ty@(FunTy { ft_mult = w, ft_arg = ty1, ft_res = ty2 }) 1431 = do { (co1, nty1) <- go ty1 1432 ; (co2, nty2) <- go ty2 1433 ; (wco, wty) <- withRole Nominal $ go w 1434 ; r <- getRole 1435 ; return (mkFunCo r wco co1 co2, ty { ft_mult = wty, ft_arg = nty1, ft_res = nty2 }) } 1436 go (ForAllTy (Bndr tcvar vis) ty) 1437 = do { (lc', tv', h, ki') <- normalise_var_bndr tcvar 1438 ; (co, nty) <- withLC lc' $ normalise_type ty 1439 ; let tv2 = setTyVarKind tv' ki' 1440 ; return (mkForAllCo tv' h co, ForAllTy (Bndr tv2 vis) nty) } 1441 go (TyVarTy tv) = normalise_tyvar tv 1442 go (CastTy ty co) 1443 = do { (nco, nty) <- go ty 1444 ; lc <- getLC 1445 ; let co' = substRightCo lc co 1446 ; return (castCoercionKind2 nco Nominal ty nty co co' 1447 , mkCastTy nty co') } 1448 go (CoercionTy co) 1449 = do { lc <- getLC 1450 ; r <- getRole 1451 ; let right_co = substRightCo lc co 1452 ; return ( mkProofIrrelCo r 1453 (liftCoSubst Nominal lc (coercionType co)) 1454 co right_co 1455 , mkCoercionTy right_co ) } 1456 1457 go_app_tys :: Type -- function 1458 -> [Type] -- args 1459 -> NormM (Coercion, Type) 1460 -- cf. GHC.Tc.Solver.Flatten.flatten_app_ty_args 1461 go_app_tys (AppTy ty1 ty2) tys = go_app_tys ty1 (ty2 : tys) 1462 go_app_tys fun_ty arg_tys 1463 = do { (fun_co, nfun) <- go fun_ty 1464 ; case tcSplitTyConApp_maybe nfun of 1465 Just (tc, xis) -> 1466 do { (second_co, nty) <- go (mkTyConApp tc (xis ++ arg_tys)) 1467 -- flatten_app_ty_args avoids redundantly processing the xis, 1468 -- but that's a much more performance-sensitive function. 1469 -- This type normalisation is not called in a loop. 1470 ; return (mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTransCo` second_co, nty) } 1471 Nothing -> 1472 do { (args_cos, nargs, res_co) <- normalise_args (typeKind nfun) 1473 (repeat Nominal) 1474 arg_tys 1475 ; role <- getRole 1476 ; let nty = mkAppTys nfun nargs 1477 nco = mkAppCos fun_co args_cos 1478 nty_casted = nty `mkCastTy` mkSymCo res_co 1479 final_co = mkCoherenceRightCo role nty (mkSymCo res_co) nco 1480 ; return (final_co, nty_casted) } } 1481 1482normalise_args :: Kind -- of the function 1483 -> [Role] -- roles at which to normalise args 1484 -> [Type] -- args 1485 -> NormM ([Coercion], [Type], Coercion) 1486-- returns (cos, xis, res_co), where each xi is the normalised 1487-- version of the corresponding type, each co is orig_arg ~ xi, 1488-- and the res_co :: kind(f orig_args) ~ kind(f xis) 1489-- NB: The xis might *not* have the same kinds as the input types, 1490-- but the resulting application *will* be well-kinded 1491-- cf. GHC.Tc.Solver.Flatten.flatten_args_slow 1492normalise_args fun_ki roles args 1493 = do { normed_args <- zipWithM normalise1 roles args 1494 ; let (xis, cos, res_co) = simplifyArgsWorker ki_binders inner_ki fvs roles normed_args 1495 ; return (map mkSymCo cos, xis, mkSymCo res_co) } 1496 where 1497 (ki_binders, inner_ki) = splitPiTys fun_ki 1498 fvs = tyCoVarsOfTypes args 1499 1500 -- flattener conventions are different from ours 1501 impedance_match :: NormM (Coercion, Type) -> NormM (Type, Coercion) 1502 impedance_match action = do { (co, ty) <- action 1503 ; return (ty, mkSymCo co) } 1504 1505 normalise1 role ty 1506 = impedance_match $ withRole role $ normalise_type ty 1507 1508normalise_tyvar :: TyVar -> NormM (Coercion, Type) 1509normalise_tyvar tv 1510 = ASSERT( isTyVar tv ) 1511 do { lc <- getLC 1512 ; r <- getRole 1513 ; return $ case liftCoSubstTyVar lc r tv of 1514 Just co -> (co, coercionRKind co) 1515 Nothing -> (mkReflCo r ty, ty) } 1516 where ty = mkTyVarTy tv 1517 1518normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Coercion, Kind) 1519normalise_var_bndr tcvar 1520 -- works for both tvar and covar 1521 = do { lc1 <- getLC 1522 ; env <- getEnv 1523 ; let callback lc ki = runNormM (normalise_type ki) env lc Nominal 1524 ; return $ liftCoSubstVarBndrUsing callback lc1 tcvar } 1525 1526-- | a monad for the normalisation functions, reading 'FamInstEnvs', 1527-- a 'LiftingContext', and a 'Role'. 1528newtype NormM a = NormM { runNormM :: 1529 FamInstEnvs -> LiftingContext -> Role -> a } 1530 deriving (Functor) 1531 1532initNormM :: FamInstEnvs -> Role 1533 -> TyCoVarSet -- the in-scope variables 1534 -> NormM a -> a 1535initNormM env role vars (NormM thing_inside) 1536 = thing_inside env lc role 1537 where 1538 in_scope = mkInScopeSet vars 1539 lc = emptyLiftingContext in_scope 1540 1541getRole :: NormM Role 1542getRole = NormM (\ _ _ r -> r) 1543 1544getLC :: NormM LiftingContext 1545getLC = NormM (\ _ lc _ -> lc) 1546 1547getEnv :: NormM FamInstEnvs 1548getEnv = NormM (\ env _ _ -> env) 1549 1550withRole :: Role -> NormM a -> NormM a 1551withRole r thing = NormM $ \ envs lc _old_r -> runNormM thing envs lc r 1552 1553withLC :: LiftingContext -> NormM a -> NormM a 1554withLC lc thing = NormM $ \ envs _old_lc r -> runNormM thing envs lc r 1555 1556instance Monad NormM where 1557 ma >>= fmb = NormM $ \env lc r -> 1558 let a = runNormM ma env lc r in 1559 runNormM (fmb a) env lc r 1560 1561instance Applicative NormM where 1562 pure x = NormM $ \ _ _ _ -> x 1563 (<*>) = ap 1564 1565{- 1566************************************************************************ 1567* * 1568 Flattening 1569* * 1570************************************************************************ 1571 1572Note [Flattening] 1573~~~~~~~~~~~~~~~~~ 1574As described in "Closed type families with overlapping equations" 1575http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf 1576we need to flatten core types before unifying them, when checking for "surely-apart" 1577against earlier equations of a closed type family. 1578Flattening means replacing all top-level uses of type functions with 1579fresh variables, *taking care to preserve sharing*. That is, the type 1580(Either (F a b) (F a b)) should flatten to (Either c c), never (Either 1581c d). 1582 1583Here is a nice example of why it's all necessary: 1584 1585 type family F a b where 1586 F Int Bool = Char 1587 F a b = Double 1588 type family G a -- open, no instances 1589 1590How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match, 1591while the second equation does. But, before reducing, we must make sure that the 1592target can never become (F Int Bool). Well, no matter what G Float becomes, it 1593certainly won't become *both* Int and Bool, so indeed we're safe reducing 1594(F (G Float) (G Float)) to Double. 1595 1596This is necessary not only to get more reductions (which we might be 1597willing to give up on), but for substitutivity. If we have (F x x), we 1598can see that (F x x) can reduce to Double. So, it had better be the 1599case that (F blah blah) can reduce to Double, no matter what (blah) 1600is! Flattening as done below ensures this. 1601 1602The algorithm works by building up a TypeMap TyVar, mapping 1603type family applications to fresh variables. This mapping must 1604be threaded through all the function calls, as any entry in 1605the mapping must be propagated to all future nodes in the tree. 1606 1607The algorithm also must track the set of in-scope variables, in 1608order to make fresh variables as it flattens. (We are far from a 1609source of fresh Uniques.) See Wrinkle 2, below. 1610 1611There are wrinkles, of course: 1612 16131. The flattening algorithm must account for the possibility 1614 of inner `forall`s. (A `forall` seen here can happen only 1615 because of impredicativity. However, the flattening operation 1616 is an algorithm in Core, which is impredicative.) 1617 Suppose we have (forall b. F b) -> (forall b. F b). Of course, 1618 those two bs are entirely unrelated, and so we should certainly 1619 not flatten the two calls F b to the same variable. Instead, they 1620 must be treated separately. We thus carry a substitution that 1621 freshens variables; we must apply this substitution (in 1622 `coreFlattenTyFamApp`) before looking up an application in the environment. 1623 Note that the range of the substitution contains only TyVars, never anything 1624 else. 1625 1626 For the sake of efficiency, we only apply this substitution when absolutely 1627 necessary. Namely: 1628 1629 * We do not perform the substitution at all if it is empty. 1630 * We only need to worry about the arguments of a type family that are within 1631 the arity of said type family, so we can get away with not applying the 1632 substitution to any oversaturated type family arguments. 1633 * Importantly, we do /not/ achieve this substitution by recursively 1634 flattening the arguments, as this would be wrong. Consider `F (G a)`, 1635 where F and G are type families. We might decide that `F (G a)` flattens 1636 to `beta`. Later, the substitution is non-empty (but does not map `a`) and 1637 so we flatten `G a` to `gamma` and try to flatten `F gamma`. Of course, 1638 `F gamma` is unknown, and so we flatten it to `delta`, but it really 1639 should have been `beta`! Argh! 1640 1641 Moral of the story: instead of flattening the arguments, just substitute 1642 them directly. 1643 16442. There are two different reasons we might add a variable 1645 to the in-scope set as we work: 1646 1647 A. We have just invented a new flattening variable. 1648 B. We have entered a `forall`. 1649 1650 Annoying here is that in-scope variable source (A) must be 1651 threaded through the calls. For example, consider (F b -> forall c. F c). 1652 Suppose that, when flattening F b, we invent a fresh variable c. 1653 Now, when we encounter (forall c. F c), we need to know c is already in 1654 scope so that we locally rename c to c'. However, if we don't thread through 1655 the in-scope set from one argument of (->) to the other, we won't know this 1656 and might get very confused. 1657 1658 In contrast, source (B) increases only as we go deeper, as in-scope sets 1659 normally do. However, even here we must be careful. The TypeMap TyVar that 1660 contains mappings from type family applications to freshened variables will 1661 be threaded through both sides of (forall b. F b) -> (forall b. F b). We 1662 thus must make sure that the two `b`s don't get renamed to the same b1. (If 1663 they did, then looking up `F b1` would yield the same flatten var for 1664 each.) So, even though `forall`-bound variables should really be in the 1665 in-scope set only when they are in scope, we retain these variables even 1666 outside of their scope. This ensures that, if we encounter a fresh 1667 `forall`-bound b, we will rename it to b2, not b1. Note that keeping a 1668 larger in-scope set than strictly necessary is always OK, as in-scope sets 1669 are only ever used to avoid collisions. 1670 1671 Sadly, the freshening substitution described in (1) really mustn't bind 1672 variables outside of their scope: note that its domain is the *unrenamed* 1673 variables. This means that the substitution gets "pushed down" (like a 1674 reader monad) while the in-scope set gets threaded (like a state monad). 1675 Because a TCvSubst contains its own in-scope set, we don't carry a TCvSubst; 1676 instead, we just carry a TvSubstEnv down, tying it to the InScopeSet 1677 traveling separately as necessary. 1678 16793. Consider `F ty_1 ... ty_n`, where F is a type family with arity k: 1680 1681 type family F ty_1 ... ty_k :: res_k 1682 1683 It's tempting to just flatten `F ty_1 ... ty_n` to `alpha`, where alpha is a 1684 flattening skolem. But we must instead flatten it to 1685 `alpha ty_(k+1) ... ty_n`—that is, by only flattening up to the arity of the 1686 type family. 1687 1688 Why is this better? Consider the following concrete example from #16995: 1689 1690 type family Param :: Type -> Type 1691 1692 type family LookupParam (a :: Type) :: Type where 1693 LookupParam (f Char) = Bool 1694 LookupParam x = Int 1695 1696 foo :: LookupParam (Param ()) 1697 foo = 42 1698 1699 In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to 1700 `Int`. But if we flatten `Param ()` to `alpha`, then GHC can't be sure if 1701 `alpha` is apart from `f Char`, so it won't fall through to the second 1702 equation. But since the `Param` type family has arity 0, we can instead 1703 flatten `Param ()` to `alpha ()`, about which GHC knows with confidence is 1704 apart from `f Char`, permitting the second equation to be reached. 1705 1706 Not only does this allow more programs to be accepted, it's also important 1707 for correctness. Not doing this was the root cause of the Core Lint error 1708 in #16995. 1709 1710flattenTys is defined here because of module dependencies. 1711-} 1712 1713data FlattenEnv 1714 = FlattenEnv { fe_type_map :: TypeMap TyVar 1715 -- domain: exactly-saturated type family applications 1716 -- range: fresh variables 1717 , fe_in_scope :: InScopeSet } 1718 -- See Note [Flattening] 1719 1720emptyFlattenEnv :: InScopeSet -> FlattenEnv 1721emptyFlattenEnv in_scope 1722 = FlattenEnv { fe_type_map = emptyTypeMap 1723 , fe_in_scope = in_scope } 1724 1725updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv 1726updateInScopeSet env upd = env { fe_in_scope = upd (fe_in_scope env) } 1727 1728flattenTys :: InScopeSet -> [Type] -> [Type] 1729-- See Note [Flattening] 1730-- NB: the returned types may mention fresh type variables, 1731-- arising from the flattening. We don't return the 1732-- mapping from those fresh vars to the ty-fam 1733-- applications they stand for (we could, but no need) 1734flattenTys in_scope tys 1735 = snd $ coreFlattenTys emptyTvSubstEnv (emptyFlattenEnv in_scope) tys 1736 1737coreFlattenTys :: TvSubstEnv -> FlattenEnv 1738 -> [Type] -> (FlattenEnv, [Type]) 1739coreFlattenTys subst = mapAccumL (coreFlattenTy subst) 1740 1741coreFlattenTy :: TvSubstEnv -> FlattenEnv 1742 -> Type -> (FlattenEnv, Type) 1743coreFlattenTy subst = go 1744 where 1745 go env ty | Just ty' <- coreView ty = go env ty' 1746 1747 go env (TyVarTy tv) 1748 | Just ty <- lookupVarEnv subst tv = (env, ty) 1749 | otherwise = let (env', ki) = go env (tyVarKind tv) in 1750 (env', mkTyVarTy $ setTyVarKind tv ki) 1751 go env (AppTy ty1 ty2) = let (env1, ty1') = go env ty1 1752 (env2, ty2') = go env1 ty2 in 1753 (env2, AppTy ty1' ty2') 1754 go env (TyConApp tc tys) 1755 -- NB: Don't just check if isFamilyTyCon: this catches *data* families, 1756 -- which are generative and thus can be preserved during flattening 1757 | not (isGenerativeTyCon tc Nominal) 1758 = coreFlattenTyFamApp subst env tc tys 1759 1760 | otherwise 1761 = let (env', tys') = coreFlattenTys subst env tys in 1762 (env', mkTyConApp tc tys') 1763 1764 go env ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 }) 1765 = let (env1, ty1') = go env ty1 1766 (env2, ty2') = go env1 ty2 1767 (env3, mult') = go env2 mult in 1768 (env3, ty { ft_mult = mult', ft_arg = ty1', ft_res = ty2' }) 1769 1770 go env (ForAllTy (Bndr tv vis) ty) 1771 = let (env1, subst', tv') = coreFlattenVarBndr subst env tv 1772 (env2, ty') = coreFlattenTy subst' env1 ty in 1773 (env2, ForAllTy (Bndr tv' vis) ty') 1774 1775 go env ty@(LitTy {}) = (env, ty) 1776 1777 go env (CastTy ty co) 1778 = let (env1, ty') = go env ty 1779 (env2, co') = coreFlattenCo subst env1 co in 1780 (env2, CastTy ty' co') 1781 1782 go env (CoercionTy co) 1783 = let (env', co') = coreFlattenCo subst env co in 1784 (env', CoercionTy co') 1785 1786 1787-- when flattening, we don't care about the contents of coercions. 1788-- so, just return a fresh variable of the right (flattened) type 1789coreFlattenCo :: TvSubstEnv -> FlattenEnv 1790 -> Coercion -> (FlattenEnv, Coercion) 1791coreFlattenCo subst env co 1792 = (env2, mkCoVarCo covar) 1793 where 1794 (env1, kind') = coreFlattenTy subst env (coercionType co) 1795 covar = mkFlattenFreshCoVar (fe_in_scope env1) kind' 1796 -- Add the covar to the FlattenEnv's in-scope set. 1797 -- See Note [Flattening], wrinkle 2A. 1798 env2 = updateInScopeSet env1 (flip extendInScopeSet covar) 1799 1800coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv 1801 -> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar) 1802coreFlattenVarBndr subst env tv 1803 = (env2, subst', tv') 1804 where 1805 -- See Note [Flattening], wrinkle 2B. 1806 kind = varType tv 1807 (env1, kind') = coreFlattenTy subst env kind 1808 tv' = uniqAway (fe_in_scope env1) (setVarType tv kind') 1809 subst' = extendVarEnv subst tv (mkTyVarTy tv') 1810 env2 = updateInScopeSet env1 (flip extendInScopeSet tv') 1811 1812coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv 1813 -> TyCon -- type family tycon 1814 -> [Type] -- args, already flattened 1815 -> (FlattenEnv, Type) 1816coreFlattenTyFamApp tv_subst env fam_tc fam_args 1817 = case lookupTypeMap type_map fam_ty of 1818 Just tv -> (env', mkAppTys (mkTyVarTy tv) leftover_args') 1819 Nothing -> let tyvar_name = mkFlattenFreshTyName fam_tc 1820 tv = uniqAway in_scope $ 1821 mkTyVar tyvar_name (typeKind fam_ty) 1822 1823 ty' = mkAppTys (mkTyVarTy tv) leftover_args' 1824 env'' = env' { fe_type_map = extendTypeMap type_map fam_ty tv 1825 , fe_in_scope = extendInScopeSet in_scope tv } 1826 in (env'', ty') 1827 where 1828 arity = tyConArity fam_tc 1829 tcv_subst = TCvSubst (fe_in_scope env) tv_subst emptyVarEnv 1830 (sat_fam_args, leftover_args) = ASSERT( arity <= length fam_args ) 1831 splitAt arity fam_args 1832 -- Apply the substitution before looking up an application in the 1833 -- environment. See Note [Flattening], wrinkle 1. 1834 -- NB: substTys short-cuts the common case when the substitution is empty. 1835 sat_fam_args' = substTys tcv_subst sat_fam_args 1836 (env', leftover_args') = coreFlattenTys tv_subst env leftover_args 1837 -- `fam_tc` may be over-applied to `fam_args` (see Note [Flattening], 1838 -- wrinkle 3), so we split it into the arguments needed to saturate it 1839 -- (sat_fam_args') and the rest (leftover_args') 1840 fam_ty = mkTyConApp fam_tc sat_fam_args' 1841 FlattenEnv { fe_type_map = type_map 1842 , fe_in_scope = in_scope } = env' 1843 1844mkFlattenFreshTyName :: Uniquable a => a -> Name 1845mkFlattenFreshTyName unq 1846 = mkSysTvName (getUnique unq) (fsLit "flt") 1847 1848mkFlattenFreshCoVar :: InScopeSet -> Kind -> CoVar 1849mkFlattenFreshCoVar in_scope kind 1850 = let uniq = unsafeGetFreshLocalUnique in_scope 1851 name = mkSystemVarName uniq (fsLit "flc") 1852 in mkCoVar name kind 1853