6a38f2f8d5fd948be454b2c50a1718ac36668261
[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 checkRecFamInstConsistency,
11 newFamInst,
12
13 -- * Injectivity
14 makeInjectivityErrors, injTyVarsOfType, injTyVarsOfTypes
15 ) where
16
17 import HscTypes
18 import FamInstEnv
19 import InstEnv( roughMatchTcs )
20 import Coercion
21 import TcEvidence
22 import LoadIface
23 import TcRnMonad
24 import SrcLoc
25 import TyCon
26 import TcType
27 import CoAxiom
28 import DynFlags
29 import Module
30 import Outputable
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 Bag( Bag, unionBags, unitBag )
43 import Control.Monad
44 import Unique
45 import NameEnv
46 import Data.Set (Set)
47 import qualified Data.Set as Set
48 import Data.List
49
50 #include "HsVersions.h"
51
52 {-
53 ************************************************************************
54 * *
55 Making a FamInst
56 * *
57 ************************************************************************
58 -}
59
60 -- All type variables in a FamInst must be fresh. This function
61 -- creates the fresh variables and applies the necessary substitution
62 -- It is defined here to avoid a dependency from FamInstEnv on the monad
63 -- code.
64
65 newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
66 -- Freshen the type variables of the FamInst branches
67 -- Called from the vectoriser monad too, hence the rather general type
68 newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
69 = ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
70 ASSERT2( tyCoVarsOfType rhs `subVarSet` tcv_set, text "rhs" <+> pp_ax )
71 ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
72 do { (subst, tvs') <- freshenTyVarBndrs tvs
73 ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
74 ; return (FamInst { fi_fam = tyConName fam_tc
75 , fi_flavor = flavor
76 , fi_tcs = roughMatchTcs lhs
77 , fi_tvs = tvs'
78 , fi_cvs = cvs'
79 , fi_tys = substTys subst lhs
80 , fi_rhs = substTy subst rhs
81 , fi_axiom = axiom }) }
82 where
83 lhs_kind = typeKind (mkTyConApp fam_tc lhs)
84 rhs_kind = typeKind rhs
85 tcv_set = mkVarSet (tvs ++ cvs)
86 pp_ax = pprCoAxiom axiom
87 CoAxBranch { cab_tvs = tvs
88 , cab_cvs = cvs
89 , cab_lhs = lhs
90 , cab_rhs = rhs } = coAxiomSingleBranch axiom
91
92
93 {-
94 ************************************************************************
95 * *
96 Optimised overlap checking for family instances
97 * *
98 ************************************************************************
99
100 Note [Checking family instance consistency]
101 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
102 For any two family instance modules that we import directly or indirectly, we
103 check whether the instances in the two modules are consistent, *unless* we can
104 be certain that the instances of the two modules have already been checked for
105 consistency during the compilation of modules that we import.
106
107 Why do we need to check? Consider
108 module X1 where module X2 where
109 data T1 data T2
110 type instance F T1 b = Int type instance F a T2 = Char
111 f1 :: F T1 a -> Int f2 :: Char -> F a T2
112 f1 x = x f2 x = x
113
114 Now if we import both X1 and X2 we could make (f2 . f1) :: Int -> Char.
115 Notice that neither instance is an orphan.
116
117 How do we know which pairs of modules have already been checked? Any pair of
118 modules where both modules occur in the `HscTypes.dep_finsts' set (of the
119 `HscTypes.Dependencies') of one of our directly imported modules must have
120 already been checked. Everything else, we check now. (So that we can be
121 certain that the modules in our `HscTypes.dep_finsts' are consistent.)
122
123 There is some fancy footwork regarding hs-boot module loops, see
124 Note [Don't check hs-boot type family instances too early]
125 -}
126
127 -- The optimisation of overlap tests is based on determining pairs of modules
128 -- whose family instances need to be checked for consistency.
129 --
130 data ModulePair = ModulePair Module Module
131 -- Invariant: first Module < second Module
132 -- use the smart constructor
133
134 -- | Smart constructor that establishes the invariant
135 modulePair :: Module -> Module -> ModulePair
136 modulePair a b
137 | a < b = ModulePair a b
138 | otherwise = ModulePair b a
139
140 instance Eq ModulePair where
141 (ModulePair a1 b1) == (ModulePair a2 b2) = a1 == a2 && b1 == b2
142
143 instance Ord ModulePair where
144 (ModulePair a1 b1) `compare` (ModulePair a2 b2) =
145 nonDetCmpModule a1 a2 `thenCmp`
146 nonDetCmpModule b1 b2
147 -- See Note [ModulePairSet determinism and performance]
148
149 instance Outputable ModulePair where
150 ppr (ModulePair m1 m2) = angleBrackets (ppr m1 <> comma <+> ppr m2)
151
152 -- Fast, nondeterministic comparison on Module. Don't use when the ordering
153 -- can change the ABI. See Note [ModulePairSet determinism and performance]
154 nonDetCmpModule :: Module -> Module -> Ordering
155 nonDetCmpModule a b =
156 nonDetCmpUnique (getUnique $ moduleUnitId a) (getUnique $ moduleUnitId b)
157 `thenCmp`
158 nonDetCmpUnique (getUnique $ moduleName a) (getUnique $ moduleName b)
159
160 type ModulePairSet = Set ModulePair
161 {-
162 Note [ModulePairSet determinism and performance]
163 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
164 The size of ModulePairSet is quadratic in the number of modules.
165 The Ord instance for Module uses string comparison which is linear in the
166 length of ModuleNames and UnitIds. This adds up to a significant cost, see
167 #12191.
168
169 To get reasonable performance ModulePairSet uses nondeterministic ordering
170 on Module based on Uniques. It doesn't affect the ABI, because it only
171 determines the order the modules are checked for family instance consistency.
172 See Note [Unique Determinism] in Unique
173 -}
174
175 listToSet :: [ModulePair] -> ModulePairSet
176 listToSet l = Set.fromList l
177
178 -- | Check family instance consistency, given:
179 --
180 -- 1. The list of all modules transitively imported by us
181 -- which define a family instance (these are the ones
182 -- we have to check for consistency), and
183 --
184 -- 2. The list of modules which we directly imported
185 -- (these specify the sets of family instance defining
186 -- modules which are already known to be consistent).
187 --
188 -- See Note [Checking family instance consistency] for more
189 -- details.
190 --
191 -- This function doesn't check ALL instances for consistency,
192 -- only ones that aren't involved in recursive knot-tying
193 -- loops; see Note [Don't check hs-boot type family instances too early].
194 -- It returns a modified 'TcGblEnv' that has saved the
195 -- instances that need to be checked later; use 'checkRecFamInstConsistency'
196 -- to check those.
197 checkFamInstConsistency :: [Module] -> [Module] -> TcM TcGblEnv
198 checkFamInstConsistency famInstMods directlyImpMods
199 = do { dflags <- getDynFlags
200 ; (eps, hpt) <- getEpsAndHpt
201 ; let { -- Fetch the iface of a given module. Must succeed as
202 -- all directly imported modules must already have been loaded.
203 modIface mod =
204 case lookupIfaceByModule dflags hpt (eps_PIT eps) mod of
205 Nothing -> panicDoc "FamInst.checkFamInstConsistency"
206 (ppr mod $$ pprHPT hpt)
207 Just iface -> iface
208
209 ; hmiModule = mi_module . hm_iface
210 ; hmiFamInstEnv = extendFamInstEnvList emptyFamInstEnv
211 . md_fam_insts . hm_details
212 ; hpt_fam_insts = mkModuleEnv [ (hmiModule hmi, hmiFamInstEnv hmi)
213 | hmi <- eltsHpt hpt]
214 ; groups = map (dep_finsts . mi_deps . modIface)
215 directlyImpMods
216 ; okPairs = listToSet $ concatMap allPairs groups
217 -- instances of okPairs are consistent
218 ; criticalPairs = listToSet $ allPairs famInstMods
219 -- all pairs that we need to consider
220 ; toCheckPairs =
221 Set.elems $ criticalPairs `Set.difference` okPairs
222 -- the difference gives us the pairs we need to check now
223 -- See Note [ModulePairSet determinism and performance]
224 }
225
226 ; pending_checks <- mapM (check hpt_fam_insts) toCheckPairs
227 ; tcg_env <- getGblEnv
228 ; return tcg_env { tcg_pending_fam_checks
229 = foldl' (plusNameEnv_C (++)) emptyNameEnv pending_checks }
230 }
231 where
232 allPairs [] = []
233 allPairs (m:ms) = map (modulePair m) ms ++ allPairs ms
234
235 check hpt_fam_insts (ModulePair m1 m2)
236 = do { env1' <- getFamInsts hpt_fam_insts m1
237 ; env2' <- getFamInsts hpt_fam_insts m2
238 -- We're checking each element of env1 against env2.
239 -- The cost of that is dominated by the size of env1, because
240 -- for each instance in env1 we look it up in the type family
241 -- environment env2, and lookup is cheap.
242 -- The code below ensures that env1 is the smaller environment.
243 ; let sizeE1 = famInstEnvSize env1'
244 sizeE2 = famInstEnvSize env2'
245 (env1, env2) = if sizeE1 < sizeE2 then (env1', env2')
246 else (env2', env1')
247 -- Note [Don't check hs-boot type family instances too early]
248 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
249 -- Family instance consistency checking involves checking that
250 -- the family instances of our imported modules are consistent with
251 -- one another; this might lead you to think that this process
252 -- has nothing to do with the module we are about to typecheck.
253 -- Not so! If a type family was defined in the hs-boot file
254 -- of the current module, we are NOT allowed to poke the TyThing
255 -- for this family: since we haven't typechecked the definition
256 -- yet (checkFamInstConsistency is called during renaming),
257 -- we won't be able to find our local copy in if_rec_types.
258 -- Failing to do this lead to #11062.
259 --
260 -- So, we have to defer the checks for family instances that
261 -- refer to families that are locally defined.
262 --
263 -- See also Note [Tying the knot] and Note [Type-checking inside the knot]
264 -- for why we are doing this at all.
265 ; this_mod <- getModule
266 ; let (check_now, check_later)
267 -- NB: == this_mod only holds if there's an hs-boot file;
268 -- otherwise we cannot possible see instances for families
269 -- defined by the module we are compiling in imports.
270 = partition ((/= this_mod) . nameModule . fi_fam)
271 (famInstEnvElts env1)
272 ; mapM_ (checkForConflicts (emptyFamInstEnv, env2)) check_now
273 ; mapM_ (checkForInjectivityConflicts (emptyFamInstEnv,env2)) check_now
274 ; let check_later_map =
275 extendNameEnvList_C (++) emptyNameEnv
276 [(fi_fam finst, [finst]) | finst <- check_later]
277 ; return (mapNameEnv (\xs -> [(xs, env2)]) check_later_map)
278 }
279
280 -- | Given a 'TyCon' that has been incorporated into the type
281 -- environment (the knot is tied), if it is a type family, check
282 -- that all deferred instances for it are consistent.
283 -- See Note [Don't check hs-boot type family instances too early]
284 checkRecFamInstConsistency :: TyCon -> TcM ()
285 checkRecFamInstConsistency tc = do
286 tcg_env <- getGblEnv
287 let checkConsistency tc
288 | isFamilyTyCon tc
289 , Just pairs <- lookupNameEnv (tcg_pending_fam_checks tcg_env)
290 (tyConName tc)
291 = forM_ pairs $ \(check_now, env2) -> do
292 mapM_ (checkForConflicts (emptyFamInstEnv, env2)) check_now
293 mapM_ (checkForInjectivityConflicts (emptyFamInstEnv,env2)) check_now
294 | otherwise
295 = return ()
296 checkConsistency tc
297
298
299 getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
300 getFamInsts hpt_fam_insts mod
301 | Just env <- lookupModuleEnv hpt_fam_insts mod = return env
302 | otherwise = do { _ <- initIfaceTcRn (loadSysInterface doc mod)
303 ; eps <- getEps
304 ; return (expectJust "checkFamInstConsistency" $
305 lookupModuleEnv (eps_mod_fam_inst_env eps) mod) }
306 where
307 doc = ppr mod <+> text "is a family-instance module"
308
309 {-
310 ************************************************************************
311 * *
312 Lookup
313 * *
314 ************************************************************************
315
316 -}
317
318 -- | If @co :: T ts ~ rep_ty@ then:
319 --
320 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
321 --
322 -- Checks for a newtype, and for being saturated
323 -- Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion
324 tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion)
325 tcInstNewTyCon_maybe = instNewTyCon_maybe
326
327 -- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
328 -- there is no data family to unwrap.
329 -- Returns a Representational coercion
330 tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
331 -> (TyCon, [TcType], Coercion)
332 tcLookupDataFamInst fam_inst_envs tc tc_args
333 | Just (rep_tc, rep_args, co)
334 <- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
335 = (rep_tc, rep_args, co)
336 | otherwise
337 = (tc, tc_args, mkRepReflCo (mkTyConApp tc tc_args))
338
339 tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
340 -> Maybe (TyCon, [TcType], Coercion)
341 -- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a)
342 -- and returns a coercion between the two: co :: F [a] ~R FList a.
343 tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
344 | isDataFamilyTyCon tc
345 , match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args
346 , FamInstMatch { fim_instance = rep_fam@(FamInst { fi_axiom = ax
347 , fi_cvs = cvs })
348 , fim_tys = rep_args
349 , fim_cos = rep_cos } <- match
350 , let rep_tc = dataFamInstRepTyCon rep_fam
351 co = mkUnbranchedAxInstCo Representational ax rep_args
352 (mkCoVarCos cvs)
353 = ASSERT( null rep_cos ) -- See Note [Constrained family instances] in FamInstEnv
354 Just (rep_tc, rep_args, co)
355
356 | otherwise
357 = Nothing
358
359 -- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes,
360 -- potentially looking through newtype /instances/.
361 --
362 -- It is only used by the type inference engine (specifically, when
363 -- solving representational equality), and hence it is careful to unwrap
364 -- only if the relevant data constructor is in scope. That's why
365 -- it get a GlobalRdrEnv argument.
366 --
367 -- It is careful not to unwrap data/newtype instances if it can't
368 -- continue unwrapping. Such care is necessary for proper error
369 -- messages.
370 --
371 -- It does not look through type families.
372 -- It does not normalise arguments to a tycon.
373 --
374 -- If the result is Just (rep_ty, (co, gres), rep_ty), then
375 -- co : ty ~R rep_ty
376 -- gres are the GREs for the data constructors that
377 -- had to be in scope
378 tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
379 -> GlobalRdrEnv
380 -> Type
381 -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
382 tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
383 -- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
384 = topNormaliseTypeX stepper plus ty
385 where
386 plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion)
387 -> (Bag GlobalRdrElt, TcCoercion)
388 plus (gres1, co1) (gres2, co2) = ( gres1 `unionBags` gres2
389 , co1 `mkTransCo` co2 )
390
391 stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
392 stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance
393
394 -- For newtype instances we take a double step or nothing, so that
395 -- we don't return the representation type of the newtype instance,
396 -- which would lead to terrible error messages
397 unwrap_newtype_instance rec_nts tc tys
398 | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys
399 = mapStepResult (\(gres, co1) -> (gres, co `mkTransCo` co1)) $
400 unwrap_newtype rec_nts tc' tys'
401 | otherwise = NS_Done
402
403 unwrap_newtype rec_nts tc tys
404 | Just con <- newTyConDataCon_maybe tc
405 , Just gre <- lookupGRE_Name rdr_env (dataConName con)
406 -- This is where we check that the
407 -- data constructor is in scope
408 = mapStepResult (\co -> (unitBag gre, co)) $
409 unwrapNewTypeStepper rec_nts tc tys
410
411 | otherwise
412 = NS_Done
413
414 {-
415 ************************************************************************
416 * *
417 Extending the family instance environment
418 * *
419 ************************************************************************
420 -}
421
422 -- Add new locally-defined family instances
423 tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a
424 tcExtendLocalFamInstEnv fam_insts thing_inside
425 = do { env <- getGblEnv
426 ; (inst_env', fam_insts') <- foldlM addLocalFamInst
427 (tcg_fam_inst_env env, tcg_fam_insts env)
428 fam_insts
429 ; let env' = env { tcg_fam_insts = fam_insts'
430 , tcg_fam_inst_env = inst_env' }
431 ; setGblEnv env' thing_inside
432 }
433
434 -- Check that the proposed new instance is OK,
435 -- and then add it to the home inst env
436 -- This must be lazy in the fam_inst arguments, see Note [Lazy axiom match]
437 -- in FamInstEnv.hs
438 addLocalFamInst :: (FamInstEnv,[FamInst])
439 -> FamInst
440 -> TcM (FamInstEnv, [FamInst])
441 addLocalFamInst (home_fie, my_fis) fam_inst
442 -- home_fie includes home package and this module
443 -- my_fies is just the ones from this module
444 = do { traceTc "addLocalFamInst" (ppr fam_inst)
445
446 -- Unlike the case of class instances, don't override existing
447 -- instances in GHCi; it's unsound. See #7102.
448
449 ; mod <- getModule
450 ; traceTc "alfi" (ppr mod)
451
452 -- Load imported instances, so that we report
453 -- overlaps correctly
454 ; eps <- getEps
455 ; let inst_envs = (eps_fam_inst_env eps, home_fie)
456 home_fie' = extendFamInstEnv home_fie fam_inst
457
458 -- Check for conflicting instance decls and injectivity violations
459 ; no_conflict <- checkForConflicts inst_envs fam_inst
460 ; injectivity_ok <- checkForInjectivityConflicts inst_envs fam_inst
461
462 ; if no_conflict && injectivity_ok then
463 return (home_fie', fam_inst : my_fis)
464 else
465 return (home_fie, my_fis) }
466
467 {-
468 ************************************************************************
469 * *
470 Checking an instance against conflicts with an instance env
471 * *
472 ************************************************************************
473
474 Check whether a single family instance conflicts with those in two instance
475 environments (one for the EPS and one for the HPT).
476 -}
477
478 checkForConflicts :: FamInstEnvs -> FamInst -> TcM Bool
479 checkForConflicts inst_envs fam_inst
480 = do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst
481 no_conflicts = null conflicts
482 ; traceTc "checkForConflicts" $
483 vcat [ ppr (map fim_instance conflicts)
484 , ppr fam_inst
485 -- , ppr inst_envs
486 ]
487 ; unless no_conflicts $ conflictInstErr fam_inst conflicts
488 ; return no_conflicts }
489
490 -- | Check whether a new open type family equation can be added without
491 -- violating injectivity annotation supplied by the user. Returns True when
492 -- this is possible and False if adding this equation would violate injectivity
493 -- annotation.
494 checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM Bool
495 checkForInjectivityConflicts instEnvs famInst
496 | isTypeFamilyTyCon tycon
497 -- type family is injective in at least one argument
498 , Injective inj <- familyTyConInjectivityInfo tycon = do
499 { let axiom = coAxiomSingleBranch fi_ax
500 conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst
501 -- see Note [Verifying injectivity annotation] in FamInstEnv
502 errs = makeInjectivityErrors fi_ax axiom inj conflicts
503 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err) errs
504 ; return (null errs)
505 }
506
507 -- if there was no injectivity annotation or tycon does not represent a
508 -- type family we report no conflicts
509 | otherwise = return True
510 where tycon = famInstTyCon famInst
511 fi_ax = fi_axiom famInst
512
513 -- | Build a list of injectivity errors together with their source locations.
514 makeInjectivityErrors
515 :: CoAxiom br -- ^ Type family for which we generate errors
516 -> CoAxBranch -- ^ Currently checked equation (represented by axiom)
517 -> [Bool] -- ^ Injectivity annotation
518 -> [CoAxBranch] -- ^ List of injectivity conflicts
519 -> [(SDoc, SrcSpan)]
520 makeInjectivityErrors fi_ax axiom inj conflicts
521 = ASSERT2( any id inj, text "No injective type variables" )
522 let lhs = coAxBranchLHS axiom
523 rhs = coAxBranchRHS axiom
524
525 are_conflicts = not $ null conflicts
526 unused_inj_tvs = unusedInjTvsInRHS (coAxiomTyCon fi_ax) inj lhs rhs
527 inj_tvs_unused = not $ and (isEmptyVarSet <$> unused_inj_tvs)
528 tf_headed = isTFHeaded rhs
529 bare_variables = bareTvInRHSViolated lhs rhs
530 wrong_bare_rhs = not $ null bare_variables
531
532 err_builder herald eqns
533 = ( hang herald
534 2 (vcat (map (pprCoAxBranch fi_ax) eqns))
535 , coAxBranchSpan (head eqns) )
536 errorIf p f = if p then [f err_builder axiom] else []
537 in errorIf are_conflicts (conflictInjInstErr conflicts )
538 ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs)
539 ++ errorIf tf_headed tfHeadedErr
540 ++ errorIf wrong_bare_rhs (bareVariableInRHSErr bare_variables)
541
542
543 -- | Return a list of type variables that the function is injective in and that
544 -- do not appear on injective positions in the RHS of a family instance
545 -- declaration. The returned Pair includes invisible vars followed by visible ones
546 unusedInjTvsInRHS :: TyCon -> [Bool] -> [Type] -> Type -> Pair TyVarSet
547 -- INVARIANT: [Bool] list contains at least one True value
548 -- See Note [Verifying injectivity annotation]. This function implements fourth
549 -- check described there.
550 -- In theory, instead of implementing this whole check in this way, we could
551 -- attempt to unify equation with itself. We would reject exactly the same
552 -- equations but this method gives us more precise error messages by returning
553 -- precise names of variables that are not mentioned in the RHS.
554 unusedInjTvsInRHS tycon injList lhs rhs =
555 (`minusVarSet` injRhsVars) <$> injLHSVars
556 where
557 -- set of type and kind variables in which type family is injective
558 (invis_pairs, vis_pairs)
559 = partitionInvisibles tycon snd (zipEqual "unusedInjTvsInRHS" injList lhs)
560 invis_lhs = uncurry filterByList $ unzip invis_pairs
561 vis_lhs = uncurry filterByList $ unzip vis_pairs
562
563 invis_vars = tyCoVarsOfTypes invis_lhs
564 Pair invis_vars' vis_vars = splitVisVarsOfTypes vis_lhs
565 injLHSVars
566 = Pair (invis_vars `minusVarSet` vis_vars `unionVarSet` invis_vars')
567 vis_vars
568
569 -- set of type variables appearing in the RHS on an injective position.
570 -- For all returned variables we assume their associated kind variables
571 -- also appear in the RHS.
572 injRhsVars = injTyVarsOfType rhs
573
574 injTyVarsOfType :: TcTauType -> TcTyVarSet
575 -- Collect all type variables that are either arguments to a type
576 -- constructor or to /injective/ type families.
577 -- Determining the overall type determines thes variables
578 --
579 -- E.g. Suppose F is injective in its second arg, but not its first
580 -- then injVarOfType (Either a (F [b] (a,c))) = {a,c}
581 -- Determining the overall type determines a,c but not b.
582 injTyVarsOfType (TyVarTy v)
583 = unitVarSet v `unionVarSet` injTyVarsOfType (tyVarKind v)
584 injTyVarsOfType (TyConApp tc tys)
585 | isTypeFamilyTyCon tc
586 = case familyTyConInjectivityInfo tc of
587 NotInjective -> emptyVarSet
588 Injective inj -> injTyVarsOfTypes (filterByList inj tys)
589 | otherwise
590 = injTyVarsOfTypes tys
591 injTyVarsOfType (LitTy {})
592 = emptyVarSet
593 injTyVarsOfType (FunTy arg res)
594 = injTyVarsOfType arg `unionVarSet` injTyVarsOfType res
595 injTyVarsOfType (AppTy fun arg)
596 = injTyVarsOfType fun `unionVarSet` injTyVarsOfType arg
597 -- No forall types in the RHS of a type family
598 injTyVarsOfType (CastTy ty _) = injTyVarsOfType ty
599 injTyVarsOfType (CoercionTy {}) = emptyVarSet
600 injTyVarsOfType (ForAllTy {}) =
601 panic "unusedInjTvsInRHS.injTyVarsOfType"
602
603 injTyVarsOfTypes :: [Type] -> VarSet
604 injTyVarsOfTypes tys = mapUnionVarSet injTyVarsOfType tys
605
606 -- | Is type headed by a type family application?
607 isTFHeaded :: Type -> Bool
608 -- See Note [Verifying injectivity annotation]. This function implements third
609 -- check described there.
610 isTFHeaded ty | Just ty' <- coreView ty
611 = isTFHeaded ty'
612 isTFHeaded ty | (TyConApp tc args) <- ty
613 , isTypeFamilyTyCon tc
614 = tyConArity tc == length args
615 isTFHeaded _ = False
616
617
618 -- | If a RHS is a bare type variable return a set of LHS patterns that are not
619 -- bare type variables.
620 bareTvInRHSViolated :: [Type] -> Type -> [Type]
621 -- See Note [Verifying injectivity annotation]. This function implements second
622 -- check described there.
623 bareTvInRHSViolated pats rhs | isTyVarTy rhs
624 = filter (not . isTyVarTy) pats
625 bareTvInRHSViolated _ _ = []
626
627
628 conflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
629 conflictInstErr fam_inst conflictingMatch
630 | (FamInstMatch { fim_instance = confInst }) : _ <- conflictingMatch
631 = let (err, span) = makeFamInstsErr
632 (text "Conflicting family instance declarations:")
633 [fam_inst, confInst]
634 in setSrcSpan span $ addErr err
635 | otherwise
636 = panic "conflictInstErr"
637
638 -- | Type of functions that use error message and a list of axioms to build full
639 -- error message (with a source location) for injective type families.
640 type InjErrorBuilder = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
641
642 -- | Build injecivity error herald common to all injectivity errors.
643 injectivityErrorHerald :: Bool -> SDoc
644 injectivityErrorHerald isSingular =
645 text "Type family equation" <> s isSingular <+> text "violate" <>
646 s (not isSingular) <+> text "injectivity annotation" <>
647 if isSingular then dot else colon
648 -- Above is an ugly hack. We want this: "sentence. herald:" (note the dot and
649 -- colon). But if herald is empty we want "sentence:" (note the colon). We
650 -- can't test herald for emptiness so we rely on the fact that herald is empty
651 -- only when isSingular is False. If herald is non empty it must end with a
652 -- colon.
653 where
654 s False = text "s"
655 s True = empty
656
657 -- | Build error message for a pair of equations violating an injectivity
658 -- annotation.
659 conflictInjInstErr :: [CoAxBranch] -> InjErrorBuilder -> CoAxBranch
660 -> (SDoc, SrcSpan)
661 conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
662 | confEqn : _ <- conflictingEqns
663 = errorBuilder (injectivityErrorHerald False) [confEqn, tyfamEqn]
664 | otherwise
665 = panic "conflictInjInstErr"
666
667 -- | Build error message for equation with injective type variables unused in
668 -- the RHS.
669 unusedInjectiveVarsErr :: Pair TyVarSet -> InjErrorBuilder -> CoAxBranch
670 -> (SDoc, SrcSpan)
671 unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn
672 = errorBuilder (injectivityErrorHerald True $$ msg)
673 [tyfamEqn]
674 where
675 tvs = invis_vars `unionVarSet` vis_vars
676 has_types = not $ isEmptyVarSet vis_vars
677 has_kinds = not $ isEmptyVarSet invis_vars
678
679 doc = sep [ what <+> text "variable" <>
680 pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . toposortTyVars)
681 , text "cannot be inferred from the right-hand side." ]
682 what = case (has_types, has_kinds) of
683 (True, True) -> text "Type and kind"
684 (True, False) -> text "Type"
685 (False, True) -> text "Kind"
686 (False, False) -> pprPanic "mkUnusedInjectiveVarsErr" $ ppr tvs
687 print_kinds_info = ppWhen has_kinds ppSuggestExplicitKinds
688 msg = doc $$ print_kinds_info $$
689 text "In the type family equation:"
690
691 -- | Build error message for equation that has a type family call at the top
692 -- level of RHS
693 tfHeadedErr :: InjErrorBuilder -> CoAxBranch
694 -> (SDoc, SrcSpan)
695 tfHeadedErr errorBuilder famInst
696 = errorBuilder (injectivityErrorHerald True $$
697 text "RHS of injective type family equation cannot" <+>
698 text "be a type family:") [famInst]
699
700 -- | Build error message for equation that has a bare type variable in the RHS
701 -- but LHS pattern is not a bare type variable.
702 bareVariableInRHSErr :: [Type] -> InjErrorBuilder -> CoAxBranch
703 -> (SDoc, SrcSpan)
704 bareVariableInRHSErr tys errorBuilder famInst
705 = errorBuilder (injectivityErrorHerald True $$
706 text "RHS of injective type family equation is a bare" <+>
707 text "type variable" $$
708 text "but these LHS type and kind patterns are not bare" <+>
709 text "variables:" <+> pprQuotedList tys) [famInst]
710
711
712 makeFamInstsErr :: SDoc -> [FamInst] -> (SDoc, SrcSpan)
713 makeFamInstsErr herald insts
714 = ASSERT( not (null insts) )
715 ( hang herald
716 2 (vcat [ pprCoAxBranchHdr (famInstAxiom fi) 0
717 | fi <- sorted ])
718 , srcSpan )
719 where
720 getSpan = getSrcLoc . famInstAxiom
721 sorted = sortWith getSpan insts
722 fi1 = head sorted
723 srcSpan = coAxBranchSpan (coAxiomSingleBranch (famInstAxiom fi1))
724 -- The sortWith just arranges that instances are dislayed in order
725 -- of source location, which reduced wobbling in error messages,
726 -- and is better for users
727
728 tcGetFamInstEnvs :: TcM FamInstEnvs
729 -- Gets both the external-package inst-env
730 -- and the home-pkg inst env (includes module being compiled)
731 tcGetFamInstEnvs
732 = do { eps <- getEps; env <- getGblEnv
733 ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }