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