never executed always true always false
1 {-# LANGUAGE GADTs, ViewPatterns #-}
2
3 -- | The @FamInst@ type: family instance heads
4 module GHC.Tc.Instance.Family (
5 FamInstEnvs, tcGetFamInstEnvs,
6 checkFamInstConsistency, tcExtendLocalFamInstEnv,
7 tcLookupDataFamInst, tcLookupDataFamInst_maybe,
8 tcInstNewTyCon_maybe, tcTopNormaliseNewTypeTF_maybe,
9 newFamInst,
10
11 -- * Injectivity
12 reportInjectivityErrors, reportConflictingInjectivityErrs
13 ) where
14
15 import GHC.Prelude
16
17 import GHC.Driver.Session
18 import GHC.Driver.Env
19
20 import GHC.Core.FamInstEnv
21 import GHC.Core.InstEnv( roughMatchTcs )
22 import GHC.Core.Coercion
23 import GHC.Core.TyCon
24 import GHC.Core.Coercion.Axiom
25 import GHC.Core.DataCon ( dataConName )
26 import GHC.Core.TyCo.Rep
27 import GHC.Core.TyCo.FVs
28
29 import GHC.Iface.Load
30
31 import GHC.Tc.Errors.Types
32 import GHC.Tc.Types.Evidence
33 import GHC.Tc.Utils.Monad
34 import GHC.Tc.Utils.Instantiate( freshenTyVarBndrs, freshenCoVarBndrsX )
35 import GHC.Tc.Utils.TcType
36
37 import GHC.Unit.External
38 import GHC.Unit.Module
39 import GHC.Unit.Module.ModIface
40 import GHC.Unit.Module.ModDetails
41 import GHC.Unit.Module.Deps
42 import GHC.Unit.Home.ModInfo
43
44 import GHC.Types.SrcLoc as SrcLoc
45 import GHC.Types.Name.Reader
46 import GHC.Types.Name
47 import GHC.Types.Var.Set
48
49 import GHC.Utils.Outputable
50 import GHC.Utils.Misc
51 import GHC.Utils.Panic
52 import GHC.Utils.Panic.Plain
53 import GHC.Utils.FV
54
55 import GHC.Data.Bag( Bag, unionBags, unitBag )
56 import GHC.Data.Maybe
57
58 import Control.Monad
59 import Data.List.NonEmpty ( NonEmpty(..) )
60 import qualified Data.List.NonEmpty as NE
61 import Data.Function ( on )
62
63 import qualified GHC.LanguageExtensions as LangExt
64
65 {- Note [The type family instance consistency story]
66 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
67
68 To preserve type safety we must ensure that for any given module, all
69 the type family instances used either in that module or in any module
70 it directly or indirectly imports are consistent. For example, consider
71
72 module F where
73 type family F a
74
75 module A where
76 import F( F )
77 type instance F Int = Bool
78 f :: F Int -> Bool
79 f x = x
80
81 module B where
82 import F( F )
83 type instance F Int = Char
84 g :: Char -> F Int
85 g x = x
86
87 module Bad where
88 import A( f )
89 import B( g )
90 bad :: Char -> Int
91 bad c = f (g c)
92
93 Even though module Bad never mentions the type family F at all, by
94 combining the functions f and g that were type checked in contradictory
95 type family instance environments, the function bad is able to coerce
96 from one type to another. So when we type check Bad we must verify that
97 the type family instances defined in module A are consistent with those
98 defined in module B.
99
100 How do we ensure that we maintain the necessary consistency?
101
102 * Call a module which defines at least one type family instance a
103 "family instance module". This flag `mi_finsts` is recorded in the
104 interface file.
105
106 * For every module we calculate the set of all of its direct and
107 indirect dependencies that are family instance modules. This list
108 `dep_finsts` is also recorded in the interface file so we can compute
109 this list for a module from the lists for its direct dependencies.
110
111 * When type checking a module M we check consistency of all the type
112 family instances that are either provided by its `dep_finsts` or
113 defined in the module M itself. This is a pairwise check, i.e., for
114 every pair of instances we must check that they are consistent.
115
116 - For family instances coming from `dep_finsts`, this is checked in
117 checkFamInstConsistency, called from tcRnImports. See Note
118 [Checking family instance consistency] for details on this check
119 (and in particular how we avoid having to do all these checks for
120 every module we compile).
121
122 - That leaves checking the family instances defined in M itself
123 against instances defined in either M or its `dep_finsts`. This is
124 checked in `tcExtendLocalFamInstEnv'.
125
126 There are four subtle points in this scheme which have not been
127 addressed yet.
128
129 * We have checked consistency of the family instances *defined* by M
130 or its imports, but this is not by definition the same thing as the
131 family instances *used* by M or its imports. Specifically, we need to
132 ensure when we use a type family instance while compiling M that this
133 instance was really defined from either M or one of its imports,
134 rather than being an instance that we happened to know about from
135 reading an interface file in the course of compiling an unrelated
136 module. Otherwise, we'll end up with no record of the fact that M
137 depends on this family instance and type safety will be compromised.
138 See #13102.
139
140 * It can also happen that M uses a function defined in another module
141 which is not transitively imported by M. Examples include the
142 desugaring of various overloaded constructs, and references inserted
143 by Template Haskell splices. If that function's definition makes use
144 of type family instances which are not checked against those visible
145 from M, type safety can again be compromised. See #13251.
146
147 * When a module C imports a boot module B.hs-boot, we check that C's
148 type family instances are compatible with those visible from
149 B.hs-boot. However, C will eventually be linked against a different
150 module B.hs, which might define additional type family instances which
151 are inconsistent with C's. This can also lead to loss of type safety.
152 See #9562.
153
154 * The call to checkFamConsistency for imported functions occurs very
155 early (in tcRnImports) and that causes problems if the imported
156 instances use type declared in the module being compiled.
157 See Note [Loading your own hi-boot file] in GHC.Iface.Load.
158 -}
159
160 {-
161 ************************************************************************
162 * *
163 Making a FamInst
164 * *
165 ************************************************************************
166 -}
167
168 -- All type variables in a FamInst must be fresh. This function
169 -- creates the fresh variables and applies the necessary substitution
170 -- It is defined here to avoid a dependency from FamInstEnv on the monad
171 -- code.
172
173 newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
174 -- Freshen the type variables of the FamInst branches
175 newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
176 = do {
177 -- Freshen the type variables
178 (subst, tvs') <- freshenTyVarBndrs tvs
179 ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
180 ; let lhs' = substTys subst lhs
181 rhs' = substTy subst rhs
182
183 ; return (FamInst { fi_fam = tyConName fam_tc
184 , fi_flavor = flavor
185 , fi_tcs = roughMatchTcs lhs
186 , fi_tvs = tvs'
187 , fi_cvs = cvs'
188 , fi_tys = lhs'
189 , fi_rhs = rhs'
190 , fi_axiom = axiom }) }
191 where
192 CoAxBranch { cab_tvs = tvs
193 , cab_cvs = cvs
194 , cab_lhs = lhs
195 , cab_rhs = rhs } = coAxiomSingleBranch axiom
196
197
198 {-
199 ************************************************************************
200 * *
201 Optimised overlap checking for family instances
202 * *
203 ************************************************************************
204
205 Note [Checking family instance consistency]
206 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
207 For any two family instance modules that we import directly or indirectly, we
208 check whether the instances in the two modules are consistent, *unless* we can
209 be certain that the instances of the two modules have already been checked for
210 consistency during the compilation of modules that we import.
211
212 Why do we need to check? Consider
213 module X1 where module X2 where
214 data T1 data T2
215 type instance F T1 b = Int type instance F a T2 = Char
216 f1 :: F T1 a -> Int f2 :: Char -> F a T2
217 f1 x = x f2 x = x
218
219 Now if we import both X1 and X2 we could make (f2 . f1) :: Int -> Char.
220 Notice that neither instance is an orphan.
221
222 How do we know which pairs of modules have already been checked? For each
223 module M we directly import, we look up the family instance modules that M
224 imports (directly or indirectly), say F1, ..., FN. For any two modules
225 among M, F1, ..., FN, we know that the family instances defined in those
226 two modules are consistent--because we checked that when we compiled M.
227
228 For every other pair of family instance modules we import (directly or
229 indirectly), we check that they are consistent now. (So that we can be
230 certain that the modules in our `GHC.Driver.Env.dep_finsts' are consistent.)
231
232 There is some fancy footwork regarding hs-boot module loops, see
233 Note [Don't check hs-boot type family instances too early]
234
235 Note [Checking family instance optimization]
236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
237 As explained in Note [Checking family instance consistency]
238 we need to ensure that every pair of transitive imports that define type family
239 instances is consistent.
240
241 Let's define df(A) = transitive imports of A that define type family instances
242 + A, if A defines type family instances
243
244 Then for every direct import A, df(A) is already consistent.
245
246 Let's name the current module M.
247
248 We want to make sure that df(M) is consistent.
249 df(M) = df(D_1) U df(D_2) U ... U df(D_i) where D_1 .. D_i are direct imports.
250
251 We perform the check iteratively, maintaining a set of consistent modules 'C'
252 and trying to add df(D_i) to it.
253
254 The key part is how to ensure that the union C U df(D_i) is consistent.
255
256 Let's consider two modules: A and B from C U df(D_i).
257 There are nine possible ways to choose A and B from C U df(D_i):
258
259 | A in C only | A in C and B in df(D_i) | A in df(D_i) only
260 --------------------------------------------------------------------------------
261 B in C only | Already checked | Already checked | Needs to be checked
262 | when checking C | when checking C |
263 --------------------------------------------------------------------------------
264 B in C and | Already checked | Already checked | Already checked when
265 B in df(D_i) | when checking C | when checking C | checking df(D_i)
266 --------------------------------------------------------------------------------
267 B in df(D_i) | Needs to be | Already checked | Already checked when
268 only | checked | when checking df(D_i) | checking df(D_i)
269
270 That means to ensure that C U df(D_i) is consistent we need to check every
271 module from C - df(D_i) against every module from df(D_i) - C and
272 every module from df(D_i) - C against every module from C - df(D_i).
273 But since the checks are symmetric it suffices to pick A from C - df(D_i)
274 and B from df(D_i) - C.
275
276 In other words these are the modules we need to check:
277 [ (m1, m2) | m1 <- C, m1 not in df(D_i)
278 , m2 <- df(D_i), m2 not in C ]
279
280 One final thing to note here is that if there's lot of overlap between
281 subsequent df(D_i)'s then we expect those set differences to be small.
282 That situation should be pretty common in practice, there's usually
283 a set of utility modules that every module imports directly or indirectly.
284
285 This is basically the idea from #13092, comment:14.
286 -}
287
288 -- This function doesn't check ALL instances for consistency,
289 -- only ones that aren't involved in recursive knot-tying
290 -- loops; see Note [Don't check hs-boot type family instances too early].
291 -- We don't need to check the current module, this is done in
292 -- tcExtendLocalFamInstEnv.
293 -- See Note [The type family instance consistency story].
294 checkFamInstConsistency :: [Module] -> TcM ()
295 checkFamInstConsistency directlyImpMods
296 = do { (eps, hpt) <- getEpsAndHpt
297 ; traceTc "checkFamInstConsistency" (ppr directlyImpMods)
298 ; let { -- Fetch the iface of a given module. Must succeed as
299 -- all directly imported modules must already have been loaded.
300 modIface mod =
301 case lookupIfaceByModule hpt (eps_PIT eps) mod of
302 Nothing -> panicDoc "FamInst.checkFamInstConsistency"
303 (ppr mod $$ pprHPT hpt)
304 Just iface -> iface
305
306 -- Which family instance modules were checked for consistency
307 -- when we compiled `mod`?
308 -- Itself (if a family instance module) and its dep_finsts.
309 -- This is df(D_i) from
310 -- Note [Checking family instance optimization]
311 ; modConsistent :: Module -> [Module]
312 ; modConsistent mod =
313 if mi_finsts (mi_final_exts (modIface mod)) then mod:deps else deps
314 where
315 deps = dep_finsts . mi_deps . modIface $ mod
316
317 ; hmiModule = mi_module . hm_iface
318 ; hmiFamInstEnv = extendFamInstEnvList emptyFamInstEnv
319 . md_fam_insts . hm_details
320 ; hpt_fam_insts = mkModuleEnv [ (hmiModule hmi, hmiFamInstEnv hmi)
321 | hmi <- eltsHpt hpt]
322
323 }
324
325 ; checkMany hpt_fam_insts modConsistent directlyImpMods
326 }
327 where
328 -- See Note [Checking family instance optimization]
329 checkMany
330 :: ModuleEnv FamInstEnv -- home package family instances
331 -> (Module -> [Module]) -- given A, modules checked when A was checked
332 -> [Module] -- modules to process
333 -> TcM ()
334 checkMany hpt_fam_insts modConsistent mods = go [] emptyModuleSet mods
335 where
336 go :: [Module] -- list of consistent modules
337 -> ModuleSet -- set of consistent modules, same elements as the
338 -- list above
339 -> [Module] -- modules to process
340 -> TcM ()
341 go _ _ [] = return ()
342 go consistent consistent_set (mod:mods) = do
343 sequence_
344 [ check hpt_fam_insts m1 m2
345 | m1 <- to_check_from_mod
346 -- loop over toCheckFromMod first, it's usually smaller,
347 -- it may even be empty
348 , m2 <- to_check_from_consistent
349 ]
350 go consistent' consistent_set' mods
351 where
352 mod_deps_consistent = modConsistent mod
353 mod_deps_consistent_set = mkModuleSet mod_deps_consistent
354 consistent' = to_check_from_mod ++ consistent
355 consistent_set' =
356 extendModuleSetList consistent_set to_check_from_mod
357 to_check_from_consistent =
358 filterOut (`elemModuleSet` mod_deps_consistent_set) consistent
359 to_check_from_mod =
360 filterOut (`elemModuleSet` consistent_set) mod_deps_consistent
361 -- Why don't we just minusModuleSet here?
362 -- We could, but doing so means one of two things:
363 --
364 -- 1. When looping over the cartesian product we convert
365 -- a set into a non-deterministicly ordered list. Which
366 -- happens to be fine for interface file determinism
367 -- in this case, today, because the order only
368 -- determines the order of deferred checks. But such
369 -- invariants are hard to keep.
370 --
371 -- 2. When looping over the cartesian product we convert
372 -- a set into a deterministically ordered list - this
373 -- adds some additional cost of sorting for every
374 -- direct import.
375 --
376 -- That also explains why we need to keep both 'consistent'
377 -- and 'consistentSet'.
378 --
379 -- See also Note [ModuleEnv performance and determinism].
380 check hpt_fam_insts m1 m2
381 = do { env1' <- getFamInsts hpt_fam_insts m1
382 ; env2' <- getFamInsts hpt_fam_insts m2
383 -- We're checking each element of env1 against env2.
384 -- The cost of that is dominated by the size of env1, because
385 -- for each instance in env1 we look it up in the type family
386 -- environment env2, and lookup is cheap.
387 -- The code below ensures that env1 is the smaller environment.
388 ; let sizeE1 = famInstEnvSize env1'
389 sizeE2 = famInstEnvSize env2'
390 (env1, env2) = if sizeE1 < sizeE2 then (env1', env2')
391 else (env2', env1')
392 -- Note [Don't check hs-boot type family instances too early]
393 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
394 -- Family instance consistency checking involves checking that
395 -- the family instances of our imported modules are consistent with
396 -- one another; this might lead you to think that this process
397 -- has nothing to do with the module we are about to typecheck.
398 -- Not so! Consider the following case:
399 --
400 -- -- A.hs-boot
401 -- type family F a
402 --
403 -- -- B.hs
404 -- import {-# SOURCE #-} A
405 -- type instance F Int = Bool
406 --
407 -- -- A.hs
408 -- import B
409 -- type family F a
410 --
411 -- When typechecking A, we are NOT allowed to poke the TyThing
412 -- for F until we have typechecked the family. Thus, we
413 -- can't do consistency checking for the instance in B
414 -- (checkFamInstConsistency is called during renaming).
415 -- Failing to defer the consistency check lead to #11062.
416 --
417 -- Additionally, we should also defer consistency checking when
418 -- type from the hs-boot file of the current module occurs on
419 -- the left hand side, as we will poke its TyThing when checking
420 -- for overlap.
421 --
422 -- -- F.hs
423 -- type family F a
424 --
425 -- -- A.hs-boot
426 -- import F
427 -- data T
428 --
429 -- -- B.hs
430 -- import {-# SOURCE #-} A
431 -- import F
432 -- type instance F T = Int
433 --
434 -- -- A.hs
435 -- import B
436 -- data T = MkT
437 --
438 -- In fact, it is even necessary to defer for occurrences in
439 -- the RHS, because we may test for *compatibility* in event
440 -- of an overlap.
441 --
442 -- Why don't we defer ALL of the checks to later? Well, many
443 -- instances aren't involved in the recursive loop at all. So
444 -- we might as well check them immediately; and there isn't
445 -- a good time to check them later in any case: every time
446 -- we finish kind-checking a type declaration and add it to
447 -- a context, we *then* consistency check all of the instances
448 -- which mentioned that type. We DO want to check instances
449 -- as quickly as possible, so that we aren't typechecking
450 -- values with inconsistent axioms in scope.
451 --
452 -- See also Note [Tying the knot]
453 -- for why we are doing this at all.
454 ; let check_now = famInstEnvElts env1
455 ; mapM_ (checkForConflicts (emptyFamInstEnv, env2)) check_now
456 ; mapM_ (checkForInjectivityConflicts (emptyFamInstEnv,env2)) check_now
457 }
458
459 getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
460 getFamInsts hpt_fam_insts mod
461 | Just env <- lookupModuleEnv hpt_fam_insts mod = return env
462 | otherwise = do { _ <- initIfaceTcRn (loadSysInterface doc mod)
463 ; eps <- getEps
464 ; return (expectJust "checkFamInstConsistency" $
465 lookupModuleEnv (eps_mod_fam_inst_env eps) mod) }
466 where
467 doc = ppr mod <+> text "is a family-instance module"
468
469 {-
470 ************************************************************************
471 * *
472 Lookup
473 * *
474 ************************************************************************
475
476 -}
477
478 -- | If @co :: T ts ~ rep_ty@ then:
479 --
480 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
481 --
482 -- Checks for a newtype, and for being saturated
483 -- Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion
484 tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion)
485 tcInstNewTyCon_maybe = instNewTyCon_maybe
486
487 -- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
488 -- there is no data family to unwrap.
489 -- Returns a Representational coercion
490 tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
491 -> (TyCon, [TcType], Coercion)
492 tcLookupDataFamInst fam_inst_envs tc tc_args
493 | Just (rep_tc, rep_args, co)
494 <- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
495 = (rep_tc, rep_args, co)
496 | otherwise
497 = (tc, tc_args, mkRepReflCo (mkTyConApp tc tc_args))
498
499 tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
500 -> Maybe (TyCon, [TcType], Coercion)
501 -- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a)
502 -- and returns a coercion between the two: co :: F [a] ~R FList a.
503 tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
504 | isDataFamilyTyCon tc
505 , match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args
506 , FamInstMatch { fim_instance = rep_fam@(FamInst { fi_axiom = ax
507 , fi_cvs = cvs })
508 , fim_tys = rep_args
509 , fim_cos = rep_cos } <- match
510 , let rep_tc = dataFamInstRepTyCon rep_fam
511 co = mkUnbranchedAxInstCo Representational ax rep_args
512 (mkCoVarCos cvs)
513 = assert (null rep_cos) $ -- See Note [Constrained family instances] in GHC.Core.FamInstEnv
514 Just (rep_tc, rep_args, co)
515
516 | otherwise
517 = Nothing
518
519 -- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes,
520 -- potentially looking through newtype /instances/.
521 --
522 -- It is only used by the type inference engine (specifically, when
523 -- solving representational equality), and hence it is careful to unwrap
524 -- only if the relevant data constructor is in scope. That's why
525 -- it gets a GlobalRdrEnv argument.
526 --
527 -- It is careful not to unwrap data/newtype instances if it can't
528 -- continue unwrapping. Such care is necessary for proper error
529 -- messages.
530 --
531 -- It does not look through type families.
532 -- It does not normalise arguments to a tycon.
533 --
534 -- If the result is Just ((gres, co), rep_ty), then
535 -- co : ty ~R rep_ty
536 -- gres are the GREs for the data constructors that
537 -- had to be in scope
538 tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
539 -> GlobalRdrEnv
540 -> Type
541 -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
542 tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
543 -- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
544 = topNormaliseTypeX stepper plus ty
545 where
546 plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion)
547 -> (Bag GlobalRdrElt, TcCoercion)
548 plus (gres1, co1) (gres2, co2) = ( gres1 `unionBags` gres2
549 , co1 `mkTransCo` co2 )
550
551 stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
552 stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance
553
554 -- For newtype instances we take a double step or nothing, so that
555 -- we don't return the representation type of the newtype instance,
556 -- which would lead to terrible error messages
557 unwrap_newtype_instance rec_nts tc tys
558 | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys
559 = mapStepResult (\(gres, co1) -> (gres, co `mkTransCo` co1)) $
560 unwrap_newtype rec_nts tc' tys'
561 | otherwise = NS_Done
562
563 unwrap_newtype rec_nts tc tys
564 | Just con <- newTyConDataCon_maybe tc
565 , Just gre <- lookupGRE_Name rdr_env (dataConName con)
566 -- This is where we check that the
567 -- data constructor is in scope
568 = mapStepResult (\co -> (unitBag gre, co)) $
569 unwrapNewTypeStepper rec_nts tc tys
570
571 | otherwise
572 = NS_Done
573
574 {-
575 ************************************************************************
576 * *
577 Extending the family instance environment
578 * *
579 ************************************************************************
580 -}
581
582 -- Add new locally-defined family instances, checking consistency with
583 -- previous locally-defined family instances as well as all instances
584 -- available from imported modules. This requires loading all of our
585 -- imports that define family instances (if we haven't loaded them already).
586 tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a
587
588 -- If we weren't actually given any instances to add, then we don't want
589 -- to go to the bother of loading family instance module dependencies.
590 tcExtendLocalFamInstEnv [] thing_inside = thing_inside
591
592 -- Otherwise proceed...
593 tcExtendLocalFamInstEnv fam_insts thing_inside
594 = do { -- Load family-instance modules "below" this module, so that
595 -- allLocalFamInst can check for consistency with them
596 -- See Note [The type family instance consistency story]
597 loadDependentFamInstModules fam_insts
598
599 -- Now add the instances one by one
600 ; env <- getGblEnv
601 ; (inst_env', fam_insts') <- foldlM addLocalFamInst
602 (tcg_fam_inst_env env, tcg_fam_insts env)
603 fam_insts
604
605 ; let env' = env { tcg_fam_insts = fam_insts'
606 , tcg_fam_inst_env = inst_env' }
607 ; setGblEnv env' thing_inside
608 }
609
610 loadDependentFamInstModules :: [FamInst] -> TcM ()
611 -- Load family-instance modules "below" this module, so that
612 -- allLocalFamInst can check for consistency with them
613 -- See Note [The type family instance consistency story]
614 loadDependentFamInstModules fam_insts
615 = do { env <- getGblEnv
616 ; let this_mod = tcg_mod env
617 imports = tcg_imports env
618
619 want_module mod -- See Note [Home package family instances]
620 | mod == this_mod = False
621 | home_fams_only = moduleUnit mod == moduleUnit this_mod
622 | otherwise = True
623 home_fams_only = all (nameIsHomePackage this_mod . fi_fam) fam_insts
624
625 ; loadModuleInterfaces (text "Loading family-instance modules") $
626 filter want_module (imp_finsts imports) }
627
628 {- Note [Home package family instances]
629 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
630 Optimization: If we're only defining type family instances
631 for type families *defined in the home package*, then we
632 only have to load interface files that belong to the home
633 package. The reason is that there's no recursion between
634 packages, so modules in other packages can't possibly define
635 instances for our type families.
636
637 (Within the home package, we could import a module M that
638 imports us via an hs-boot file, and thereby defines an
639 instance of a type family defined in this module. So we can't
640 apply the same logic to avoid reading any interface files at
641 all, when we define an instances for type family defined in
642 the current module.
643 -}
644
645 -- Check that the proposed new instance is OK,
646 -- and then add it to the home inst env
647 -- This must be lazy in the fam_inst arguments, see Note [Lazy axiom match]
648 -- in GHC.Core.FamInstEnv
649 addLocalFamInst :: (FamInstEnv,[FamInst])
650 -> FamInst
651 -> TcM (FamInstEnv, [FamInst])
652 addLocalFamInst (home_fie, my_fis) fam_inst
653 -- home_fie includes home package and this module
654 -- my_fies is just the ones from this module
655 = do { traceTc "addLocalFamInst" (ppr fam_inst)
656
657 -- Unlike the case of class instances, don't override existing
658 -- instances in GHCi; it's unsound. See #7102.
659
660 ; mod <- getModule
661 ; traceTc "alfi" (ppr mod)
662
663 -- Fetch imported instances, so that we report
664 -- overlaps correctly.
665 -- Really we ought to only check consistency with
666 -- those instances which are transitively imported
667 -- by the current module, rather than every instance
668 -- we've ever seen. Fixing this is part of #13102.
669 ; eps <- getEps
670 ; let inst_envs = (eps_fam_inst_env eps, home_fie)
671 home_fie' = extendFamInstEnv home_fie fam_inst
672
673 -- Check for conflicting instance decls and injectivity violations
674 ; ((), no_errs) <- askNoErrs $
675 do { checkForConflicts inst_envs fam_inst
676 ; checkForInjectivityConflicts inst_envs fam_inst
677 ; checkInjectiveEquation fam_inst
678 }
679
680 ; if no_errs then
681 return (home_fie', fam_inst : my_fis)
682 else
683 return (home_fie, my_fis) }
684
685 {-
686 ************************************************************************
687 * *
688 Checking an instance against conflicts with an instance env
689 * *
690 ************************************************************************
691
692 Check whether a single family instance conflicts with those in two instance
693 environments (one for the EPS and one for the HPT).
694 -}
695
696 -- | Checks to make sure no two family instances overlap.
697 checkForConflicts :: FamInstEnvs -> FamInst -> TcM ()
698 checkForConflicts inst_envs fam_inst
699 = do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst
700 ; traceTc "checkForConflicts" $
701 vcat [ ppr (map fim_instance conflicts)
702 , ppr fam_inst
703 -- , ppr inst_envs
704 ]
705 ; reportConflictInstErr fam_inst conflicts }
706
707 checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM ()
708 -- see Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv, check 1B1.
709 checkForInjectivityConflicts instEnvs famInst
710 | isTypeFamilyTyCon tycon -- as opposed to data family tycon
711 , Injective inj <- tyConInjectivityInfo tycon
712 = let conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst in
713 reportConflictingInjectivityErrs tycon conflicts (coAxiomSingleBranch (fi_axiom famInst))
714
715 | otherwise
716 = return ()
717
718 where tycon = famInstTyCon famInst
719
720 -- | Check whether a new open type family equation can be added without
721 -- violating injectivity annotation supplied by the user. Returns True when
722 -- this is possible and False if adding this equation would violate injectivity
723 -- annotation. This looks only at the one equation; it does not look for
724 -- interaction between equations. Use checkForInjectivityConflicts for that.
725 -- Does checks (2)-(4) of Note [Verifying injectivity annotation] in "GHC.Core.FamInstEnv".
726 checkInjectiveEquation :: FamInst -> TcM ()
727 checkInjectiveEquation famInst
728 | isTypeFamilyTyCon tycon
729 -- type family is injective in at least one argument
730 , Injective inj <- tyConInjectivityInfo tycon = do
731 { dflags <- getDynFlags
732 ; let axiom = coAxiomSingleBranch fi_ax
733 -- see Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv
734 ; reportInjectivityErrors dflags fi_ax axiom inj
735 }
736
737 -- if there was no injectivity annotation or tycon does not represent a
738 -- type family we report no conflicts
739 | otherwise
740 = return ()
741
742 where tycon = famInstTyCon famInst
743 fi_ax = fi_axiom famInst
744
745 -- | Report a list of injectivity errors together with their source locations.
746 -- Looks only at one equation; does not look for conflicts *among* equations.
747 reportInjectivityErrors
748 :: DynFlags
749 -> CoAxiom br -- ^ Type family for which we generate errors
750 -> CoAxBranch -- ^ Currently checked equation (represented by axiom)
751 -> [Bool] -- ^ Injectivity annotation
752 -> TcM ()
753 reportInjectivityErrors dflags fi_ax axiom inj
754 = assertPpr (any id inj) (text "No injective type variables") $
755 do let lhs = coAxBranchLHS axiom
756 rhs = coAxBranchRHS axiom
757 fam_tc = coAxiomTyCon fi_ax
758 (unused_inj_tvs, unused_vis, undec_inst_flag)
759 = unusedInjTvsInRHS dflags fam_tc lhs rhs
760 inj_tvs_unused = not $ isEmptyVarSet unused_inj_tvs
761 tf_headed = isTFHeaded rhs
762 bare_variables = bareTvInRHSViolated lhs rhs
763 wrong_bare_rhs = not $ null bare_variables
764
765 when inj_tvs_unused $ reportUnusedInjectiveVarsErr fam_tc unused_inj_tvs
766 unused_vis undec_inst_flag axiom
767 when tf_headed $ reportTfHeadedErr fam_tc axiom
768 when wrong_bare_rhs $ reportBareVariableInRHSErr fam_tc bare_variables axiom
769
770 -- | Is type headed by a type family application?
771 isTFHeaded :: Type -> Bool
772 -- See Note [Verifying injectivity annotation], case 3.
773 isTFHeaded ty | Just ty' <- coreView ty
774 = isTFHeaded ty'
775 isTFHeaded ty | (TyConApp tc args) <- ty
776 , isTypeFamilyTyCon tc
777 = args `lengthIs` tyConArity tc
778 isTFHeaded _ = False
779
780
781 -- | If a RHS is a bare type variable return a set of LHS patterns that are not
782 -- bare type variables.
783 bareTvInRHSViolated :: [Type] -> Type -> [Type]
784 -- See Note [Verifying injectivity annotation], case 2.
785 bareTvInRHSViolated pats rhs | isTyVarTy rhs
786 = filter (not . isTyVarTy) pats
787 bareTvInRHSViolated _ _ = []
788
789 ------------------------------------------------------------------
790 -- Checking for the coverage condition for injective type families
791 ------------------------------------------------------------------
792
793 {-
794 Note [Coverage condition for injective type families]
795 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
796 The Injective Type Families paper describes how we can tell whether
797 or not a type family equation upholds the injectivity condition.
798 Briefly, consider the following:
799
800 type family F a b = r | r -> a -- NB: b is not injective
801
802 type instance F ty1 ty2 = ty3
803
804 We need to make sure that all variables mentioned in ty1 are mentioned in ty3
805 -- that's how we know that knowing ty3 determines ty1. But they can't be
806 mentioned just anywhere in ty3: they must be in *injective* positions in ty3.
807 For example:
808
809 type instance F a Int = Maybe (G a)
810
811 This is no good, if G is not injective. However, if G is indeed injective,
812 then this would appear to meet our needs. There is a trap here, though: while
813 knowing G a does indeed determine a, trying to compute a from G a might not
814 terminate. This is precisely the same problem that we have with functional
815 dependencies and their liberal coverage condition. Here is the test case:
816
817 type family G a = r | r -> a
818 type instance G [a] = [G a]
819 [W] G alpha ~ [alpha]
820
821 We see that the equation given applies, because G alpha equals a list. So we
822 learn that alpha must be [beta] for some beta. We then have
823
824 [W] G [beta] ~ [[beta]]
825
826 This can reduce to
827
828 [W] [G beta] ~ [[beta]]
829
830 which then decomposes to
831
832 [W] G beta ~ [beta]
833
834 right where we started. The equation G [a] = [G a] thus is dangerous: while
835 it does not violate the injectivity assumption, it might throw us into a loop,
836 with a particularly dastardly Wanted.
837
838 We thus do what functional dependencies do: require -XUndecidableInstances to
839 accept this.
840
841 Checking the coverage condition is not terribly hard, but we also want to produce
842 a nice error message. A nice error message has at least two properties:
843
844 1. If any of the variables involved are invisible or are used in an invisible context,
845 we want to print invisible arguments (as -fprint-explicit-kinds does).
846
847 2. If we fail to accept the equation because we're worried about non-termination,
848 we want to suggest UndecidableInstances.
849
850 To gather the right information, we can talk about the *usage* of a variable. Every
851 variable is used either visibly or invisibly, and it is either not used at all,
852 in a context where acceptance requires UndecidableInstances, or in a context that
853 does not require UndecidableInstances. If a variable is used both visibly and
854 invisibly, then we want to remember the fact that it was used invisibly: printing
855 out invisibles will be helpful for the user to understand what is going on.
856 If a variable is used where we need -XUndecidableInstances and where we don't,
857 we can similarly just remember the latter.
858
859 We thus define Visibility and NeedsUndecInstFlag below. These enumerations are
860 *ordered*, and we used their Ord instances. We then define VarUsage, which is just a pair
861 of a Visibility and a NeedsUndecInstFlag. (The visibility is irrelevant when a
862 variable is NotPresent, but this extra slack in the representation causes no
863 harm.) We finally define VarUsages as a mapping from variables to VarUsage.
864 Its Monoid instance combines two maps, using the Semigroup instance of VarUsage
865 to combine elements that are represented in both maps. In this way, we can
866 compositionally analyze types (and portions thereof).
867
868 To do the injectivity check:
869
870 1. We build VarUsages that represent the LHS (rather, the portion of the LHS
871 that is flagged as injective); each usage on the LHS is NotPresent, because we
872 have not yet looked at the RHS.
873
874 2. We also build a VarUsage for the RHS, done by injTyVarUsages.
875
876 3. We then combine these maps. Now, every variable in the injective components of the LHS
877 will be mapped to its correct usage (either NotPresent or perhaps needing
878 -XUndecidableInstances in order to be seen as injective).
879
880 4. We look up each var used in an injective argument on the LHS in
881 the map, making a list of tvs that should be determined by the RHS
882 but aren't.
883
884 5. We then return the set of bad variables, whether any of the bad
885 ones were used invisibly, and whether any bad ones need -XUndecidableInstances.
886 If -XUndecidableInstances is enabled, than a var that needs the flag
887 won't be bad, so it won't appear in this list.
888
889 6. We use all this information to produce a nice error message, (a) switching
890 on -fprint-explicit-kinds if appropriate and (b) telling the user about
891 -XUndecidableInstances if appropriate.
892
893 -}
894
895 -- | Return the set of type variables that a type family equation is
896 -- expected to be injective in but is not. Suppose we have @type family
897 -- F a b = r | r -> a@. Then any variables that appear free in the first
898 -- argument to F in an equation must be fixed by that equation's RHS.
899 -- This function returns all such variables that are not indeed fixed.
900 -- It also returns whether any of these variables appear invisibly
901 -- and whether -XUndecidableInstances would help.
902 -- See Note [Coverage condition for injective type families].
903 unusedInjTvsInRHS :: DynFlags
904 -> TyCon -- type family
905 -> [Type] -- LHS arguments
906 -> Type -- the RHS
907 -> ( TyVarSet
908 , HasKinds -- YesHasKinds <=> one or more variable is used invisibly
909 , SuggestUndecidableInstances) -- YesSuggestUndecidableInstaces <=> suggest -XUndecidableInstances
910 -- See Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv.
911 -- This function implements check (4) described there, further
912 -- described in Note [Coverage condition for injective type families].
913 -- In theory (and modulo the -XUndecidableInstances wrinkle),
914 -- instead of implementing this whole check in this way, we could
915 -- attempt to unify equation with itself. We would reject exactly the same
916 -- equations but this method gives us more precise error messages by returning
917 -- precise names of variables that are not mentioned in the RHS.
918 unusedInjTvsInRHS dflags tycon@(tyConInjectivityInfo -> Injective inj_list) lhs rhs =
919 -- Note [Coverage condition for injective type families], step 5
920 (bad_vars, hasKinds any_invisible, suggestUndecidableInstances suggest_undec)
921 where
922 undec_inst = xopt LangExt.UndecidableInstances dflags
923
924 inj_lhs = filterByList inj_list lhs
925 lhs_vars = tyCoVarsOfTypes inj_lhs
926
927 rhs_inj_vars = fvVarSet $ injectiveVarsOfType undec_inst rhs
928
929 bad_vars = lhs_vars `minusVarSet` rhs_inj_vars
930
931 any_bad = not $ isEmptyVarSet bad_vars
932
933 invis_vars = fvVarSet $ invisibleVarsOfTypes [mkTyConApp tycon lhs, rhs]
934
935 any_invisible = any_bad && (bad_vars `intersectsVarSet` invis_vars)
936 suggest_undec = any_bad &&
937 not undec_inst &&
938 (lhs_vars `subVarSet` fvVarSet (injectiveVarsOfType True rhs))
939
940 -- When the type family is not injective in any arguments
941 unusedInjTvsInRHS _ _ _ _ = (emptyVarSet, NoHasKinds, NoSuggestUndecidableInstaces)
942
943 ---------------------------------------
944 -- Producing injectivity error messages
945 ---------------------------------------
946
947 -- | Report error message for a pair of equations violating an injectivity
948 -- annotation. No error message if there are no branches.
949 reportConflictingInjectivityErrs :: TyCon -> [CoAxBranch] -> CoAxBranch -> TcM ()
950 reportConflictingInjectivityErrs _ [] _ = return ()
951 reportConflictingInjectivityErrs fam_tc (confEqn1:_) tyfamEqn
952 = addErrs [buildInjectivityError (TcRnFamInstNotInjective InjErrRhsOverlap)
953 fam_tc
954 (confEqn1 :| [tyfamEqn])]
955
956 -- | Report error message for equation with injective type variables unused in
957 -- the RHS. Note [Coverage condition for injective type families], step 6
958 reportUnusedInjectiveVarsErr :: TyCon
959 -> TyVarSet
960 -> HasKinds -- YesHasKinds <=> print invisible arguments
961 -> SuggestUndecidableInstances -- YesSuggestUndecidableInstaces <=> suggest -XUndecidableInstances
962 -> CoAxBranch
963 -> TcM ()
964 reportUnusedInjectiveVarsErr fam_tc tvs has_kinds undec_inst tyfamEqn
965 = let reason = InjErrCannotInferFromRhs tvs has_kinds undec_inst
966 (loc, dia) = buildInjectivityError (TcRnFamInstNotInjective reason) fam_tc (tyfamEqn :| [])
967 in addErrAt loc dia
968
969 -- | Report error message for equation that has a type family call at the top
970 -- level of RHS
971 reportTfHeadedErr :: TyCon -> CoAxBranch -> TcM ()
972 reportTfHeadedErr fam_tc branch
973 = addErrs [buildInjectivityError (TcRnFamInstNotInjective InjErrRhsCannotBeATypeFam)
974 fam_tc
975 (branch :| [])]
976
977 -- | Report error message for equation that has a bare type variable in the RHS
978 -- but LHS pattern is not a bare type variable.
979 reportBareVariableInRHSErr :: TyCon -> [Type] -> CoAxBranch -> TcM ()
980 reportBareVariableInRHSErr fam_tc tys branch
981 = addErrs [buildInjectivityError (TcRnFamInstNotInjective (InjErrRhsBareTyVar tys))
982 fam_tc
983 (branch :| [])]
984
985 buildInjectivityError :: (TyCon -> NonEmpty CoAxBranch -> TcRnMessage)
986 -> TyCon
987 -> NonEmpty CoAxBranch
988 -> (SrcSpan, TcRnMessage)
989 buildInjectivityError mkErr fam_tc branches
990 = ( coAxBranchSpan (NE.head branches), mkErr fam_tc branches )
991
992 reportConflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
993 reportConflictInstErr _ []
994 = return () -- No conflicts
995 reportConflictInstErr fam_inst (match1 : _)
996 | FamInstMatch { fim_instance = conf_inst } <- match1
997 , let sorted = NE.sortBy (SrcLoc.leftmost_smallest `on` getSpan) (fam_inst NE.:| [conf_inst])
998 fi1 = NE.head sorted
999 span = coAxBranchSpan (coAxiomSingleBranch (famInstAxiom fi1))
1000 = setSrcSpan span $ addErr $ TcRnConflictingFamInstDecls sorted
1001 where
1002 getSpan = getSrcSpan . famInstAxiom
1003 -- The sortBy just arranges that instances are displayed in order
1004 -- of source location, which reduced wobbling in error messages,
1005 -- and is better for users
1006
1007 tcGetFamInstEnvs :: TcM FamInstEnvs
1008 -- Gets both the external-package inst-env
1009 -- and the home-pkg inst env (includes module being compiled)
1010 tcGetFamInstEnvs
1011 = do { eps <- getEps; env <- getGblEnv
1012 ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }