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