e4b2cc3517666e7f616a44290aff71e02daafb6f
[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
14 ) where
15
16 import HscTypes
17 import FamInstEnv
18 import InstEnv( roughMatchTcs )
19 import Coercion
20 import TcEvidence
21 import LoadIface
22 import TcRnMonad
23 import SrcLoc
24 import TyCon
25 import TcType
26 import CoAxiom
27 import DynFlags
28 import Module
29 import Outputable
30 import UniqFM
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 Control.Monad
43 import Data.Map (Map)
44 import qualified Data.Map as Map
45
46 #include "HsVersions.h"
47
48 {-
49 ************************************************************************
50 * *
51 Making a FamInst
52 * *
53 ************************************************************************
54 -}
55
56 -- All type variables in a FamInst must be fresh. This function
57 -- creates the fresh variables and applies the necessary substitution
58 -- It is defined here to avoid a dependency from FamInstEnv on the monad
59 -- code.
60
61 newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
62 -- Freshen the type variables of the FamInst branches
63 -- Called from the vectoriser monad too, hence the rather general type
64 newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
65 = do { (subst, tvs') <- freshenTyVarBndrs tvs
66 ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
67 ; return (FamInst { fi_fam = tyConName fam_tc
68 , fi_flavor = flavor
69 , fi_tcs = roughMatchTcs lhs
70 , fi_tvs = tvs'
71 , fi_cvs = cvs'
72 , fi_tys = substTys subst lhs
73 , fi_rhs = substTy subst rhs
74 , fi_axiom = axiom }) }
75 where
76 CoAxBranch { cab_tvs = tvs
77 , cab_cvs = cvs
78 , cab_lhs = lhs
79 , cab_rhs = rhs } = coAxiomSingleBranch axiom
80
81
82 {-
83 ************************************************************************
84 * *
85 Optimised overlap checking for family instances
86 * *
87 ************************************************************************
88
89 For any two family instance modules that we import directly or indirectly, we
90 check whether the instances in the two modules are consistent, *unless* we can
91 be certain that the instances of the two modules have already been checked for
92 consistency during the compilation of modules that we import.
93
94 Why do we need to check? Consider
95 module X1 where module X2 where
96 data T1 data T2
97 type instance F T1 b = Int type instance F a T2 = Char
98 f1 :: F T1 a -> Int f2 :: Char -> F a T2
99 f1 x = x f2 x = x
100
101 Now if we import both X1 and X2 we could make (f2 . f1) :: Int -> Char.
102 Notice that neither instance is an orphan.
103
104 How do we know which pairs of modules have already been checked? Any pair of
105 modules where both modules occur in the `HscTypes.dep_finsts' set (of the
106 `HscTypes.Dependencies') of one of our directly imported modules must have
107 already been checked. Everything else, we check now. (So that we can be
108 certain that the modules in our `HscTypes.dep_finsts' are consistent.)
109 -}
110
111 -- The optimisation of overlap tests is based on determining pairs of modules
112 -- whose family instances need to be checked for consistency.
113 --
114 data ModulePair = ModulePair Module Module
115
116 -- canonical order of the components of a module pair
117 --
118 canon :: ModulePair -> (Module, Module)
119 canon (ModulePair m1 m2) | m1 < m2 = (m1, m2)
120 | otherwise = (m2, m1)
121
122 instance Eq ModulePair where
123 mp1 == mp2 = canon mp1 == canon mp2
124
125 instance Ord ModulePair where
126 mp1 `compare` mp2 = canon mp1 `compare` canon mp2
127
128 instance Outputable ModulePair where
129 ppr (ModulePair m1 m2) = angleBrackets (ppr m1 <> comma <+> ppr m2)
130
131 -- Sets of module pairs
132 --
133 type ModulePairSet = Map ModulePair ()
134
135 listToSet :: [ModulePair] -> ModulePairSet
136 listToSet l = Map.fromList (zip l (repeat ()))
137
138 checkFamInstConsistency :: [Module] -> [Module] -> TcM ()
139 checkFamInstConsistency famInstMods directlyImpMods
140 = do { dflags <- getDynFlags
141 ; (eps, hpt) <- getEpsAndHpt
142 ; let { -- Fetch the iface of a given module. Must succeed as
143 -- all directly imported modules must already have been loaded.
144 modIface mod =
145 case lookupIfaceByModule dflags hpt (eps_PIT eps) mod of
146 Nothing -> panicDoc "FamInst.checkFamInstConsistency"
147 (ppr mod $$ pprHPT hpt)
148 Just iface -> iface
149
150 ; hmiModule = mi_module . hm_iface
151 ; hmiFamInstEnv = extendFamInstEnvList emptyFamInstEnv
152 . md_fam_insts . hm_details
153 ; hpt_fam_insts = mkModuleEnv [ (hmiModule hmi, hmiFamInstEnv hmi)
154 | hmi <- eltsUFM hpt]
155 ; groups = map (dep_finsts . mi_deps . modIface)
156 directlyImpMods
157 ; okPairs = listToSet $ concatMap allPairs groups
158 -- instances of okPairs are consistent
159 ; criticalPairs = listToSet $ allPairs famInstMods
160 -- all pairs that we need to consider
161 ; toCheckPairs = Map.keys $ criticalPairs `Map.difference` okPairs
162 -- the difference gives us the pairs we need to check now
163 }
164
165 ; mapM_ (check hpt_fam_insts) toCheckPairs
166 }
167 where
168 allPairs [] = []
169 allPairs (m:ms) = map (ModulePair m) ms ++ allPairs ms
170
171 check hpt_fam_insts (ModulePair m1 m2)
172 = do { env1 <- getFamInsts hpt_fam_insts m1
173 ; env2 <- getFamInsts hpt_fam_insts m2
174 ; mapM_ (checkForConflicts (emptyFamInstEnv, env2))
175 (famInstEnvElts env1)
176 ; mapM_ (checkForInjectivityConflicts (emptyFamInstEnv,env2))
177 (famInstEnvElts env1)
178 }
179
180
181 getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
182 getFamInsts hpt_fam_insts mod
183 | Just env <- lookupModuleEnv hpt_fam_insts mod = return env
184 | otherwise = do { _ <- initIfaceTcRn (loadSysInterface doc mod)
185 ; eps <- getEps
186 ; return (expectJust "checkFamInstConsistency" $
187 lookupModuleEnv (eps_mod_fam_inst_env eps) mod) }
188 where
189 doc = ppr mod <+> text "is a family-instance module"
190
191 {-
192 ************************************************************************
193 * *
194 Lookup
195 * *
196 ************************************************************************
197
198 -}
199
200 -- | If @co :: T ts ~ rep_ty@ then:
201 --
202 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
203 --
204 -- Checks for a newtype, and for being saturated
205 -- Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion
206 tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion)
207 tcInstNewTyCon_maybe = instNewTyCon_maybe
208
209 -- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
210 -- there is no data family to unwrap.
211 -- Returns a Representational coercion
212 tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
213 -> (TyCon, [TcType], Coercion)
214 tcLookupDataFamInst fam_inst_envs tc tc_args
215 | Just (rep_tc, rep_args, co)
216 <- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
217 = (rep_tc, rep_args, co)
218 | otherwise
219 = (tc, tc_args, mkRepReflCo (mkTyConApp tc tc_args))
220
221 tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
222 -> Maybe (TyCon, [TcType], Coercion)
223 -- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a)
224 -- and returns a coercion between the two: co :: F [a] ~R FList a.
225 tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
226 | isDataFamilyTyCon tc
227 , match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args
228 , FamInstMatch { fim_instance = rep_fam@(FamInst { fi_axiom = ax
229 , fi_cvs = cvs })
230 , fim_tys = rep_args
231 , fim_cos = rep_cos } <- match
232 , let rep_tc = dataFamInstRepTyCon rep_fam
233 co = mkUnbranchedAxInstCo Representational ax rep_args
234 (mkCoVarCos cvs)
235 = ASSERT( null rep_cos ) -- See Note [Constrained family instances] in FamInstEnv
236 Just (rep_tc, rep_args, co)
237
238 | otherwise
239 = Nothing
240
241 -- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes,
242 -- potentially looking through newtype instances.
243 --
244 -- It is only used by the type inference engine (specifically, when
245 -- solving representational equality), and hence it is careful to unwrap
246 -- only if the relevant data constructor is in scope. That's why
247 -- it get a GlobalRdrEnv argument.
248 --
249 -- It is careful not to unwrap data/newtype instances if it can't
250 -- continue unwrapping. Such care is necessary for proper error
251 -- messages.
252 --
253 -- It does not look through type families.
254 -- It does not normalise arguments to a tycon.
255 --
256 -- Always produces a representational coercion.
257 tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
258 -> GlobalRdrEnv
259 -> Type
260 -> Maybe (TcCoercion, Type)
261 tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
262 -- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
263 = topNormaliseTypeX_maybe stepper ty
264 where
265 stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance
266
267 -- For newtype instances we take a double step or nothing, so that
268 -- we don't return the reprsentation type of the newtype instance,
269 -- which would lead to terrible error messages
270 unwrap_newtype_instance rec_nts tc tys
271 | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys
272 = modifyStepResultCo (co `mkTransCo`) $
273 unwrap_newtype rec_nts tc' tys'
274 | otherwise = NS_Done
275
276 unwrap_newtype rec_nts tc tys
277 | data_cons_in_scope tc
278 = unwrapNewTypeStepper rec_nts tc tys
279
280 | otherwise
281 = NS_Done
282
283 data_cons_in_scope :: TyCon -> Bool
284 data_cons_in_scope tc
285 = isWiredInName (tyConName tc) ||
286 (not (isAbstractTyCon tc) && all in_scope data_con_names)
287 where
288 data_con_names = map dataConName (tyConDataCons tc)
289 in_scope dc = not $ null $ lookupGRE_Name rdr_env dc
290
291 {-
292 ************************************************************************
293 * *
294 Extending the family instance environment
295 * *
296 ************************************************************************
297 -}
298
299 -- Add new locally-defined family instances
300 tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a
301 tcExtendLocalFamInstEnv fam_insts thing_inside
302 = do { env <- getGblEnv
303 ; (inst_env', fam_insts') <- foldlM addLocalFamInst
304 (tcg_fam_inst_env env, tcg_fam_insts env)
305 fam_insts
306 ; let env' = env { tcg_fam_insts = fam_insts'
307 , tcg_fam_inst_env = inst_env' }
308 ; setGblEnv env' thing_inside
309 }
310
311 -- Check that the proposed new instance is OK,
312 -- and then add it to the home inst env
313 -- This must be lazy in the fam_inst arguments, see Note [Lazy axiom match]
314 -- in FamInstEnv.hs
315 addLocalFamInst :: (FamInstEnv,[FamInst])
316 -> FamInst
317 -> TcM (FamInstEnv, [FamInst])
318 addLocalFamInst (home_fie, my_fis) fam_inst
319 -- home_fie includes home package and this module
320 -- my_fies is just the ones from this module
321 = do { traceTc "addLocalFamInst" (ppr fam_inst)
322
323 ; isGHCi <- getIsGHCi
324 ; mod <- getModule
325 ; traceTc "alfi" (ppr mod $$ ppr isGHCi)
326
327 -- In GHCi, we *override* any identical instances
328 -- that are also defined in the interactive context
329 -- See Note [Override identical instances in GHCi] in HscTypes
330 ; let home_fie'
331 | isGHCi = deleteFromFamInstEnv home_fie fam_inst
332 | otherwise = home_fie
333
334 -- Load imported instances, so that we report
335 -- overlaps correctly
336 ; eps <- getEps
337 ; let inst_envs = (eps_fam_inst_env eps, home_fie')
338 home_fie'' = extendFamInstEnv home_fie fam_inst
339
340 -- Check for conflicting instance decls and injectivity violations
341 ; no_conflict <- checkForConflicts inst_envs fam_inst
342 ; injectivity_ok <- checkForInjectivityConflicts inst_envs fam_inst
343
344 ; if no_conflict && injectivity_ok then
345 return (home_fie'', fam_inst : my_fis)
346 else
347 return (home_fie, my_fis) }
348
349 {-
350 ************************************************************************
351 * *
352 Checking an instance against conflicts with an instance env
353 * *
354 ************************************************************************
355
356 Check whether a single family instance conflicts with those in two instance
357 environments (one for the EPS and one for the HPT).
358 -}
359
360 checkForConflicts :: FamInstEnvs -> FamInst -> TcM Bool
361 checkForConflicts inst_envs fam_inst
362 = do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst
363 no_conflicts = null conflicts
364 ; traceTc "checkForConflicts" $
365 vcat [ ppr (map fim_instance conflicts)
366 , ppr fam_inst
367 -- , ppr inst_envs
368 ]
369 ; unless no_conflicts $ conflictInstErr fam_inst conflicts
370 ; return no_conflicts }
371
372 -- | Check whether a new open type family equation can be added without
373 -- violating injectivity annotation supplied by the user. Returns True when
374 -- this is possible and False if adding this equation would violate injectivity
375 -- annotation.
376 checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM Bool
377 checkForInjectivityConflicts instEnvs famInst
378 | isTypeFamilyTyCon tycon
379 -- type family is injective in at least one argument
380 , Injective inj <- familyTyConInjectivityInfo tycon = do
381 { let axiom = coAxiomSingleBranch fi_ax
382 conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst
383 -- see Note [Verifying injectivity annotation] in FamInstEnv
384 errs = makeInjectivityErrors fi_ax axiom inj conflicts
385 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err) errs
386 ; return (null errs)
387 }
388
389 -- if there was no injectivity annotation or tycon does not represent a
390 -- type family we report no conflicts
391 | otherwise = return True
392 where tycon = famInstTyCon famInst
393 fi_ax = fi_axiom famInst
394
395 -- | Build a list of injectivity errors together with their source locations.
396 makeInjectivityErrors
397 :: CoAxiom br -- ^ Type family for which we generate errors
398 -> CoAxBranch -- ^ Currently checked equation (represented by axiom)
399 -> [Bool] -- ^ Injectivity annotation
400 -> [CoAxBranch] -- ^ List of injectivity conflicts
401 -> [(SDoc, SrcSpan)]
402 makeInjectivityErrors fi_ax axiom inj conflicts
403 = ASSERT2( any id inj, text "No injective type variables" )
404 let lhs = coAxBranchLHS axiom
405 rhs = coAxBranchRHS axiom
406
407 are_conflicts = not $ null conflicts
408 unused_inj_tvs = unusedInjTvsInRHS (coAxiomTyCon fi_ax) inj lhs rhs
409 inj_tvs_unused = not $ and (isEmptyVarSet <$> unused_inj_tvs)
410 tf_headed = isTFHeaded rhs
411 bare_variables = bareTvInRHSViolated lhs rhs
412 wrong_bare_rhs = not $ null bare_variables
413
414 err_builder herald eqns
415 = ( hang herald
416 2 (vcat (map (pprCoAxBranch fi_ax) eqns))
417 , coAxBranchSpan (head eqns) )
418 errorIf p f = if p then [f err_builder axiom] else []
419 in errorIf are_conflicts (conflictInjInstErr conflicts )
420 ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs)
421 ++ errorIf tf_headed tfHeadedErr
422 ++ errorIf wrong_bare_rhs (bareVariableInRHSErr bare_variables)
423
424
425 -- | Return a list of type variables that the function is injective in and that
426 -- do not appear on injective positions in the RHS of a family instance
427 -- declaration. The returned Pair includes invisible vars followed by visible ones
428 unusedInjTvsInRHS :: TyCon -> [Bool] -> [Type] -> Type -> Pair TyVarSet
429 -- INVARIANT: [Bool] list contains at least one True value
430 -- See Note [Verifying injectivity annotation]. This function implements fourth
431 -- check described there.
432 -- In theory, instead of implementing this whole check in this way, we could
433 -- attempt to unify equation with itself. We would reject exactly the same
434 -- equations but this method gives us more precise error messages by returning
435 -- precise names of variables that are not mentioned in the RHS.
436 unusedInjTvsInRHS tycon injList lhs rhs =
437 (`minusVarSet` injRhsVars) <$> injLHSVars
438 where
439 -- set of type and kind variables in which type family is injective
440 (invis_pairs, vis_pairs)
441 = partitionInvisibles tycon snd (zipEqual "unusedInjTvsInRHS" injList lhs)
442 invis_lhs = uncurry filterByList $ unzip invis_pairs
443 vis_lhs = uncurry filterByList $ unzip vis_pairs
444
445 invis_vars = tyCoVarsOfTypes invis_lhs
446 Pair invis_vars' vis_vars = splitVisVarsOfTypes vis_lhs
447 injLHSVars
448 = Pair (invis_vars `minusVarSet` vis_vars `unionVarSet` invis_vars')
449 vis_vars
450
451 -- set of type variables appearing in the RHS on an injective position.
452 -- For all returned variables we assume their associated kind variables
453 -- also appear in the RHS.
454 injRhsVars = collectInjVars rhs
455
456 -- Collect all type variables that are either arguments to a type
457 -- constructor or to injective type families.
458 collectInjVars :: Type -> VarSet
459 collectInjVars (TyVarTy v)
460 = unitVarSet v `unionVarSet` collectInjVars (tyVarKind v)
461 collectInjVars (TyConApp tc tys)
462 | isTypeFamilyTyCon tc = collectInjTFVars tys
463 (familyTyConInjectivityInfo tc)
464 | otherwise = mapUnionVarSet collectInjVars tys
465 collectInjVars (LitTy {})
466 = emptyVarSet
467 collectInjVars (ForAllTy (Anon arg) res)
468 = collectInjVars arg `unionVarSet` collectInjVars res
469 collectInjVars (AppTy fun arg)
470 = collectInjVars fun `unionVarSet` collectInjVars arg
471 -- no forall types in the RHS of a type family
472 collectInjVars (ForAllTy _ _) =
473 panic "unusedInjTvsInRHS.collectInjVars"
474 collectInjVars (CastTy ty _) = collectInjVars ty
475 collectInjVars (CoercionTy {}) = emptyVarSet
476
477 collectInjTFVars :: [Type] -> Injectivity -> VarSet
478 collectInjTFVars _ NotInjective
479 = emptyVarSet
480 collectInjTFVars tys (Injective injList)
481 = mapUnionVarSet collectInjVars (filterByList injList tys)
482
483
484 -- | Is type headed by a type family application?
485 isTFHeaded :: Type -> Bool
486 -- See Note [Verifying injectivity annotation]. This function implements third
487 -- check described there.
488 isTFHeaded ty | Just ty' <- coreView ty
489 = isTFHeaded ty'
490 isTFHeaded ty | (TyConApp tc args) <- ty
491 , isTypeFamilyTyCon tc
492 = tyConArity tc == length args
493 isTFHeaded _ = False
494
495
496 -- | If a RHS is a bare type variable return a set of LHS patterns that are not
497 -- bare type variables.
498 bareTvInRHSViolated :: [Type] -> Type -> [Type]
499 -- See Note [Verifying injectivity annotation]. This function implements second
500 -- check described there.
501 bareTvInRHSViolated pats rhs | isTyVarTy rhs
502 = filter (not . isTyVarTy) pats
503 bareTvInRHSViolated _ _ = []
504
505
506 conflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
507 conflictInstErr fam_inst conflictingMatch
508 | (FamInstMatch { fim_instance = confInst }) : _ <- conflictingMatch
509 = let (err, span) = makeFamInstsErr
510 (text "Conflicting family instance declarations:")
511 [fam_inst, confInst]
512 in setSrcSpan span $ addErr err
513 | otherwise
514 = panic "conflictInstErr"
515
516 -- | Type of functions that use error message and a list of axioms to build full
517 -- error message (with a source location) for injective type families.
518 type InjErrorBuilder = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
519
520 -- | Build injecivity error herald common to all injectivity errors.
521 injectivityErrorHerald :: Bool -> SDoc
522 injectivityErrorHerald isSingular =
523 text "Type family equation" <> s isSingular <+> text "violate" <>
524 s (not isSingular) <+> text "injectivity annotation" <>
525 if isSingular then dot else colon
526 -- Above is an ugly hack. We want this: "sentence. herald:" (note the dot and
527 -- colon). But if herald is empty we want "sentence:" (note the colon). We
528 -- can't test herald for emptiness so we rely on the fact that herald is empty
529 -- only when isSingular is False. If herald is non empty it must end with a
530 -- colon.
531 where
532 s False = text "s"
533 s True = empty
534
535 -- | Build error message for a pair of equations violating an injectivity
536 -- annotation.
537 conflictInjInstErr :: [CoAxBranch] -> InjErrorBuilder -> CoAxBranch
538 -> (SDoc, SrcSpan)
539 conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
540 | confEqn : _ <- conflictingEqns
541 = errorBuilder (injectivityErrorHerald False) [confEqn, tyfamEqn]
542 | otherwise
543 = panic "conflictInjInstErr"
544
545 -- | Build error message for equation with injective type variables unused in
546 -- the RHS.
547 unusedInjectiveVarsErr :: Pair TyVarSet -> InjErrorBuilder -> CoAxBranch
548 -> (SDoc, SrcSpan)
549 unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn
550 = errorBuilder (injectivityErrorHerald True $$ msg)
551 [tyfamEqn]
552 where
553 tvs = varSetElemsWellScoped (invis_vars `unionVarSet` vis_vars)
554 has_types = not $ isEmptyVarSet vis_vars
555 has_kinds = not $ isEmptyVarSet invis_vars
556
557 doc = sep [ what <+> text "variable" <>
558 plural tvs <+> pprQuotedList tvs
559 , text "cannot be inferred from the right-hand side." ]
560 what = case (has_types, has_kinds) of
561 (True, True) -> text "Type and kind"
562 (True, False) -> text "Type"
563 (False, True) -> text "Kind"
564 (False, False) -> pprPanic "mkUnusedInjectiveVarsErr" $ ppr tvs
565 print_kinds_info = sdocWithDynFlags $ \ dflags ->
566 if has_kinds && not (gopt Opt_PrintExplicitKinds dflags)
567 then text "(enabling -fprint-explicit-kinds might help)"
568 else empty
569 msg = doc $$ print_kinds_info $$
570 text "In the type family equation:"
571
572 -- | Build error message for equation that has a type family call at the top
573 -- level of RHS
574 tfHeadedErr :: InjErrorBuilder -> CoAxBranch
575 -> (SDoc, SrcSpan)
576 tfHeadedErr errorBuilder famInst
577 = errorBuilder (injectivityErrorHerald True $$
578 text "RHS of injective type family equation cannot" <+>
579 text "be a type family:") [famInst]
580
581 -- | Build error message for equation that has a bare type variable in the RHS
582 -- but LHS pattern is not a bare type variable.
583 bareVariableInRHSErr :: [Type] -> InjErrorBuilder -> CoAxBranch
584 -> (SDoc, SrcSpan)
585 bareVariableInRHSErr tys errorBuilder famInst
586 = errorBuilder (injectivityErrorHerald True $$
587 text "RHS of injective type family equation is a bare" <+>
588 text "type variable" $$
589 text "but these LHS type and kind patterns are not bare" <+>
590 text "variables:" <+> pprQuotedList tys) [famInst]
591
592
593 makeFamInstsErr :: SDoc -> [FamInst] -> (SDoc, SrcSpan)
594 makeFamInstsErr herald insts
595 = ASSERT( not (null insts) )
596 ( hang herald
597 2 (vcat [ pprCoAxBranchHdr (famInstAxiom fi) 0
598 | fi <- sorted ])
599 , srcSpan )
600 where
601 getSpan = getSrcLoc . famInstAxiom
602 sorted = sortWith getSpan insts
603 fi1 = head sorted
604 srcSpan = coAxBranchSpan (coAxiomSingleBranch (famInstAxiom fi1))
605 -- The sortWith just arranges that instances are dislayed in order
606 -- of source location, which reduced wobbling in error messages,
607 -- and is better for users
608
609 tcGetFamInstEnvs :: TcM FamInstEnvs
610 -- Gets both the external-package inst-env
611 -- and the home-pkg inst env (includes module being compiled)
612 tcGetFamInstEnvs
613 = do { eps <- getEps; env <- getGblEnv
614 ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }