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