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