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