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