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