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