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