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