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