Get rid of some stuttering in comments and docs
[ghc.git] / compiler / typecheck / FamInst.hs
1 -- The @FamInst@ type: family instance heads
2
3 {-# LANGUAGE CPP, GADTs #-}
4
5 module FamInst (
6 FamInstEnvs, tcGetFamInstEnvs,
7 checkFamInstConsistency, tcExtendLocalFamInstEnv,
8 tcLookupDataFamInst, tcLookupDataFamInst_maybe,
9 tcInstNewTyCon_maybe, tcTopNormaliseNewTypeTF_maybe,
10 newFamInst,
11
12 -- * Injectivity
13 makeInjectivityErrors, injTyVarsOfType, injTyVarsOfTypes
14 ) where
15
16 import GhcPrelude
17
18 import HscTypes
19 import FamInstEnv
20 import InstEnv( roughMatchTcs )
21 import Coercion
22 import TcEvidence
23 import LoadIface
24 import TcRnMonad
25 import SrcLoc
26 import TyCon
27 import TcType
28 import CoAxiom
29 import DynFlags
30 import Module
31 import Outputable
32 import Util
33 import RdrName
34 import DataCon ( dataConName )
35 import Maybes
36 import Type
37 import TyCoRep
38 import TcMType
39 import Name
40 import Pair
41 import Panic
42 import VarSet
43 import Bag( Bag, unionBags, unitBag )
44 import Control.Monad
45
46 #include "HsVersions.h"
47
48 {-
49
50 Note [The type family instance consistency story]
51 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
52
53 To preserve type safety we must ensure that for any given module, all
54 the type family instances used either in that module or in any module
55 it directly or indirectly imports are consistent. For example, consider
56
57 module F where
58 type family F a
59
60 module A where
61 import F( F )
62 type instance F Int = Bool
63 f :: F Int -> Bool
64 f x = x
65
66 module B where
67 import F( F )
68 type instance F Int = Char
69 g :: Char -> F Int
70 g x = x
71
72 module Bad where
73 import A( f )
74 import B( g )
75 bad :: Char -> Int
76 bad c = f (g c)
77
78 Even though module Bad never mentions the type family F at all, by
79 combining the functions f and g that were type checked in contradictory
80 type family instance environments, the function bad is able to coerce
81 from one type to another. So when we type check Bad we must verify that
82 the type family instances defined in module A are consistent with those
83 defined in module B.
84
85 How do we ensure that we maintain the necessary consistency?
86
87 * Call a module which defines at least one type family instance a
88 "family instance module". This flag `mi_finsts` is recorded in the
89 interface file.
90
91 * For every module we calculate the set of all of its direct and
92 indirect dependencies that are family instance modules. This list
93 `dep_finsts` is also recorded in the interface file so we can compute
94 this list for a module from the lists for its direct dependencies.
95
96 * When type checking a module M we check consistency of all the type
97 family instances that are either provided by its `dep_finsts` or
98 defined in the module M itself. This is a pairwise check, i.e., for
99 every pair of instances we must check that they are consistent.
100
101 - For family instances coming from `dep_finsts`, this is checked in
102 checkFamInstConsistency, called from tcRnImports. See Note
103 [Checking family instance consistency] for details on this check (and
104 in particular how we avoid having to do all these checks for every
105 module we compile).
106
107 - That leaves checking the family instances defined in M itself
108 against instances defined in either M or its `dep_finsts`. This is
109 checked in `tcExtendLocalFamInstEnv'.
110
111 There are two subtle points in this scheme which have not been
112 addressed yet.
113
114 * We have checked consistency of the family instances *defined* by M
115 or its imports, but this is not by definition the same thing as the
116 family instances *used* by M or its imports. Specifically, we need to
117 ensure when we use a type family instance while compiling M that this
118 instance was really defined from either M or one of its imports,
119 rather than being an instance that we happened to know about from
120 reading an interface file in the course of compiling an unrelated
121 module. Otherwise, we'll end up with no record of the fact that M
122 depends on this family instance and type safety will be compromised.
123 See #13102.
124
125 * It can also happen that M uses a function defined in another module
126 which is not transitively imported by M. Examples include the
127 desugaring of various overloaded constructs, and references inserted
128 by Template Haskell splices. If that function's definition makes use
129 of type family instances which are not checked against those visible
130 from M, type safety can again be compromised. See #13251.
131
132 * When a module C imports a boot module B.hs-boot, we check that C's
133 type family instances are compatible with those visible from
134 B.hs-boot. However, C will eventually be linked against a different
135 module B.hs, which might define additional type family instances which
136 are inconsistent with C's. This can also lead to loss of type safety.
137 See #9562.
138
139 -}
140
141 {-
142 ************************************************************************
143 * *
144 Making a FamInst
145 * *
146 ************************************************************************
147 -}
148
149 -- All type variables in a FamInst must be fresh. This function
150 -- creates the fresh variables and applies the necessary substitution
151 -- It is defined here to avoid a dependency from FamInstEnv on the monad
152 -- code.
153
154 newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
155 -- Freshen the type variables of the FamInst branches
156 -- Called from the vectoriser monad too, hence the rather general type
157 newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
158 = ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
159 ASSERT2( tyCoVarsOfType rhs `subVarSet` tcv_set, text "rhs" <+> pp_ax )
160 ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
161 do { (subst, tvs') <- freshenTyVarBndrs tvs
162 ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
163 ; return (FamInst { fi_fam = tyConName fam_tc
164 , fi_flavor = flavor
165 , fi_tcs = roughMatchTcs lhs
166 , fi_tvs = tvs'
167 , fi_cvs = cvs'
168 , fi_tys = substTys subst lhs
169 , fi_rhs = substTy subst rhs
170 , fi_axiom = axiom }) }
171 where
172 lhs_kind = typeKind (mkTyConApp fam_tc lhs)
173 rhs_kind = typeKind rhs
174 tcv_set = mkVarSet (tvs ++ cvs)
175 pp_ax = pprCoAxiom axiom
176 CoAxBranch { cab_tvs = tvs
177 , cab_cvs = cvs
178 , cab_lhs = lhs
179 , cab_rhs = rhs } = coAxiomSingleBranch axiom
180
181
182 {-
183 ************************************************************************
184 * *
185 Optimised overlap checking for family instances
186 * *
187 ************************************************************************
188
189 Note [Checking family instance consistency]
190 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
191 For any two family instance modules that we import directly or indirectly, we
192 check whether the instances in the two modules are consistent, *unless* we can
193 be certain that the instances of the two modules have already been checked for
194 consistency during the compilation of modules that we import.
195
196 Why do we need to check? Consider
197 module X1 where module X2 where
198 data T1 data T2
199 type instance F T1 b = Int type instance F a T2 = Char
200 f1 :: F T1 a -> Int f2 :: Char -> F a T2
201 f1 x = x f2 x = x
202
203 Now if we import both X1 and X2 we could make (f2 . f1) :: Int -> Char.
204 Notice that neither instance is an orphan.
205
206 How do we know which pairs of modules have already been checked? For each
207 module M we directly import, we look up the family instance modules that M
208 imports (directly or indirectly), say F1, ..., FN. For any two modules
209 among M, F1, ..., FN, we know that the family instances defined in those
210 two modules are consistent--because we checked that when we compiled M.
211
212 For every other pair of family instance modules we import (directly or
213 indirectly), we check that they are consistent now. (So that we can be
214 certain that the modules in our `HscTypes.dep_finsts' are consistent.)
215
216 There is some fancy footwork regarding hs-boot module loops, see
217 Note [Don't check hs-boot type family instances too early]
218
219 Note [Checking family instance optimization]
220 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
221 As explained in Note [Checking family instance consistency]
222 we need to ensure that every pair of transitive imports that define type family
223 instances is consistent.
224
225 Let's define df(A) = transitive imports of A that define type family instances
226 + A, if A defines type family instances
227
228 Then for every direct import A, df(A) is already consistent.
229
230 Let's name the current module M.
231
232 We want to make sure that df(M) is consistent.
233 df(M) = df(D_1) U df(D_2) U ... U df(D_i) where D_1 .. D_i are direct imports.
234
235 We perform the check iteratively, maintaining a set of consistent modules 'C'
236 and trying to add df(D_i) to it.
237
238 The key part is how to ensure that the union C U df(D_i) is consistent.
239
240 Let's consider two modules: A and B from C U df(D_i).
241 There are nine possible ways to choose A and B from C U df(D_i):
242
243 | A in C only | A in C and B in df(D_i) | A in df(D_i) only
244 --------------------------------------------------------------------------------
245 B in C only | Already checked | Already checked | Needs to be checked
246 | when checking C | when checking C |
247 --------------------------------------------------------------------------------
248 B in C and | Already checked | Already checked | Already checked when
249 B in df(D_i) | when checking C | when checking C | checking df(D_i)
250 --------------------------------------------------------------------------------
251 B in df(D_i) | Needs to be | Already checked | Already checked when
252 only | checked | when checking df(D_i) | checking df(D_i)
253
254 That means to ensure that C U df(D_i) is consistent we need to check every
255 module from C - df(D_i) against every module from df(D_i) - C and
256 every module from df(D_i) - C against every module from C - df(D_i).
257 But since the checks are symmetric it suffices to pick A from C - df(D_i)
258 and B from df(D_i) - C.
259
260 In other words these are the modules we need to check:
261 [ (m1, m2) | m1 <- C, m1 not in df(D_i)
262 , m2 <- df(D_i), m2 not in C ]
263
264 One final thing to note here is that if there's lot of overlap between
265 subsequent df(D_i)'s then we expect those set differences to be small.
266 That situation should be pretty common in practice, there's usually
267 a set of utility modules that every module imports directly or indirectly.
268
269 This is basically the idea from #13092, comment:14.
270 -}
271
272 -- This function doesn't check ALL instances for consistency,
273 -- only ones that aren't involved in recursive knot-tying
274 -- loops; see Note [Don't check hs-boot type family instances too early].
275 -- We don't need to check the current module, this is done in
276 -- tcExtendLocalFamInstEnv.
277 -- See Note [The type family instance consistency story].
278 checkFamInstConsistency :: [Module] -> TcM ()
279 checkFamInstConsistency directlyImpMods
280 = do { dflags <- getDynFlags
281 ; (eps, hpt) <- getEpsAndHpt
282 ; traceTc "checkFamInstConsistency" (ppr directlyImpMods)
283 ; let { -- Fetch the iface of a given module. Must succeed as
284 -- all directly imported modules must already have been loaded.
285 modIface mod =
286 case lookupIfaceByModule dflags hpt (eps_PIT eps) mod of
287 Nothing -> panicDoc "FamInst.checkFamInstConsistency"
288 (ppr mod $$ pprHPT hpt)
289 Just iface -> iface
290
291 -- Which family instance modules were checked for consistency
292 -- when we compiled `mod`?
293 -- Itself (if a family instance module) and its dep_finsts.
294 -- This is df(D_i) from
295 -- Note [Checking family instance optimization]
296 ; modConsistent :: Module -> [Module]
297 ; modConsistent mod =
298 if mi_finsts (modIface mod) then mod:deps else deps
299 where
300 deps = dep_finsts . mi_deps . modIface $ mod
301
302 ; hmiModule = mi_module . hm_iface
303 ; hmiFamInstEnv = extendFamInstEnvList emptyFamInstEnv
304 . md_fam_insts . hm_details
305 ; hpt_fam_insts = mkModuleEnv [ (hmiModule hmi, hmiFamInstEnv hmi)
306 | hmi <- eltsHpt hpt]
307
308 }
309
310 ; checkMany hpt_fam_insts modConsistent directlyImpMods
311 }
312 where
313 -- See Note [Checking family instance optimization]
314 checkMany
315 :: ModuleEnv FamInstEnv -- home package family instances
316 -> (Module -> [Module]) -- given A, modules checked when A was checked
317 -> [Module] -- modules to process
318 -> TcM ()
319 checkMany hpt_fam_insts modConsistent mods = go [] emptyModuleSet mods
320 where
321 go :: [Module] -- list of consistent modules
322 -> ModuleSet -- set of consistent modules, same elements as the
323 -- list above
324 -> [Module] -- modules to process
325 -> TcM ()
326 go _ _ [] = return ()
327 go consistent consistent_set (mod:mods) = do
328 sequence_
329 [ check hpt_fam_insts m1 m2
330 | m1 <- to_check_from_mod
331 -- loop over toCheckFromMod first, it's usually smaller,
332 -- it may even be empty
333 , m2 <- to_check_from_consistent
334 ]
335 go consistent' consistent_set' mods
336 where
337 mod_deps_consistent = modConsistent mod
338 mod_deps_consistent_set = mkModuleSet mod_deps_consistent
339 consistent' = to_check_from_mod ++ consistent
340 consistent_set' =
341 extendModuleSetList consistent_set to_check_from_mod
342 to_check_from_consistent =
343 filterOut (`elemModuleSet` mod_deps_consistent_set) consistent
344 to_check_from_mod =
345 filterOut (`elemModuleSet` consistent_set) mod_deps_consistent
346 -- Why don't we just minusModuleSet here?
347 -- We could, but doing so means one of two things:
348 --
349 -- 1. When looping over the cartesian product we convert
350 -- a set into a non-deterministicly ordered list. Which
351 -- happens to be fine for interface file determinism
352 -- in this case, today, because the order only
353 -- determines the order of deferred checks. But such
354 -- invariants are hard to keep.
355 --
356 -- 2. When looping over the cartesian product we convert
357 -- a set into a deterministically ordered list - this
358 -- adds some additional cost of sorting for every
359 -- direct import.
360 --
361 -- That also explains why we need to keep both 'consistent'
362 -- and 'consistentSet'.
363 --
364 -- See also Note [ModuleEnv performance and determinism].
365 check hpt_fam_insts m1 m2
366 = do { env1' <- getFamInsts hpt_fam_insts m1
367 ; env2' <- getFamInsts hpt_fam_insts m2
368 -- We're checking each element of env1 against env2.
369 -- The cost of that is dominated by the size of env1, because
370 -- for each instance in env1 we look it up in the type family
371 -- environment env2, and lookup is cheap.
372 -- The code below ensures that env1 is the smaller environment.
373 ; let sizeE1 = famInstEnvSize env1'
374 sizeE2 = famInstEnvSize env2'
375 (env1, env2) = if sizeE1 < sizeE2 then (env1', env2')
376 else (env2', env1')
377 -- Note [Don't check hs-boot type family instances too early]
378 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
379 -- Family instance consistency checking involves checking that
380 -- the family instances of our imported modules are consistent with
381 -- one another; this might lead you to think that this process
382 -- has nothing to do with the module we are about to typecheck.
383 -- Not so! Consider the following case:
384 --
385 -- -- A.hs-boot
386 -- type family F a
387 --
388 -- -- B.hs
389 -- import {-# SOURCE #-} A
390 -- type instance F Int = Bool
391 --
392 -- -- A.hs
393 -- import B
394 -- type family F a
395 --
396 -- When typechecking A, we are NOT allowed to poke the TyThing
397 -- for F until we have typechecked the family. Thus, we
398 -- can't do consistency checking for the instance in B
399 -- (checkFamInstConsistency is called during renaming).
400 -- Failing to defer the consistency check lead to #11062.
401 --
402 -- Additionally, we should also defer consistency checking when
403 -- type from the hs-boot file of the current module occurs on
404 -- the left hand side, as we will poke its TyThing when checking
405 -- for overlap.
406 --
407 -- -- F.hs
408 -- type family F a
409 --
410 -- -- A.hs-boot
411 -- import F
412 -- data T
413 --
414 -- -- B.hs
415 -- import {-# SOURCE #-} A
416 -- import F
417 -- type instance F T = Int
418 --
419 -- -- A.hs
420 -- import B
421 -- data T = MkT
422 --
423 -- In fact, it is even necessary to defer for occurrences in
424 -- the RHS, because we may test for *compatibility* in event
425 -- of an overlap.
426 --
427 -- Why don't we defer ALL of the checks to later? Well, many
428 -- instances aren't involved in the recursive loop at all. So
429 -- we might as well check them immediately; and there isn't
430 -- a good time to check them later in any case: every time
431 -- we finish kind-checking a type declaration and add it to
432 -- a context, we *then* consistency check all of the instances
433 -- which mentioned that type. We DO want to check instances
434 -- as quickly as possible, so that we aren't typechecking
435 -- values with inconsistent axioms in scope.
436 --
437 -- See also Note [Tying the knot] and Note [Type-checking inside the knot]
438 -- for why we are doing this at all.
439 ; let check_now = famInstEnvElts env1
440 ; mapM_ (checkForConflicts (emptyFamInstEnv, env2)) check_now
441 ; mapM_ (checkForInjectivityConflicts (emptyFamInstEnv,env2)) check_now
442 }
443
444 getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
445 getFamInsts hpt_fam_insts mod
446 | Just env <- lookupModuleEnv hpt_fam_insts mod = return env
447 | otherwise = do { _ <- initIfaceTcRn (loadSysInterface doc mod)
448 ; eps <- getEps
449 ; return (expectJust "checkFamInstConsistency" $
450 lookupModuleEnv (eps_mod_fam_inst_env eps) mod) }
451 where
452 doc = ppr mod <+> text "is a family-instance module"
453
454 {-
455 ************************************************************************
456 * *
457 Lookup
458 * *
459 ************************************************************************
460
461 -}
462
463 -- | If @co :: T ts ~ rep_ty@ then:
464 --
465 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
466 --
467 -- Checks for a newtype, and for being saturated
468 -- Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion
469 tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion)
470 tcInstNewTyCon_maybe = instNewTyCon_maybe
471
472 -- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
473 -- there is no data family to unwrap.
474 -- Returns a Representational coercion
475 tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
476 -> (TyCon, [TcType], Coercion)
477 tcLookupDataFamInst fam_inst_envs tc tc_args
478 | Just (rep_tc, rep_args, co)
479 <- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
480 = (rep_tc, rep_args, co)
481 | otherwise
482 = (tc, tc_args, mkRepReflCo (mkTyConApp tc tc_args))
483
484 tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
485 -> Maybe (TyCon, [TcType], Coercion)
486 -- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a)
487 -- and returns a coercion between the two: co :: F [a] ~R FList a.
488 tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
489 | isDataFamilyTyCon tc
490 , match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args
491 , FamInstMatch { fim_instance = rep_fam@(FamInst { fi_axiom = ax
492 , fi_cvs = cvs })
493 , fim_tys = rep_args
494 , fim_cos = rep_cos } <- match
495 , let rep_tc = dataFamInstRepTyCon rep_fam
496 co = mkUnbranchedAxInstCo Representational ax rep_args
497 (mkCoVarCos cvs)
498 = ASSERT( null rep_cos ) -- See Note [Constrained family instances] in FamInstEnv
499 Just (rep_tc, rep_args, co)
500
501 | otherwise
502 = Nothing
503
504 -- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes,
505 -- potentially looking through newtype /instances/.
506 --
507 -- It is only used by the type inference engine (specifically, when
508 -- solving representational equality), and hence it is careful to unwrap
509 -- only if the relevant data constructor is in scope. That's why
510 -- it get a GlobalRdrEnv argument.
511 --
512 -- It is careful not to unwrap data/newtype instances if it can't
513 -- continue unwrapping. Such care is necessary for proper error
514 -- messages.
515 --
516 -- It does not look through type families.
517 -- It does not normalise arguments to a tycon.
518 --
519 -- If the result is Just (rep_ty, (co, gres), rep_ty), then
520 -- co : ty ~R rep_ty
521 -- gres are the GREs for the data constructors that
522 -- had to be in scope
523 tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
524 -> GlobalRdrEnv
525 -> Type
526 -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
527 tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
528 -- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
529 = topNormaliseTypeX stepper plus ty
530 where
531 plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion)
532 -> (Bag GlobalRdrElt, TcCoercion)
533 plus (gres1, co1) (gres2, co2) = ( gres1 `unionBags` gres2
534 , co1 `mkTransCo` co2 )
535
536 stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
537 stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance
538
539 -- For newtype instances we take a double step or nothing, so that
540 -- we don't return the representation type of the newtype instance,
541 -- which would lead to terrible error messages
542 unwrap_newtype_instance rec_nts tc tys
543 | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys
544 = mapStepResult (\(gres, co1) -> (gres, co `mkTransCo` co1)) $
545 unwrap_newtype rec_nts tc' tys'
546 | otherwise = NS_Done
547
548 unwrap_newtype rec_nts tc tys
549 | Just con <- newTyConDataCon_maybe tc
550 , Just gre <- lookupGRE_Name rdr_env (dataConName con)
551 -- This is where we check that the
552 -- data constructor is in scope
553 = mapStepResult (\co -> (unitBag gre, co)) $
554 unwrapNewTypeStepper rec_nts tc tys
555
556 | otherwise
557 = NS_Done
558
559 {-
560 ************************************************************************
561 * *
562 Extending the family instance environment
563 * *
564 ************************************************************************
565 -}
566
567 -- Add new locally-defined family instances, checking consistency with
568 -- previous locally-defined family instances as well as all instances
569 -- available from imported modules. This requires loading all of our
570 -- imports that define family instances (if we haven't loaded them already).
571 tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a
572
573 -- If we weren't actually given any instances to add, then we don't want
574 -- to go to the bother of loading family instance module dependencies.
575 tcExtendLocalFamInstEnv [] thing_inside = thing_inside
576
577 -- Otherwise proceed...
578 tcExtendLocalFamInstEnv fam_insts thing_inside
579 = do { env <- getGblEnv
580 ; let this_mod = tcg_mod env
581 imports = tcg_imports env
582
583 -- Optimization: If we're only defining type family instances
584 -- for type families *defined in the home package*, then we
585 -- only have to load interface files that belong to the home
586 -- package. The reason is that there's no recursion between
587 -- packages, so modules in other packages can't possibly define
588 -- instances for our type families.
589 --
590 -- (Within the home package, we could import a module M that
591 -- imports us via an hs-boot file, and thereby defines an
592 -- instance of a type family defined in this module. So we can't
593 -- apply the same logic to avoid reading any interface files at
594 -- all, when we define an instances for type family defined in
595 -- the current module.)
596 home_fams_only = all (nameIsHomePackage this_mod . fi_fam) fam_insts
597 want_module mod
598 | mod == this_mod = False
599 | home_fams_only = moduleUnitId mod == moduleUnitId this_mod
600 | otherwise = True
601 ; loadModuleInterfaces (text "Loading family-instance modules")
602 (filter want_module (imp_finsts imports))
603 ; (inst_env', fam_insts') <- foldlM addLocalFamInst
604 (tcg_fam_inst_env env, tcg_fam_insts env)
605 fam_insts
606 ; let env' = env { tcg_fam_insts = fam_insts'
607 , tcg_fam_inst_env = inst_env' }
608 ; setGblEnv env' thing_inside
609 }
610
611 -- Check that the proposed new instance is OK,
612 -- and then add it to the home inst env
613 -- This must be lazy in the fam_inst arguments, see Note [Lazy axiom match]
614 -- in FamInstEnv.hs
615 addLocalFamInst :: (FamInstEnv,[FamInst])
616 -> FamInst
617 -> TcM (FamInstEnv, [FamInst])
618 addLocalFamInst (home_fie, my_fis) fam_inst
619 -- home_fie includes home package and this module
620 -- my_fies is just the ones from this module
621 = do { traceTc "addLocalFamInst" (ppr fam_inst)
622
623 -- Unlike the case of class instances, don't override existing
624 -- instances in GHCi; it's unsound. See #7102.
625
626 ; mod <- getModule
627 ; traceTc "alfi" (ppr mod)
628
629 -- Fetch imported instances, so that we report
630 -- overlaps correctly.
631 -- Really we ought to only check consistency with
632 -- those instances which are transitively imported
633 -- by the current module, rather than every instance
634 -- we've ever seen. Fixing this is part of #13102.
635 ; eps <- getEps
636 ; let inst_envs = (eps_fam_inst_env eps, home_fie)
637 home_fie' = extendFamInstEnv home_fie fam_inst
638
639 -- Check for conflicting instance decls and injectivity violations
640 ; no_conflict <- checkForConflicts inst_envs fam_inst
641 ; injectivity_ok <- checkForInjectivityConflicts inst_envs fam_inst
642
643 ; if no_conflict && injectivity_ok then
644 return (home_fie', fam_inst : my_fis)
645 else
646 return (home_fie, my_fis) }
647
648 {-
649 ************************************************************************
650 * *
651 Checking an instance against conflicts with an instance env
652 * *
653 ************************************************************************
654
655 Check whether a single family instance conflicts with those in two instance
656 environments (one for the EPS and one for the HPT).
657 -}
658
659 checkForConflicts :: FamInstEnvs -> FamInst -> TcM Bool
660 checkForConflicts inst_envs fam_inst
661 = do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst
662 no_conflicts = null conflicts
663 ; traceTc "checkForConflicts" $
664 vcat [ ppr (map fim_instance conflicts)
665 , ppr fam_inst
666 -- , ppr inst_envs
667 ]
668 ; unless no_conflicts $ conflictInstErr fam_inst conflicts
669 ; return no_conflicts }
670
671 -- | Check whether a new open type family equation can be added without
672 -- violating injectivity annotation supplied by the user. Returns True when
673 -- this is possible and False if adding this equation would violate injectivity
674 -- annotation.
675 checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM Bool
676 checkForInjectivityConflicts instEnvs famInst
677 | isTypeFamilyTyCon tycon
678 -- type family is injective in at least one argument
679 , Injective inj <- tyConInjectivityInfo tycon = do
680 { let axiom = coAxiomSingleBranch fi_ax
681 conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst
682 -- see Note [Verifying injectivity annotation] in FamInstEnv
683 errs = makeInjectivityErrors fi_ax axiom inj conflicts
684 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err) errs
685 ; return (null errs)
686 }
687
688 -- if there was no injectivity annotation or tycon does not represent a
689 -- type family we report no conflicts
690 | otherwise = return True
691 where tycon = famInstTyCon famInst
692 fi_ax = fi_axiom famInst
693
694 -- | Build a list of injectivity errors together with their source locations.
695 makeInjectivityErrors
696 :: CoAxiom br -- ^ Type family for which we generate errors
697 -> CoAxBranch -- ^ Currently checked equation (represented by axiom)
698 -> [Bool] -- ^ Injectivity annotation
699 -> [CoAxBranch] -- ^ List of injectivity conflicts
700 -> [(SDoc, SrcSpan)]
701 makeInjectivityErrors fi_ax axiom inj conflicts
702 = ASSERT2( any id inj, text "No injective type variables" )
703 let lhs = coAxBranchLHS axiom
704 rhs = coAxBranchRHS axiom
705
706 are_conflicts = not $ null conflicts
707 unused_inj_tvs = unusedInjTvsInRHS (coAxiomTyCon fi_ax) inj lhs rhs
708 inj_tvs_unused = not $ and (isEmptyVarSet <$> unused_inj_tvs)
709 tf_headed = isTFHeaded rhs
710 bare_variables = bareTvInRHSViolated lhs rhs
711 wrong_bare_rhs = not $ null bare_variables
712
713 err_builder herald eqns
714 = ( hang herald
715 2 (vcat (map (pprCoAxBranch fi_ax) eqns))
716 , coAxBranchSpan (head eqns) )
717 errorIf p f = if p then [f err_builder axiom] else []
718 in errorIf are_conflicts (conflictInjInstErr conflicts )
719 ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs)
720 ++ errorIf tf_headed tfHeadedErr
721 ++ errorIf wrong_bare_rhs (bareVariableInRHSErr bare_variables)
722
723
724 -- | Return a list of type variables that the function is injective in and that
725 -- do not appear on injective positions in the RHS of a family instance
726 -- declaration. The returned Pair includes invisible vars followed by visible ones
727 unusedInjTvsInRHS :: TyCon -> [Bool] -> [Type] -> Type -> Pair TyVarSet
728 -- INVARIANT: [Bool] list contains at least one True value
729 -- See Note [Verifying injectivity annotation]. This function implements fourth
730 -- check described there.
731 -- In theory, instead of implementing this whole check in this way, we could
732 -- attempt to unify equation with itself. We would reject exactly the same
733 -- equations but this method gives us more precise error messages by returning
734 -- precise names of variables that are not mentioned in the RHS.
735 unusedInjTvsInRHS tycon injList lhs rhs =
736 (`minusVarSet` injRhsVars) <$> injLHSVars
737 where
738 -- set of type and kind variables in which type family is injective
739 (invis_pairs, vis_pairs)
740 = partitionInvisibles tycon snd (zipEqual "unusedInjTvsInRHS" injList lhs)
741 invis_lhs = uncurry filterByList $ unzip invis_pairs
742 vis_lhs = uncurry filterByList $ unzip vis_pairs
743
744 invis_vars = tyCoVarsOfTypes invis_lhs
745 Pair invis_vars' vis_vars = splitVisVarsOfTypes vis_lhs
746 injLHSVars
747 = Pair (invis_vars `minusVarSet` vis_vars `unionVarSet` invis_vars')
748 vis_vars
749
750 -- set of type variables appearing in the RHS on an injective position.
751 -- For all returned variables we assume their associated kind variables
752 -- also appear in the RHS.
753 injRhsVars = injTyVarsOfType rhs
754
755 injTyVarsOfType :: TcTauType -> TcTyVarSet
756 -- Collect all type variables that are either arguments to a type
757 -- constructor or to /injective/ type families.
758 -- Determining the overall type determines thes variables
759 --
760 -- E.g. Suppose F is injective in its second arg, but not its first
761 -- then injVarOfType (Either a (F [b] (a,c))) = {a,c}
762 -- Determining the overall type determines a,c but not b.
763 injTyVarsOfType (TyVarTy v)
764 = unitVarSet v `unionVarSet` injTyVarsOfType (tyVarKind v)
765 injTyVarsOfType (TyConApp tc tys)
766 | isTypeFamilyTyCon tc
767 = case tyConInjectivityInfo tc of
768 NotInjective -> emptyVarSet
769 Injective inj -> injTyVarsOfTypes (filterByList inj tys)
770 | otherwise
771 = injTyVarsOfTypes tys
772 injTyVarsOfType (LitTy {})
773 = emptyVarSet
774 injTyVarsOfType (FunTy arg res)
775 = injTyVarsOfType arg `unionVarSet` injTyVarsOfType res
776 injTyVarsOfType (AppTy fun arg)
777 = injTyVarsOfType fun `unionVarSet` injTyVarsOfType arg
778 -- No forall types in the RHS of a type family
779 injTyVarsOfType (CastTy ty _) = injTyVarsOfType ty
780 injTyVarsOfType (CoercionTy {}) = emptyVarSet
781 injTyVarsOfType (ForAllTy {}) =
782 panic "unusedInjTvsInRHS.injTyVarsOfType"
783
784 injTyVarsOfTypes :: [Type] -> VarSet
785 injTyVarsOfTypes tys = mapUnionVarSet injTyVarsOfType tys
786
787 -- | Is type headed by a type family application?
788 isTFHeaded :: Type -> Bool
789 -- See Note [Verifying injectivity annotation]. This function implements third
790 -- check described there.
791 isTFHeaded ty | Just ty' <- coreView ty
792 = isTFHeaded ty'
793 isTFHeaded ty | (TyConApp tc args) <- ty
794 , isTypeFamilyTyCon tc
795 = args `lengthIs` tyConArity tc
796 isTFHeaded _ = False
797
798
799 -- | If a RHS is a bare type variable return a set of LHS patterns that are not
800 -- bare type variables.
801 bareTvInRHSViolated :: [Type] -> Type -> [Type]
802 -- See Note [Verifying injectivity annotation]. This function implements second
803 -- check described there.
804 bareTvInRHSViolated pats rhs | isTyVarTy rhs
805 = filter (not . isTyVarTy) pats
806 bareTvInRHSViolated _ _ = []
807
808
809 conflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
810 conflictInstErr fam_inst conflictingMatch
811 | (FamInstMatch { fim_instance = confInst }) : _ <- conflictingMatch
812 = let (err, span) = makeFamInstsErr
813 (text "Conflicting family instance declarations:")
814 [fam_inst, confInst]
815 in setSrcSpan span $ addErr err
816 | otherwise
817 = panic "conflictInstErr"
818
819 -- | Type of functions that use error message and a list of axioms to build full
820 -- error message (with a source location) for injective type families.
821 type InjErrorBuilder = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
822
823 -- | Build injecivity error herald common to all injectivity errors.
824 injectivityErrorHerald :: Bool -> SDoc
825 injectivityErrorHerald isSingular =
826 text "Type family equation" <> s isSingular <+> text "violate" <>
827 s (not isSingular) <+> text "injectivity annotation" <>
828 if isSingular then dot else colon
829 -- Above is an ugly hack. We want this: "sentence. herald:" (note the dot and
830 -- colon). But if herald is empty we want "sentence:" (note the colon). We
831 -- can't test herald for emptiness so we rely on the fact that herald is empty
832 -- only when isSingular is False. If herald is non empty it must end with a
833 -- colon.
834 where
835 s False = text "s"
836 s True = empty
837
838 -- | Build error message for a pair of equations violating an injectivity
839 -- annotation.
840 conflictInjInstErr :: [CoAxBranch] -> InjErrorBuilder -> CoAxBranch
841 -> (SDoc, SrcSpan)
842 conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
843 | confEqn : _ <- conflictingEqns
844 = errorBuilder (injectivityErrorHerald False) [confEqn, tyfamEqn]
845 | otherwise
846 = panic "conflictInjInstErr"
847
848 -- | Build error message for equation with injective type variables unused in
849 -- the RHS.
850 unusedInjectiveVarsErr :: Pair TyVarSet -> InjErrorBuilder -> CoAxBranch
851 -> (SDoc, SrcSpan)
852 unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn
853 = errorBuilder (injectivityErrorHerald True $$ msg)
854 [tyfamEqn]
855 where
856 tvs = invis_vars `unionVarSet` vis_vars
857 has_types = not $ isEmptyVarSet vis_vars
858 has_kinds = not $ isEmptyVarSet invis_vars
859
860 doc = sep [ what <+> text "variable" <>
861 pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . toposortTyVars)
862 , text "cannot be inferred from the right-hand side." ]
863 what = case (has_types, has_kinds) of
864 (True, True) -> text "Type and kind"
865 (True, False) -> text "Type"
866 (False, True) -> text "Kind"
867 (False, False) -> pprPanic "mkUnusedInjectiveVarsErr" $ ppr tvs
868 print_kinds_info = ppWhen has_kinds ppSuggestExplicitKinds
869 msg = doc $$ print_kinds_info $$
870 text "In the type family equation:"
871
872 -- | Build error message for equation that has a type family call at the top
873 -- level of RHS
874 tfHeadedErr :: InjErrorBuilder -> CoAxBranch
875 -> (SDoc, SrcSpan)
876 tfHeadedErr errorBuilder famInst
877 = errorBuilder (injectivityErrorHerald True $$
878 text "RHS of injective type family equation cannot" <+>
879 text "be a type family:") [famInst]
880
881 -- | Build error message for equation that has a bare type variable in the RHS
882 -- but LHS pattern is not a bare type variable.
883 bareVariableInRHSErr :: [Type] -> InjErrorBuilder -> CoAxBranch
884 -> (SDoc, SrcSpan)
885 bareVariableInRHSErr tys errorBuilder famInst
886 = errorBuilder (injectivityErrorHerald True $$
887 text "RHS of injective type family equation is a bare" <+>
888 text "type variable" $$
889 text "but these LHS type and kind patterns are not bare" <+>
890 text "variables:" <+> pprQuotedList tys) [famInst]
891
892
893 makeFamInstsErr :: SDoc -> [FamInst] -> (SDoc, SrcSpan)
894 makeFamInstsErr herald insts
895 = ASSERT( not (null insts) )
896 ( hang herald
897 2 (vcat [ pprCoAxBranchHdr (famInstAxiom fi) 0
898 | fi <- sorted ])
899 , srcSpan )
900 where
901 getSpan = getSrcLoc . famInstAxiom
902 sorted = sortWith getSpan insts
903 fi1 = head sorted
904 srcSpan = coAxBranchSpan (coAxiomSingleBranch (famInstAxiom fi1))
905 -- The sortWith just arranges that instances are dislayed in order
906 -- of source location, which reduced wobbling in error messages,
907 -- and is better for users
908
909 tcGetFamInstEnvs :: TcM FamInstEnvs
910 -- Gets both the external-package inst-env
911 -- and the home-pkg inst env (includes module being compiled)
912 tcGetFamInstEnvs
913 = do { eps <- getEps; env <- getGblEnv
914 ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }