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