Revert "Make globals use sharedCAF"
[ghc.git] / compiler / types / FamInstEnv.hs
1 -- (c) The University of Glasgow 2006
2 --
3 -- FamInstEnv: Type checked family instance declarations
4
5 {-# LANGUAGE CPP, GADTs, ScopedTypeVariables #-}
6
7 module FamInstEnv (
8 FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
9 famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
10 pprFamInst, pprFamInsts,
11 mkImportedFamInst,
12
13 FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
14 extendFamInstEnv, deleteFromFamInstEnv, extendFamInstEnvList,
15 identicalFamInstHead, famInstEnvElts, familyInstances,
16
17 -- * CoAxioms
18 mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
19 mkNewTypeCoAxiom,
20
21 FamInstMatch(..),
22 lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
23
24 isDominatedBy, apartnessCheck,
25
26 -- Injectivity
27 InjectivityCheckResult(..),
28 lookupFamInstEnvInjectivityConflicts, injectiveBranches,
29
30 -- Normalisation
31 topNormaliseType, topNormaliseType_maybe,
32 normaliseType, normaliseTcApp,
33 reduceTyFamApp_maybe,
34
35 -- Flattening
36 flattenTys
37 ) where
38
39 #include "HsVersions.h"
40
41 import Unify
42 import Type
43 import TyCoRep
44 import TyCon
45 import Coercion
46 import CoAxiom
47 import VarSet
48 import VarEnv
49 import Name
50 import PrelNames ( eqPrimTyConKey )
51 import UniqDFM
52 import Outputable
53 import Maybes
54 import TrieMap
55 import Unique
56 import Util
57 import Var
58 import Pair
59 import SrcLoc
60 import FastString
61 import MonadUtils
62 import Control.Monad
63 import Data.Function ( on )
64 import Data.List( mapAccumL )
65
66 {-
67 ************************************************************************
68 * *
69 Type checked family instance heads
70 * *
71 ************************************************************************
72
73 Note [FamInsts and CoAxioms]
74 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
75 * CoAxioms and FamInsts are just like
76 DFunIds and ClsInsts
77
78 * A CoAxiom is a System-FC thing: it can relate any two types
79
80 * A FamInst is a Haskell source-language thing, corresponding
81 to a type/data family instance declaration.
82 - The FamInst contains a CoAxiom, which is the evidence
83 for the instance
84
85 - The LHS of the CoAxiom is always of form F ty1 .. tyn
86 where F is a type family
87 -}
88
89 data FamInst -- See Note [FamInsts and CoAxioms]
90 = FamInst { fi_axiom :: CoAxiom Unbranched -- The new coercion axiom
91 -- introduced by this family
92 -- instance
93 -- INVARIANT: apart from freshening (see below)
94 -- fi_tvs = cab_tvs of the (single) axiom branch
95 -- fi_cvs = cab_cvs ...ditto...
96 -- fi_tys = cab_lhs ...ditto...
97 -- fi_rhs = cab_rhs ...ditto...
98
99 , fi_flavor :: FamFlavor
100
101 -- Everything below here is a redundant,
102 -- cached version of the two things above
103 -- except that the TyVars are freshened
104 , fi_fam :: Name -- Family name
105
106 -- Used for "rough matching"; same idea as for class instances
107 -- See Note [Rough-match field] in InstEnv
108 , fi_tcs :: [Maybe Name] -- Top of type args
109 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
110
111 -- Used for "proper matching"; ditto
112 , fi_tvs :: [TyVar] -- Template tyvars for full match
113 , fi_cvs :: [CoVar] -- Template covars for full match
114 -- Like ClsInsts, these variables are always fresh
115 -- See Note [Template tyvars are fresh] in InstEnv
116
117 , fi_tys :: [Type] -- The LHS type patterns
118 -- May be eta-reduced; see Note [Eta reduction for data families]
119
120 , fi_rhs :: Type -- the RHS, with its freshened vars
121 }
122
123 data FamFlavor
124 = SynFamilyInst -- A synonym family
125 | DataFamilyInst TyCon -- A data family, with its representation TyCon
126
127 {- Note [Eta reduction for data families]
128 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
129 Consider this
130 data family T a b :: *
131 newtype instance T Int a = MkT (IO a) deriving( Monad )
132 We'd like this to work.
133
134 From the 'newtype instance' you might think we'd get:
135 newtype TInt a = MkT (IO a)
136 axiom ax1 a :: T Int a ~ TInt a -- The newtype-instance part
137 axiom ax2 a :: TInt a ~ IO a -- The newtype part
138
139 But now what can we do? We have this problem
140 Given: d :: Monad IO
141 Wanted: d' :: Monad (T Int) = d |> ????
142 What coercion can we use for the ???
143
144 Solution: eta-reduce both axioms, thus:
145 axiom ax1 :: T Int ~ TInt
146 axiom ax2 :: TInt ~ IO
147 Now
148 d' = d |> Monad (sym (ax2 ; ax1))
149
150 This eta reduction happens for data instances as well as newtype
151 instances. Here we want to eta-reduce the data family axiom.
152 All this is done in TcInstDcls.tcDataFamInstDecl.
153
154 See also Note [Newtype eta] in TyCon.
155
156 Bottom line:
157 For a FamInst with fi_flavour = DataFamilyInst rep_tc,
158 - fi_tvs may be shorter than tyConTyVars of rep_tc
159 - fi_tys may be shorter than tyConArity of the family tycon
160 i.e. LHS is unsaturated
161 - fi_rhs will be (rep_tc fi_tvs)
162 i.e. RHS is un-saturated
163
164 But when fi_flavour = SynFamilyInst,
165 - fi_tys has the exact arity of the family tycon
166 -}
167
168 -- Obtain the axiom of a family instance
169 famInstAxiom :: FamInst -> CoAxiom Unbranched
170 famInstAxiom = fi_axiom
171
172 -- Split the left-hand side of the FamInst
173 famInstSplitLHS :: FamInst -> (TyCon, [Type])
174 famInstSplitLHS (FamInst { fi_axiom = axiom, fi_tys = lhs })
175 = (coAxiomTyCon axiom, lhs)
176
177 -- Get the RHS of the FamInst
178 famInstRHS :: FamInst -> Type
179 famInstRHS = fi_rhs
180
181 -- Get the family TyCon of the FamInst
182 famInstTyCon :: FamInst -> TyCon
183 famInstTyCon = coAxiomTyCon . famInstAxiom
184
185 -- Return the representation TyCons introduced by data family instances, if any
186 famInstsRepTyCons :: [FamInst] -> [TyCon]
187 famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis]
188
189 -- Extracts the TyCon for this *data* (or newtype) instance
190 famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
191 famInstRepTyCon_maybe fi
192 = case fi_flavor fi of
193 DataFamilyInst tycon -> Just tycon
194 SynFamilyInst -> Nothing
195
196 dataFamInstRepTyCon :: FamInst -> TyCon
197 dataFamInstRepTyCon fi
198 = case fi_flavor fi of
199 DataFamilyInst tycon -> tycon
200 SynFamilyInst -> pprPanic "dataFamInstRepTyCon" (ppr fi)
201
202 {-
203 ************************************************************************
204 * *
205 Pretty printing
206 * *
207 ************************************************************************
208 -}
209
210 instance NamedThing FamInst where
211 getName = coAxiomName . fi_axiom
212
213 instance Outputable FamInst where
214 ppr = pprFamInst
215
216 -- Prints the FamInst as a family instance declaration
217 -- NB: FamInstEnv.pprFamInst is used only for internal, debug printing
218 -- See pprTyThing.pprFamInst for printing for the user
219 pprFamInst :: FamInst -> SDoc
220 pprFamInst famInst
221 = hang (pprFamInstHdr famInst) 2 (ifPprDebug debug_stuff)
222 where
223 ax = fi_axiom famInst
224 debug_stuff = vcat [ text "Coercion axiom:" <+> ppr ax
225 , text "Tvs:" <+> ppr (fi_tvs famInst)
226 , text "LHS:" <+> ppr (fi_tys famInst)
227 , text "RHS:" <+> ppr (fi_rhs famInst) ]
228
229 pprFamInstHdr :: FamInst -> SDoc
230 pprFamInstHdr fi@(FamInst {fi_flavor = flavor})
231 = pprTyConSort <+> pp_instance <+> pp_head
232 where
233 -- For *associated* types, say "type T Int = blah"
234 -- For *top level* type instances, say "type instance T Int = blah"
235 pp_instance
236 | isTyConAssoc fam_tc = empty
237 | otherwise = text "instance"
238
239 (fam_tc, etad_lhs_tys) = famInstSplitLHS fi
240 vanilla_pp_head = pprTypeApp fam_tc etad_lhs_tys
241
242 pp_head | DataFamilyInst rep_tc <- flavor
243 , isAlgTyCon rep_tc
244 , let extra_tvs = dropList etad_lhs_tys (tyConTyVars rep_tc)
245 , not (null extra_tvs)
246 = getPprStyle $ \ sty ->
247 if debugStyle sty
248 then vanilla_pp_head -- With -dppr-debug just show it as-is
249 else pprTypeApp fam_tc (etad_lhs_tys ++ mkTyVarTys extra_tvs)
250 -- Without -dppr-debug, eta-expand
251 -- See Trac #8674
252 -- (This is probably over the top now that we use this
253 -- only for internal debug printing; PprTyThing.pprFamInst
254 -- is used for user-level printing.)
255 | otherwise
256 = vanilla_pp_head
257
258 pprTyConSort = case flavor of
259 SynFamilyInst -> text "type"
260 DataFamilyInst tycon
261 | isDataTyCon tycon -> text "data"
262 | isNewTyCon tycon -> text "newtype"
263 | isAbstractTyCon tycon -> text "data"
264 | otherwise -> text "WEIRD" <+> ppr tycon
265
266 pprFamInsts :: [FamInst] -> SDoc
267 pprFamInsts finsts = vcat (map pprFamInst finsts)
268
269 {-
270 Note [Lazy axiom match]
271 ~~~~~~~~~~~~~~~~~~~~~~~
272 It is Vitally Important that mkImportedFamInst is *lazy* in its axiom
273 parameter. The axiom is loaded lazily, via a forkM, in TcIface. Sometime
274 later, mkImportedFamInst is called using that axiom. However, the axiom
275 may itself depend on entities which are not yet loaded as of the time
276 of the mkImportedFamInst. Thus, if mkImportedFamInst eagerly looks at the
277 axiom, a dependency loop spontaneously appears and GHC hangs. The solution
278 is simply for mkImportedFamInst never, ever to look inside of the axiom
279 until everything else is good and ready to do so. We can assume that this
280 readiness has been achieved when some other code pulls on the axiom in the
281 FamInst. Thus, we pattern match on the axiom lazily (in the where clause,
282 not in the parameter list) and we assert the consistency of names there
283 also.
284 -}
285
286 -- Make a family instance representation from the information found in an
287 -- interface file. In particular, we get the rough match info from the iface
288 -- (instead of computing it here).
289 mkImportedFamInst :: Name -- Name of the family
290 -> [Maybe Name] -- Rough match info
291 -> CoAxiom Unbranched -- Axiom introduced
292 -> FamInst -- Resulting family instance
293 mkImportedFamInst fam mb_tcs axiom
294 = FamInst {
295 fi_fam = fam,
296 fi_tcs = mb_tcs,
297 fi_tvs = tvs,
298 fi_cvs = cvs,
299 fi_tys = tys,
300 fi_rhs = rhs,
301 fi_axiom = axiom,
302 fi_flavor = flavor }
303 where
304 -- See Note [Lazy axiom match]
305 ~(CoAxBranch { cab_lhs = tys
306 , cab_tvs = tvs
307 , cab_cvs = cvs
308 , cab_rhs = rhs }) = coAxiomSingleBranch axiom
309
310 -- Derive the flavor for an imported FamInst rather disgustingly
311 -- Maybe we should store it in the IfaceFamInst?
312 flavor = case splitTyConApp_maybe rhs of
313 Just (tc, _)
314 | Just ax' <- tyConFamilyCoercion_maybe tc
315 , ax' == axiom
316 -> DataFamilyInst tc
317 _ -> SynFamilyInst
318
319 {-
320 ************************************************************************
321 * *
322 FamInstEnv
323 * *
324 ************************************************************************
325
326 Note [FamInstEnv]
327 ~~~~~~~~~~~~~~~~~
328 A FamInstEnv maps a family name to the list of known instances for that family.
329
330 The same FamInstEnv includes both 'data family' and 'type family' instances.
331 Type families are reduced during type inference, but not data families;
332 the user explains when to use a data family instance by using constructors
333 and pattern matching.
334
335 Nevertheless it is still useful to have data families in the FamInstEnv:
336
337 - For finding overlaps and conflicts
338
339 - For finding the representation type...see FamInstEnv.topNormaliseType
340 and its call site in Simplify
341
342 - In standalone deriving instance Eq (T [Int]) we need to find the
343 representation type for T [Int]
344
345 Note [Varying number of patterns for data family axioms]
346 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
347 For data families, the number of patterns may vary between instances.
348 For example
349 data family T a b
350 data instance T Int a = T1 a | T2
351 data instance T Bool [a] = T3 a
352
353 Then we get a data type for each instance, and an axiom:
354 data TInt a = T1 a | T2
355 data TBoolList a = T3 a
356
357 axiom ax7 :: T Int ~ TInt -- Eta-reduced
358 axiom ax8 a :: T Bool [a] ~ TBoolList a
359
360 These two axioms for T, one with one pattern, one with two;
361 see Note [Eta reduction for data families]
362
363 Note [FamInstEnv determinism]
364 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
365 We turn FamInstEnvs into a list in some places that don't directly affect
366 the ABI. That happens in family consistency checks and when producing output
367 for `:info`. Unfortunately that nondeterminism is nonlocal and it's hard
368 to tell what it affects without following a chain of functions. It's also
369 easy to accidentally make that nondeterminism affect the ABI. Furthermore
370 the envs should be relatively small, so it should be free to use deterministic
371 maps here. Testing with nofib and validate detected no difference between
372 UniqFM and UniqDFM.
373 See Note [Deterministic UniqFM].
374 -}
375
376 type FamInstEnv = UniqDFM FamilyInstEnv -- Maps a family to its instances
377 -- See Note [FamInstEnv]
378 -- See Note [FamInstEnv determinism]
379
380 type FamInstEnvs = (FamInstEnv, FamInstEnv)
381 -- External package inst-env, Home-package inst-env
382
383 newtype FamilyInstEnv
384 = FamIE [FamInst] -- The instances for a particular family, in any order
385
386 instance Outputable FamilyInstEnv where
387 ppr (FamIE fs) = text "FamIE" <+> vcat (map ppr fs)
388
389 -- INVARIANTS:
390 -- * The fs_tvs are distinct in each FamInst
391 -- of a range value of the map (so we can safely unify them)
392
393 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
394 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
395
396 emptyFamInstEnv :: FamInstEnv
397 emptyFamInstEnv = emptyUDFM
398
399 famInstEnvElts :: FamInstEnv -> [FamInst]
400 famInstEnvElts fi = [elt | FamIE elts <- eltsUDFM fi, elt <- elts]
401 -- See Note [FamInstEnv determinism]
402
403 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
404 familyInstances (pkg_fie, home_fie) fam
405 = get home_fie ++ get pkg_fie
406 where
407 get env = case lookupUDFM env fam of
408 Just (FamIE insts) -> insts
409 Nothing -> []
410
411 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
412 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
413
414 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
415 extendFamInstEnv inst_env
416 ins_item@(FamInst {fi_fam = cls_nm})
417 = addToUDFM_C add inst_env cls_nm (FamIE [ins_item])
418 where
419 add (FamIE items) _ = FamIE (ins_item:items)
420
421 deleteFromFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
422 -- Used only for overriding in GHCi
423 deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm})
424 = adjustUDFM adjust inst_env fam_nm
425 where
426 adjust :: FamilyInstEnv -> FamilyInstEnv
427 adjust (FamIE items)
428 = FamIE (filterOut (identicalFamInstHead fam_inst) items)
429
430 identicalFamInstHead :: FamInst -> FamInst -> Bool
431 -- ^ True when the LHSs are identical
432 -- Used for overriding in GHCi
433 identicalFamInstHead (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
434 = coAxiomTyCon ax1 == coAxiomTyCon ax2
435 && numBranches brs1 == numBranches brs2
436 && and ((zipWith identical_branch `on` fromBranches) brs1 brs2)
437 where
438 brs1 = coAxiomBranches ax1
439 brs2 = coAxiomBranches ax2
440
441 identical_branch br1 br2
442 = isJust (tcMatchTys lhs1 lhs2)
443 && isJust (tcMatchTys lhs2 lhs1)
444 where
445 lhs1 = coAxBranchLHS br1
446 lhs2 = coAxBranchLHS br2
447
448 {-
449 ************************************************************************
450 * *
451 Compatibility
452 * *
453 ************************************************************************
454
455 Note [Apartness]
456 ~~~~~~~~~~~~~~~~
457 In dealing with closed type families, we must be able to check that one type
458 will never reduce to another. This check is called /apartness/. The check
459 is always between a target (which may be an arbitrary type) and a pattern.
460 Here is how we do it:
461
462 apart(target, pattern) = not (unify(flatten(target), pattern))
463
464 where flatten (implemented in flattenTys, below) converts all type-family
465 applications into fresh variables. (See Note [Flattening].)
466
467 Note [Compatibility]
468 ~~~~~~~~~~~~~~~~~~~~
469 Two patterns are /compatible/ if either of the following conditions hold:
470 1) The patterns are apart.
471 2) The patterns unify with a substitution S, and their right hand sides
472 equal under that substitution.
473
474 For open type families, only compatible instances are allowed. For closed
475 type families, the story is slightly more complicated. Consider the following:
476
477 type family F a where
478 F Int = Bool
479 F a = Int
480
481 g :: Show a => a -> F a
482 g x = length (show x)
483
484 Should that type-check? No. We need to allow for the possibility that 'a'
485 might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
486 only when we can be sure that 'a' is not Int.
487
488 To achieve this, after finding a possible match within the equations, we have to
489 go back to all previous equations and check that, under the
490 substitution induced by the match, other branches are surely apart. (See
491 Note [Apartness].) This is similar to what happens with class
492 instance selection, when we need to guarantee that there is only a match and
493 no unifiers. The exact algorithm is different here because the the
494 potentially-overlapping group is closed.
495
496 As another example, consider this:
497
498 type family G x where
499 G Int = Bool
500 G a = Double
501
502 type family H y
503 -- no instances
504
505 Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
506 simplify to be Int. So, (G (H Char)) is stuck, for now.
507
508 While everything above is quite sound, it isn't as expressive as we'd like.
509 Consider this:
510
511 type family J a where
512 J Int = Int
513 J a = a
514
515 Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
516 b is instantiated with Int, but the RHSs coincide there, so it's all OK.
517
518 So, the rule is this: when looking up a branch in a closed type family, we
519 find a branch that matches the target, but then we make sure that the target
520 is apart from every previous *incompatible* branch. We don't check the
521 branches that are compatible with the matching branch, because they are either
522 irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
523 -}
524
525 -- See Note [Compatibility]
526 compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
527 compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
528 (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
529 = case tcUnifyTysFG (const BindMe) lhs1 lhs2 of
530 SurelyApart -> True
531 Unifiable subst
532 | Type.substTyAddInScope subst rhs1 `eqType`
533 Type.substTyAddInScope subst rhs2
534 -> True
535 _ -> False
536
537 -- | Result of testing two type family equations for injectiviy.
538 data InjectivityCheckResult
539 = InjectivityAccepted
540 -- ^ Either RHSs are distinct or unification of RHSs leads to unification of
541 -- LHSs
542 | InjectivityUnified CoAxBranch CoAxBranch
543 -- ^ RHSs unify but LHSs don't unify under that substitution. Relevant for
544 -- closed type families where equation after unification might be
545 -- overlpapped (in which case it is OK if they don't unify). Constructor
546 -- stores axioms after unification.
547
548 -- | Check whether two type family axioms don't violate injectivity annotation.
549 injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch
550 -> InjectivityCheckResult
551 injectiveBranches injectivity
552 ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
553 ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
554 -- See Note [Verifying injectivity annotation]. This function implements first
555 -- check described there.
556 = let getInjArgs = filterByList injectivity
557 in case tcUnifyTyWithTFs True rhs1 rhs2 of -- True = two-way pre-unification
558 Nothing -> InjectivityAccepted -- RHS are different, so equations are
559 -- injective.
560 Just subst -> -- RHS unify under a substitution
561 let lhs1Subst = Type.substTys subst (getInjArgs lhs1)
562 lhs2Subst = Type.substTys subst (getInjArgs lhs2)
563 -- If LHSs are equal under the substitution used for RHSs then this pair
564 -- of equations does not violate injectivity annotation. If LHSs are not
565 -- equal under that substitution then this pair of equations violates
566 -- injectivity annotation, but for closed type families it still might
567 -- be the case that one LHS after substitution is unreachable.
568 in if eqTypes lhs1Subst lhs2Subst
569 then InjectivityAccepted
570 else InjectivityUnified ( ax1 { cab_lhs = Type.substTys subst lhs1
571 , cab_rhs = Type.substTy subst rhs1 })
572 ( ax2 { cab_lhs = Type.substTys subst lhs2
573 , cab_rhs = Type.substTy subst rhs2 })
574
575 -- takes a CoAxiom with unknown branch incompatibilities and computes
576 -- the compatibilities
577 -- See Note [Storing compatibility] in CoAxiom
578 computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
579 computeAxiomIncomps branches
580 = snd (mapAccumL go [] branches)
581 where
582 go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
583 go prev_brs cur_br
584 = (cur_br : prev_brs, new_br)
585 where
586 new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
587
588 mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
589 mk_incomps prev_brs cur_br
590 = filter (not . compatibleBranches cur_br) prev_brs
591
592 {-
593 ************************************************************************
594 * *
595 Constructing axioms
596 These functions are here because tidyType / tcUnifyTysFG
597 are not available in CoAxiom
598
599 Also computeAxiomIncomps is too sophisticated for CoAxiom
600 * *
601 ************************************************************************
602
603 Note [Tidy axioms when we build them]
604 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
605 We print out axioms and don't want to print stuff like
606 F k k a b = ...
607 Instead we must tidy those kind variables. See Trac #7524.
608 -}
609
610 -- all axiom roles are Nominal, as this is only used with type families
611 mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
612 -> [CoVar] -- possibly stale covars
613 -> [Type] -- LHS patterns
614 -> Type -- RHS
615 -> [Role]
616 -> SrcSpan
617 -> CoAxBranch
618 mkCoAxBranch tvs cvs lhs rhs roles loc
619 = CoAxBranch { cab_tvs = tvs1
620 , cab_cvs = cvs1
621 , cab_lhs = tidyTypes env lhs
622 , cab_roles = roles
623 , cab_rhs = tidyType env rhs
624 , cab_loc = loc
625 , cab_incomps = placeHolderIncomps }
626 where
627 (env1, tvs1) = tidyTyCoVarBndrs emptyTidyEnv tvs
628 (env, cvs1) = tidyTyCoVarBndrs env1 cvs
629 -- See Note [Tidy axioms when we build them]
630
631 -- all of the following code is here to avoid mutual dependencies with
632 -- Coercion
633 mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
634 mkBranchedCoAxiom ax_name fam_tc branches
635 = CoAxiom { co_ax_unique = nameUnique ax_name
636 , co_ax_name = ax_name
637 , co_ax_tc = fam_tc
638 , co_ax_role = Nominal
639 , co_ax_implicit = False
640 , co_ax_branches = manyBranches (computeAxiomIncomps branches) }
641
642 mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
643 mkUnbranchedCoAxiom ax_name fam_tc branch
644 = CoAxiom { co_ax_unique = nameUnique ax_name
645 , co_ax_name = ax_name
646 , co_ax_tc = fam_tc
647 , co_ax_role = Nominal
648 , co_ax_implicit = False
649 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
650
651 mkSingleCoAxiom :: Role -> Name
652 -> [TyVar] -> [CoVar] -> TyCon -> [Type] -> Type
653 -> CoAxiom Unbranched
654 -- Make a single-branch CoAxiom, incluidng making the branch itself
655 -- Used for both type family (Nominal) and data family (Representational)
656 -- axioms, hence passing in the Role
657 mkSingleCoAxiom role ax_name tvs cvs fam_tc lhs_tys rhs_ty
658 = CoAxiom { co_ax_unique = nameUnique ax_name
659 , co_ax_name = ax_name
660 , co_ax_tc = fam_tc
661 , co_ax_role = role
662 , co_ax_implicit = False
663 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
664 where
665 branch = mkCoAxBranch tvs cvs lhs_tys rhs_ty
666 (map (const Nominal) tvs)
667 (getSrcSpan ax_name)
668
669 -- | Create a coercion constructor (axiom) suitable for the given
670 -- newtype 'TyCon'. The 'Name' should be that of a new coercion
671 -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
672 -- the type the appropriate right hand side of the @newtype@, with
673 -- the free variables a subset of those 'TyVar's.
674 mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
675 mkNewTypeCoAxiom name tycon tvs roles rhs_ty
676 = CoAxiom { co_ax_unique = nameUnique name
677 , co_ax_name = name
678 , co_ax_implicit = True -- See Note [Implicit axioms] in TyCon
679 , co_ax_role = Representational
680 , co_ax_tc = tycon
681 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
682 where
683 branch = mkCoAxBranch tvs [] (mkTyVarTys tvs) rhs_ty
684 roles (getSrcSpan name)
685
686 {-
687 ************************************************************************
688 * *
689 Looking up a family instance
690 * *
691 ************************************************************************
692
693 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
694 Multiple matches are only possible in case of type families (not data
695 families), and then, it doesn't matter which match we choose (as the
696 instances are guaranteed confluent).
697
698 We return the matching family instances and the type instance at which it
699 matches. For example, if we lookup 'T [Int]' and have a family instance
700
701 data instance T [a] = ..
702
703 desugared to
704
705 data :R42T a = ..
706 coe :Co:R42T a :: T [a] ~ :R42T a
707
708 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
709 -}
710
711 -- when matching a type family application, we get a FamInst,
712 -- and the list of types the axiom should be applied to
713 data FamInstMatch = FamInstMatch { fim_instance :: FamInst
714 , fim_tys :: [Type]
715 , fim_cos :: [Coercion]
716 }
717 -- See Note [Over-saturated matches]
718
719 instance Outputable FamInstMatch where
720 ppr (FamInstMatch { fim_instance = inst
721 , fim_tys = tys
722 , fim_cos = cos })
723 = text "match with" <+> parens (ppr inst) <+> ppr tys <+> ppr cos
724
725 lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
726 lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc
727 = get pkg_ie ++ get home_ie
728 where
729 get ie = case lookupUDFM ie fam_tc of
730 Nothing -> []
731 Just (FamIE fis) -> fis
732
733 lookupFamInstEnv
734 :: FamInstEnvs
735 -> TyCon -> [Type] -- What we are looking for
736 -> [FamInstMatch] -- Successful matches
737 -- Precondition: the tycon is saturated (or over-saturated)
738
739 lookupFamInstEnv
740 = lookup_fam_inst_env match
741 where
742 match _ _ tpl_tys tys = tcMatchTys tpl_tys tys
743
744 lookupFamInstEnvConflicts
745 :: FamInstEnvs
746 -> FamInst -- Putative new instance
747 -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field)
748 -- E.g. when we are about to add
749 -- f : type instance F [a] = a->a
750 -- we do (lookupFamInstConflicts f [b])
751 -- to find conflicting matches
752 --
753 -- Precondition: the tycon is saturated (or over-saturated)
754
755 lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
756 = lookup_fam_inst_env my_unify envs fam tys
757 where
758 (fam, tys) = famInstSplitLHS fam_inst
759 -- In example above, fam tys' = F [b]
760
761 my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
762 = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs,
763 (ppr fam <+> ppr tys) $$
764 (ppr tpl_tvs <+> ppr tpl_tys) )
765 -- Unification will break badly if the variables overlap
766 -- They shouldn't because we allocate separate uniques for them
767 if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
768 then Nothing
769 else Just noSubst
770 -- Note [Family instance overlap conflicts]
771
772 noSubst = panic "lookupFamInstEnvConflicts noSubst"
773 new_branch = coAxiomSingleBranch new_axiom
774
775 --------------------------------------------------------------------------------
776 -- Type family injectivity checking bits --
777 --------------------------------------------------------------------------------
778
779 {- Note [Verifying injectivity annotation]
780 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
781
782 Injectivity means that the RHS of a type family uniquely determines the LHS (see
783 Note [Type inference for type families with injectivity]). User informs about
784 injectivity using an injectivity annotation and it is GHC's task to verify that
785 that annotation is correct wrt. to type family equations. Whenever we see a new
786 equation of a type family we need to make sure that adding this equation to
787 already known equations of a type family does not violate injectivity annotation
788 supplied by the user (see Note [Injectivity annotation]). Of course if the type
789 family has no injectivity annotation then no check is required. But if a type
790 family has injectivity annotation we need to make sure that the following
791 conditions hold:
792
793 1. For each pair of *different* equations of a type family, one of the following
794 conditions holds:
795
796 A: RHSs are different.
797
798 B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution
799 then it must be possible to unify the LHSs under the same substitution.
800 Example:
801
802 type family FunnyId a = r | r -> a
803 type instance FunnyId Int = Int
804 type instance FunnyId a = a
805
806 RHSs of these two equations unify under [ a |-> Int ] substitution.
807 Under this substitution LHSs are equal therefore these equations don't
808 violate injectivity annotation.
809
810 B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some
811 substitution then either the LHSs unify under the same substitution or
812 the LHS of the latter equation is overlapped by earlier equations.
813 Example 1:
814
815 type family SwapIntChar a = r | r -> a where
816 SwapIntChar Int = Char
817 SwapIntChar Char = Int
818 SwapIntChar a = a
819
820 Say we are checking the last two equations. RHSs unify under [ a |->
821 Int ] substitution but LHSs don't. So we apply the substitution to LHS
822 of last equation and check whether it is overlapped by any of previous
823 equations. Since it is overlapped by the first equation we conclude
824 that pair of last two equations does not violate injectivity
825 annotation.
826
827 A special case of B is when RHSs unify with an empty substitution ie. they
828 are identical.
829
830 If any of the above two conditions holds we conclude that the pair of
831 equations does not violate injectivity annotation. But if we find a pair
832 of equations where neither of the above holds we report that this pair
833 violates injectivity annotation because for a given RHS we don't have a
834 unique LHS. (Note that (B) actually implies (A).)
835
836 Note that we only take into account these LHS patterns that were declared
837 as injective.
838
839 2. If a RHS of a type family equation is a bare type variable then
840 all LHS variables (including implicit kind variables) also have to be bare.
841 In other words, this has to be a sole equation of that type family and it has
842 to cover all possible patterns. So for example this definition will be
843 rejected:
844
845 type family W1 a = r | r -> a
846 type instance W1 [a] = a
847
848 If it were accepted we could call `W1 [W1 Int]`, which would reduce to
849 `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`,
850 which is bogus.
851
852 3. If a RHS of a type family equation is a type family application then the type
853 family is rejected as not injective.
854
855 4. If a LHS type variable that is declared as injective is not mentioned on
856 injective position in the RHS then the type family is rejected as not
857 injective. "Injective position" means either an argument to a type
858 constructor or argument to a type family on injective position.
859
860 See also Note [Injective type families] in TyCon
861 -}
862
863
864 -- | Check whether an open type family equation can be added to already existing
865 -- instance environment without causing conflicts with supplied injectivity
866 -- annotations. Returns list of conflicting axioms (type instance
867 -- declarations).
868 lookupFamInstEnvInjectivityConflicts
869 :: [Bool] -- injectivity annotation for this type family instance
870 -- INVARIANT: list contains at least one True value
871 -> FamInstEnvs -- all type instances seens so far
872 -> FamInst -- new type instance that we're checking
873 -> [CoAxBranch] -- conflicting instance delcarations
874 lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie)
875 fam_inst@(FamInst { fi_axiom = new_axiom })
876 -- See Note [Verifying injectivity annotation]. This function implements
877 -- check (1.B1) for open type families described there.
878 = lookup_inj_fam_conflicts home_ie ++ lookup_inj_fam_conflicts pkg_ie
879 where
880 fam = famInstTyCon fam_inst
881 new_branch = coAxiomSingleBranch new_axiom
882
883 -- filtering function used by `lookup_inj_fam_conflicts` to check whether
884 -- a pair of equations conflicts with the injectivity annotation.
885 isInjConflict (FamInst { fi_axiom = old_axiom })
886 | InjectivityAccepted <-
887 injectiveBranches injList (coAxiomSingleBranch old_axiom) new_branch
888 = False -- no conflict
889 | otherwise = True
890
891 lookup_inj_fam_conflicts ie
892 | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUDFM ie fam
893 = map (coAxiomSingleBranch . fi_axiom) $
894 filter isInjConflict insts
895 | otherwise = []
896
897
898 --------------------------------------------------------------------------------
899 -- Type family overlap checking bits --
900 --------------------------------------------------------------------------------
901
902 {-
903 Note [Family instance overlap conflicts]
904 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
905 - In the case of data family instances, any overlap is fundamentally a
906 conflict (as these instances imply injective type mappings).
907
908 - In the case of type family instances, overlap is admitted as long as
909 the right-hand sides of the overlapping rules coincide under the
910 overlap substitution. eg
911 type instance F a Int = a
912 type instance F Int b = b
913 These two overlap on (F Int Int) but then both RHSs are Int,
914 so all is well. We require that they are syntactically equal;
915 anything else would be difficult to test for at this stage.
916 -}
917
918 ------------------------------------------------------------
919 -- Might be a one-way match or a unifier
920 type MatchFun = FamInst -- The FamInst template
921 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
922 -> [Type] -- Target to match against
923 -> Maybe TCvSubst
924
925 lookup_fam_inst_env' -- The worker, local to this module
926 :: MatchFun
927 -> FamInstEnv
928 -> TyCon -> [Type] -- What we are looking for
929 -> [FamInstMatch]
930 lookup_fam_inst_env' match_fun ie fam match_tys
931 | isOpenFamilyTyCon fam
932 , Just (FamIE insts) <- lookupUDFM ie fam
933 = find insts -- The common case
934 | otherwise = []
935 where
936
937 find [] = []
938 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs
939 , fi_tys = tpl_tys }) : rest)
940 -- Fast check for no match, uses the "rough match" fields
941 | instanceCantMatch rough_tcs mb_tcs
942 = find rest
943
944 -- Proper check
945 | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
946 = (FamInstMatch { fim_instance = item
947 , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2
948 , fim_cos = ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
949 substCoVars subst tpl_cvs
950 })
951 : find rest
952
953 -- No match => try next
954 | otherwise
955 = find rest
956
957 where
958 (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
959
960 -- Precondition: the tycon is saturated (or over-saturated)
961
962 -- Deal with over-saturation
963 -- See Note [Over-saturated matches]
964 split_tys tpl_tys
965 | isTypeFamilyTyCon fam
966 = pre_rough_split_tys
967
968 | otherwise
969 = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
970 rough_tcs = roughMatchTcs match_tys1
971 in (rough_tcs, match_tys1, match_tys2)
972
973 (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
974 pre_rough_split_tys
975 = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
976
977 lookup_fam_inst_env -- The worker, local to this module
978 :: MatchFun
979 -> FamInstEnvs
980 -> TyCon -> [Type] -- What we are looking for
981 -> [FamInstMatch] -- Successful matches
982
983 -- Precondition: the tycon is saturated (or over-saturated)
984
985 lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
986 = lookup_fam_inst_env' match_fun home_ie fam tys
987 ++ lookup_fam_inst_env' match_fun pkg_ie fam tys
988
989 {-
990 Note [Over-saturated matches]
991 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
992 It's ok to look up an over-saturated type constructor. E.g.
993 type family F a :: * -> *
994 type instance F (a,b) = Either (a->b)
995
996 The type instance gives rise to a newtype TyCon (at a higher kind
997 which you can't do in Haskell!):
998 newtype FPair a b = FP (Either (a->b))
999
1000 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
1001 (FPair, [Int,Bool,Char])
1002 The "extra" type argument [Char] just stays on the end.
1003
1004 We handle data families and type families separately here:
1005
1006 * For type families, all instances of a type family must have the
1007 same arity, so we can precompute the split between the match_tys
1008 and the overflow tys. This is done in pre_rough_split_tys.
1009
1010 * For data family instances, though, we need to re-split for each
1011 instance, because the breakdown might be different for each
1012 instance. Why? Because of eta reduction; see
1013 Note [Eta reduction for data families].
1014 -}
1015
1016 -- checks if one LHS is dominated by a list of other branches
1017 -- in other words, if an application would match the first LHS, it is guaranteed
1018 -- to match at least one of the others. The RHSs are ignored.
1019 -- This algorithm is conservative:
1020 -- True -> the LHS is definitely covered by the others
1021 -- False -> no information
1022 -- It is currently (Oct 2012) used only for generating errors for
1023 -- inaccessible branches. If these errors go unreported, no harm done.
1024 -- This is defined here to avoid a dependency from CoAxiom to Unify
1025 isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
1026 isDominatedBy branch branches
1027 = or $ map match branches
1028 where
1029 lhs = coAxBranchLHS branch
1030 match (CoAxBranch { cab_lhs = tys })
1031 = isJust $ tcMatchTys tys lhs
1032
1033 {-
1034 ************************************************************************
1035 * *
1036 Choosing an axiom application
1037 * *
1038 ************************************************************************
1039
1040 The lookupFamInstEnv function does a nice job for *open* type families,
1041 but we also need to handle closed ones when normalising a type:
1042 -}
1043
1044 reduceTyFamApp_maybe :: FamInstEnvs
1045 -> Role -- Desired role of result coercion
1046 -> TyCon -> [Type]
1047 -> Maybe (Coercion, Type)
1048 -- Attempt to do a *one-step* reduction of a type-family application
1049 -- but *not* newtypes
1050 -- Works on type-synonym families always; data-families only if
1051 -- the role we seek is representational
1052 -- It does *not* normlise the type arguments first, so this may not
1053 -- go as far as you want. If you want normalised type arguments,
1054 -- use normaliseTcArgs first.
1055 --
1056 -- The TyCon can be oversaturated.
1057 -- Works on both open and closed families
1058 --
1059 -- Always returns a *homogeneous* coercion -- type family reductions are always
1060 -- homogeneous
1061 reduceTyFamApp_maybe envs role tc tys
1062 | Phantom <- role
1063 = Nothing
1064
1065 | case role of
1066 Representational -> isOpenFamilyTyCon tc
1067 _ -> isOpenTypeFamilyTyCon tc
1068 -- If we seek a representational coercion
1069 -- (e.g. the call in topNormaliseType_maybe) then we can
1070 -- unwrap data families as well as type-synonym families;
1071 -- otherwise only type-synonym families
1072 , FamInstMatch { fim_instance = FamInst { fi_axiom = ax }
1073 , fim_tys = inst_tys
1074 , fim_cos = inst_cos } : _ <- lookupFamInstEnv envs tc tys
1075 -- NB: Allow multiple matches because of compatible overlap
1076
1077 = let co = mkUnbranchedAxInstCo role ax inst_tys inst_cos
1078 ty = pSnd (coercionKind co)
1079 in Just (co, ty)
1080
1081 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
1082 , Just (ind, inst_tys, inst_cos) <- chooseBranch ax tys
1083 = let co = mkAxInstCo role ax ind inst_tys inst_cos
1084 ty = pSnd (coercionKind co)
1085 in Just (co, ty)
1086
1087 | Just ax <- isBuiltInSynFamTyCon_maybe tc
1088 , Just (coax,ts,ty) <- sfMatchFam ax tys
1089 = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
1090 in Just (co, ty)
1091
1092 | otherwise
1093 = Nothing
1094
1095 -- The axiom can be oversaturated. (Closed families only.)
1096 chooseBranch :: CoAxiom Branched -> [Type]
1097 -> Maybe (BranchIndex, [Type], [Coercion]) -- found match, with args
1098 chooseBranch axiom tys
1099 = do { let num_pats = coAxiomNumPats axiom
1100 (target_tys, extra_tys) = splitAt num_pats tys
1101 branches = coAxiomBranches axiom
1102 ; (ind, inst_tys, inst_cos)
1103 <- findBranch (fromBranches branches) target_tys
1104 ; return ( ind, inst_tys `chkAppend` extra_tys, inst_cos ) }
1105
1106 -- The axiom must *not* be oversaturated
1107 findBranch :: [CoAxBranch] -- branches to check
1108 -> [Type] -- target types
1109 -> Maybe (BranchIndex, [Type], [Coercion])
1110 -- coercions relate requested types to returned axiom LHS at role N
1111 findBranch branches target_tys
1112 = go 0 branches
1113 where
1114 go ind (branch@(CoAxBranch { cab_tvs = tpl_tvs, cab_cvs = tpl_cvs
1115 , cab_lhs = tpl_lhs
1116 , cab_incomps = incomps }) : rest)
1117 = let in_scope = mkInScopeSet (unionVarSets $
1118 map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
1119 -- See Note [Flattening] below
1120 flattened_target = flattenTys in_scope target_tys
1121 in case tcMatchTys tpl_lhs target_tys of
1122 Just subst -- matching worked. now, check for apartness.
1123 | apartnessCheck flattened_target branch
1124 -> -- matching worked & we're apart from all incompatible branches.
1125 -- success
1126 ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
1127 Just (ind, substTyVars subst tpl_tvs, substCoVars subst tpl_cvs)
1128
1129 -- failure. keep looking
1130 _ -> go (ind+1) rest
1131
1132 -- fail if no branches left
1133 go _ [] = Nothing
1134
1135 -- | Do an apartness check, as described in the "Closed Type Families" paper
1136 -- (POPL '14). This should be used when determining if an equation
1137 -- ('CoAxBranch') of a closed type family can be used to reduce a certain target
1138 -- type family application.
1139 apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure
1140 -- they're flattened! See Note [Flattening].
1141 -- (NB: This "flat" is a different
1142 -- "flat" than is used in TcFlatten.)
1143 -> CoAxBranch -- ^ the candidate equation we wish to use
1144 -- Precondition: this matches the target
1145 -> Bool -- ^ True <=> equation can fire
1146 apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps })
1147 = all (isSurelyApart
1148 . tcUnifyTysFG (const BindMe) flattened_target
1149 . coAxBranchLHS) incomps
1150 where
1151 isSurelyApart SurelyApart = True
1152 isSurelyApart _ = False
1153
1154 {-
1155 ************************************************************************
1156 * *
1157 Looking up a family instance
1158 * *
1159 ************************************************************************
1160
1161 Note [Normalising types]
1162 ~~~~~~~~~~~~~~~~~~~~~~~~
1163 The topNormaliseType function removes all occurrences of type families
1164 and newtypes from the top-level structure of a type. normaliseTcApp does
1165 the type family lookup and is fairly straightforward. normaliseType is
1166 a little more involved.
1167
1168 The complication comes from the fact that a type family might be used in the
1169 kind of a variable bound in a forall. We wish to remove this type family
1170 application, but that means coming up with a fresh variable (with the new
1171 kind). Thus, we need a substitution to be built up as we recur through the
1172 type. However, an ordinary TCvSubst just won't do: when we hit a type variable
1173 whose kind has changed during normalisation, we need both the new type
1174 variable *and* the coercion. We could conjure up a new VarEnv with just this
1175 property, but a usable substitution environment already exists:
1176 LiftingContexts from the liftCoSubst family of functions, defined in Coercion.
1177 A LiftingContext maps a type variable to a coercion and a coercion variable to
1178 a pair of coercions. Let's ignore coercion variables for now. Because the
1179 coercion a type variable maps to contains the destination type (via
1180 coercionKind), we don't need to store that destination type separately. Thus,
1181 a LiftingContext has what we need: a map from type variables to (Coercion,
1182 Type) pairs.
1183
1184 We also benefit because we can piggyback on the liftCoSubstVarBndr function to
1185 deal with binders. However, I had to modify that function to work with this
1186 application. Thus, we now have liftCoSubstVarBndrCallback, which takes
1187 a function used to process the kind of the binder. We don't wish
1188 to lift the kind, but instead normalise it. So, we pass in a callback function
1189 that processes the kind of the binder.
1190
1191 After that brilliant explanation of all this, I'm sure you've forgotten the
1192 dangling reference to coercion variables. What do we do with those? Nothing at
1193 all. The point of normalising types is to remove type family applications, but
1194 there's no sense in removing these from coercions. We would just get back a
1195 new coercion witnessing the equality between the same types as the original
1196 coercion. Because coercions are irrelevant anyway, there is no point in doing
1197 this. So, whenever we encounter a coercion, we just say that it won't change.
1198 That's what the CoercionTy case is doing within normalise_type.
1199
1200 -}
1201
1202 topNormaliseType :: FamInstEnvs -> Type -> Type
1203 topNormaliseType env ty = case topNormaliseType_maybe env ty of
1204 Just (_co, ty') -> ty'
1205 Nothing -> ty
1206
1207 topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
1208
1209 -- ^ Get rid of *outermost* (or toplevel)
1210 -- * type function redex
1211 -- * data family redex
1212 -- * newtypes
1213 -- returning an appropriate Representational coercion. Specifically, if
1214 -- topNormaliseType_maybe env ty = Maybe (co, ty')
1215 -- then
1216 -- (a) co :: ty ~R ty'
1217 -- (b) ty' is not a newtype, and is not a type-family or data-family redex
1218 --
1219 -- However, ty' can be something like (Maybe (F ty)), where
1220 -- (F ty) is a redex.
1221 --
1222 -- Its a bit like Type.repType, but handles type families too
1223
1224 topNormaliseType_maybe env ty
1225 = topNormaliseTypeX stepper mkTransCo ty
1226 where
1227 stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
1228
1229 tyFamStepper rec_nts tc tys -- Try to step a type/data familiy
1230 = let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
1231 -- NB: It's OK to use normaliseTcArgs here instead of
1232 -- normalise_tc_args (which takes the LiftingContext described
1233 -- in Note [Normalising types]) because the reduceTyFamApp below
1234 -- works only at top level. We'll never recur in this function
1235 -- after reducing the kind of a bound tyvar.
1236
1237 case reduceTyFamApp_maybe env Representational tc ntys of
1238 Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
1239 _ -> NS_Done
1240
1241 ---------------
1242 normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
1243 -- See comments on normaliseType for the arguments of this function
1244 normaliseTcApp env role tc tys
1245 = initNormM env role (tyCoVarsOfTypes tys) $
1246 normalise_tc_app tc tys
1247
1248 -- See Note [Normalising types] about the LiftingContext
1249 normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type)
1250 normalise_tc_app tc tys
1251 = do { (args_co, ntys) <- normalise_tc_args tc tys
1252 ; case expandSynTyCon_maybe tc ntys of
1253 { Just (tenv, rhs, ntys') ->
1254 do { (co2, ninst_rhs)
1255 <- normalise_type (substTy (mkTvSubstPrs tenv) rhs)
1256 ; return $
1257 if isReflCo co2
1258 then (args_co, mkTyConApp tc ntys)
1259 else (args_co `mkTransCo` co2, mkAppTys ninst_rhs ntys') }
1260 ; Nothing ->
1261 do { env <- getEnv
1262 ; role <- getRole
1263 ; case reduceTyFamApp_maybe env role tc ntys of
1264 Just (first_co, ty')
1265 -> do { (rest_co,nty) <- normalise_type ty'
1266 ; return ( args_co `mkTransCo` first_co `mkTransCo` rest_co
1267 , nty ) }
1268 _ -> -- No unique matching family instance exists;
1269 -- we do not do anything
1270 return (args_co, mkTyConApp tc ntys) }}}
1271
1272 ---------------
1273 -- | Normalise arguments to a tycon
1274 normaliseTcArgs :: FamInstEnvs -- ^ env't with family instances
1275 -> Role -- ^ desired role of output coercion
1276 -> TyCon -- ^ tc
1277 -> [Type] -- ^ tys
1278 -> (Coercion, [Type]) -- ^ co :: tc tys ~ tc new_tys
1279 normaliseTcArgs env role tc tys
1280 = initNormM env role (tyCoVarsOfTypes tys) $
1281 normalise_tc_args tc tys
1282
1283 normalise_tc_args :: TyCon -> [Type] -- tc tys
1284 -> NormM (Coercion, [Type]) -- (co, new_tys), where
1285 -- co :: tc tys ~ tc new_tys
1286 normalise_tc_args tc tys
1287 = do { role <- getRole
1288 ; (cois, ntys) <- zipWithAndUnzipM normalise_type_role
1289 tys (tyConRolesX role tc)
1290 ; return (mkTyConAppCo role tc cois, ntys) }
1291 where
1292 normalise_type_role ty r = withRole r $ normalise_type ty
1293
1294 ---------------
1295 normaliseType :: FamInstEnvs
1296 -> Role -- desired role of coercion
1297 -> Type -> (Coercion, Type)
1298 normaliseType env role ty
1299 = initNormM env role (tyCoVarsOfType ty) $ normalise_type ty
1300
1301 normalise_type :: Type -- old type
1302 -> NormM (Coercion, Type) -- (coercion,new type), where
1303 -- co :: old-type ~ new_type
1304 -- Normalise the input type, by eliminating *all* type-function redexes
1305 -- but *not* newtypes (which are visible to the programmer)
1306 -- Returns with Refl if nothing happens
1307 -- Does nothing to newtypes
1308 -- The returned coercion *must* be *homogeneous*
1309 -- See Note [Normalising types]
1310 -- Try to not to disturb type synonyms if possible
1311
1312 normalise_type
1313 = go
1314 where
1315 go (TyConApp tc tys) = normalise_tc_app tc tys
1316 go ty@(LitTy {}) = do { r <- getRole
1317 ; return (mkReflCo r ty, ty) }
1318 go (AppTy ty1 ty2)
1319 = do { (co, nty1) <- go ty1
1320 ; (arg, nty2) <- withRole Nominal $ go ty2
1321 ; return (mkAppCo co arg, mkAppTy nty1 nty2) }
1322 go (FunTy ty1 ty2)
1323 = do { (co1, nty1) <- go ty1
1324 ; (co2, nty2) <- go ty2
1325 ; r <- getRole
1326 ; return (mkFunCo r co1 co2, mkFunTy nty1 nty2) }
1327 go (ForAllTy (TvBndr tyvar vis) ty)
1328 = do { (lc', tv', h, ki') <- normalise_tyvar_bndr tyvar
1329 ; (co, nty) <- withLC lc' $ normalise_type ty
1330 ; let tv2 = setTyVarKind tv' ki'
1331 ; return (mkForAllCo tv' h co, ForAllTy (TvBndr tv2 vis) nty) }
1332 go (TyVarTy tv) = normalise_tyvar tv
1333 go (CastTy ty co)
1334 = do { (nco, nty) <- go ty
1335 ; lc <- getLC
1336 ; let co' = substRightCo lc co
1337 ; return (castCoercionKind nco co co', mkCastTy nty co') }
1338 go (CoercionTy co)
1339 = do { lc <- getLC
1340 ; r <- getRole
1341 ; let right_co = substRightCo lc co
1342 ; return ( mkProofIrrelCo r
1343 (liftCoSubst Nominal lc (coercionType co))
1344 co right_co
1345 , mkCoercionTy right_co ) }
1346
1347 normalise_tyvar :: TyVar -> NormM (Coercion, Type)
1348 normalise_tyvar tv
1349 = ASSERT( isTyVar tv )
1350 do { lc <- getLC
1351 ; r <- getRole
1352 ; return $ case liftCoSubstTyVar lc r tv of
1353 Just co -> (co, pSnd $ coercionKind co)
1354 Nothing -> (mkReflCo r ty, ty) }
1355 where ty = mkTyVarTy tv
1356
1357 normalise_tyvar_bndr :: TyVar -> NormM (LiftingContext, TyVar, Coercion, Kind)
1358 normalise_tyvar_bndr tv
1359 = do { lc1 <- getLC
1360 ; env <- getEnv
1361 ; let callback lc ki = runNormM (normalise_type ki) env lc Nominal
1362 ; return $ liftCoSubstVarBndrCallback callback lc1 tv }
1363
1364 -- | a monad for the normalisation functions, reading 'FamInstEnvs',
1365 -- a 'LiftingContext', and a 'Role'.
1366 newtype NormM a = NormM { runNormM ::
1367 FamInstEnvs -> LiftingContext -> Role -> a }
1368
1369 initNormM :: FamInstEnvs -> Role
1370 -> TyCoVarSet -- the in-scope variables
1371 -> NormM a -> a
1372 initNormM env role vars (NormM thing_inside)
1373 = thing_inside env lc role
1374 where
1375 in_scope = mkInScopeSet vars
1376 lc = emptyLiftingContext in_scope
1377
1378 getRole :: NormM Role
1379 getRole = NormM (\ _ _ r -> r)
1380
1381 getLC :: NormM LiftingContext
1382 getLC = NormM (\ _ lc _ -> lc)
1383
1384 getEnv :: NormM FamInstEnvs
1385 getEnv = NormM (\ env _ _ -> env)
1386
1387 withRole :: Role -> NormM a -> NormM a
1388 withRole r thing = NormM $ \ envs lc _old_r -> runNormM thing envs lc r
1389
1390 withLC :: LiftingContext -> NormM a -> NormM a
1391 withLC lc thing = NormM $ \ envs _old_lc r -> runNormM thing envs lc r
1392
1393 instance Monad NormM where
1394 ma >>= fmb = NormM $ \env lc r ->
1395 let a = runNormM ma env lc r in
1396 runNormM (fmb a) env lc r
1397
1398 instance Functor NormM where
1399 fmap = liftM
1400 instance Applicative NormM where
1401 pure x = NormM $ \ _ _ _ -> x
1402 (<*>) = ap
1403
1404 {-
1405 ************************************************************************
1406 * *
1407 Flattening
1408 * *
1409 ************************************************************************
1410
1411 Note [Flattening]
1412 ~~~~~~~~~~~~~~~~~
1413 As described in "Closed type families with overlapping equations"
1414 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
1415 we need to flatten core types before unifying them, when checking for "surely-apart"
1416 against earlier equations of a closed type family.
1417 Flattening means replacing all top-level uses of type functions with
1418 fresh variables, *taking care to preserve sharing*. That is, the type
1419 (Either (F a b) (F a b)) should flatten to (Either c c), never (Either
1420 c d).
1421
1422 Here is a nice example of why it's all necessary:
1423
1424 type family F a b where
1425 F Int Bool = Char
1426 F a b = Double
1427 type family G a -- open, no instances
1428
1429 How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
1430 while the second equation does. But, before reducing, we must make sure that the
1431 target can never become (F Int Bool). Well, no matter what G Float becomes, it
1432 certainly won't become *both* Int and Bool, so indeed we're safe reducing
1433 (F (G Float) (G Float)) to Double.
1434
1435 This is necessary not only to get more reductions (which we might be
1436 willing to give up on), but for substitutivity. If we have (F x x), we
1437 can see that (F x x) can reduce to Double. So, it had better be the
1438 case that (F blah blah) can reduce to Double, no matter what (blah)
1439 is! Flattening as done below ensures this.
1440
1441 flattenTys is defined here because of module dependencies.
1442 -}
1443
1444 data FlattenEnv = FlattenEnv { fe_type_map :: TypeMap TyVar
1445 , fe_subst :: TCvSubst }
1446
1447 emptyFlattenEnv :: InScopeSet -> FlattenEnv
1448 emptyFlattenEnv in_scope
1449 = FlattenEnv { fe_type_map = emptyTypeMap
1450 , fe_subst = mkEmptyTCvSubst in_scope }
1451
1452 -- See Note [Flattening]
1453 flattenTys :: InScopeSet -> [Type] -> [Type]
1454 flattenTys in_scope tys = snd $ coreFlattenTys env tys
1455 where
1456 -- when we hit a type function, we replace it with a fresh variable
1457 -- but, we need to make sure that this fresh variable isn't mentioned
1458 -- *anywhere* in the types we're flattening, even if locally-bound in
1459 -- a forall. That way, we can ensure consistency both within and outside
1460 -- of that forall.
1461 all_in_scope = in_scope `extendInScopeSetSet` allTyVarsInTys tys
1462 env = emptyFlattenEnv all_in_scope
1463
1464 coreFlattenTys :: FlattenEnv -> [Type] -> (FlattenEnv, [Type])
1465 coreFlattenTys = go []
1466 where
1467 go rtys env [] = (env, reverse rtys)
1468 go rtys env (ty : tys)
1469 = let (env', ty') = coreFlattenTy env ty in
1470 go (ty' : rtys) env' tys
1471
1472 coreFlattenTy :: FlattenEnv -> Type -> (FlattenEnv, Type)
1473 coreFlattenTy = go
1474 where
1475 go env ty | Just ty' <- coreView ty = go env ty'
1476
1477 go env (TyVarTy tv) = (env, substTyVar (fe_subst env) tv)
1478 go env (AppTy ty1 ty2) = let (env1, ty1') = go env ty1
1479 (env2, ty2') = go env1 ty2 in
1480 (env2, AppTy ty1' ty2')
1481 go env (TyConApp tc tys)
1482 -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
1483 -- which are generative and thus can be preserved during flattening
1484 | not (isGenerativeTyCon tc Nominal)
1485 = let (env', tv) = coreFlattenTyFamApp env tc tys in
1486 (env', mkTyVarTy tv)
1487
1488 | otherwise
1489 = let (env', tys') = coreFlattenTys env tys in
1490 (env', mkTyConApp tc tys')
1491
1492 go env (FunTy ty1 ty2) = let (env1, ty1') = go env ty1
1493 (env2, ty2') = go env1 ty2 in
1494 (env2, mkFunTy ty1' ty2')
1495
1496 go env (ForAllTy (TvBndr tv vis) ty)
1497 = let (env1, tv') = coreFlattenVarBndr env tv
1498 (env2, ty') = go env1 ty in
1499 (env2, ForAllTy (TvBndr tv' vis) ty')
1500
1501 go env ty@(LitTy {}) = (env, ty)
1502
1503 go env (CastTy ty co) = let (env1, ty') = go env ty
1504 (env2, co') = coreFlattenCo env1 co in
1505 (env2, CastTy ty' co')
1506
1507 go env (CoercionTy co) = let (env', co') = coreFlattenCo env co in
1508 (env', CoercionTy co')
1509
1510 -- when flattening, we don't care about the contents of coercions.
1511 -- so, just return a fresh variable of the right (flattened) type
1512 coreFlattenCo :: FlattenEnv -> Coercion -> (FlattenEnv, Coercion)
1513 coreFlattenCo env co
1514 = (env2, mkCoVarCo covar)
1515 where
1516 (env1, kind') = coreFlattenTy env (coercionType co)
1517 fresh_name = mkFlattenFreshCoName
1518 subst1 = fe_subst env1
1519 in_scope = getTCvInScope subst1
1520 covar = uniqAway in_scope (mkCoVar fresh_name kind')
1521 env2 = env1 { fe_subst = subst1 `extendTCvInScope` covar }
1522
1523 coreFlattenVarBndr :: FlattenEnv -> TyVar -> (FlattenEnv, TyVar)
1524 coreFlattenVarBndr env tv
1525 | kind' `eqType` kind
1526 = ( env { fe_subst = extendTvSubst old_subst tv (mkTyVarTy tv) }
1527 -- override any previous binding for tv
1528 , tv)
1529
1530 | otherwise
1531 = let new_tv = uniqAway (getTCvInScope old_subst) (setTyVarKind tv kind')
1532 new_subst = extendTvSubstWithClone old_subst tv new_tv
1533 in
1534 (env' { fe_subst = new_subst }, new_tv)
1535 where
1536 kind = tyVarKind tv
1537 (env', kind') = coreFlattenTy env kind
1538 old_subst = fe_subst env
1539
1540 coreFlattenTyFamApp :: FlattenEnv
1541 -> TyCon -- type family tycon
1542 -> [Type] -- args
1543 -> (FlattenEnv, TyVar)
1544 coreFlattenTyFamApp env fam_tc fam_args
1545 = case lookupTypeMap type_map fam_ty of
1546 Just tv -> (env, tv)
1547 -- we need fresh variables here, but this is called far from
1548 -- any good source of uniques. So, we just use the fam_tc's unique
1549 -- and trust uniqAway to avoid clashes. Recall that the in_scope set
1550 -- contains *all* tyvars, even locally bound ones elsewhere in the
1551 -- overall type, so this really is fresh.
1552 Nothing -> let tyvar_name = mkFlattenFreshTyName fam_tc
1553 tv = uniqAway (getTCvInScope subst) $
1554 mkTyVar tyvar_name (typeKind fam_ty)
1555 env' = env { fe_type_map = extendTypeMap type_map fam_ty tv
1556 , fe_subst = extendTCvInScope subst tv }
1557 in (env', tv)
1558 where fam_ty = mkTyConApp fam_tc fam_args
1559 FlattenEnv { fe_type_map = type_map
1560 , fe_subst = subst } = env
1561
1562 -- | Get the set of all type variables mentioned anywhere in the list
1563 -- of types. These variables are not necessarily free.
1564 allTyVarsInTys :: [Type] -> VarSet
1565 allTyVarsInTys [] = emptyVarSet
1566 allTyVarsInTys (ty:tys) = allTyVarsInTy ty `unionVarSet` allTyVarsInTys tys
1567
1568 -- | Get the set of all type variables mentioned anywhere in a type.
1569 allTyVarsInTy :: Type -> VarSet
1570 allTyVarsInTy = go
1571 where
1572 go (TyVarTy tv) = unitVarSet tv
1573 go (TyConApp _ tys) = allTyVarsInTys tys
1574 go (AppTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1575 go (FunTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1576 go (ForAllTy (TvBndr tv _) ty) = unitVarSet tv `unionVarSet`
1577 go (tyVarKind tv) `unionVarSet`
1578 go ty
1579 -- Don't remove the tv from the set!
1580 go (LitTy {}) = emptyVarSet
1581 go (CastTy ty co) = go ty `unionVarSet` go_co co
1582 go (CoercionTy co) = go_co co
1583
1584 go_co (Refl _ ty) = go ty
1585 go_co (TyConAppCo _ _ args) = go_cos args
1586 go_co (AppCo co arg) = go_co co `unionVarSet` go_co arg
1587 go_co (ForAllCo tv h co)
1588 = unionVarSets [unitVarSet tv, go_co co, go_co h]
1589 go_co (CoVarCo cv) = unitVarSet cv
1590 go_co (AxiomInstCo _ _ cos) = go_cos cos
1591 go_co (UnivCo p _ t1 t2) = go_prov p `unionVarSet` go t1 `unionVarSet` go t2
1592 go_co (SymCo co) = go_co co
1593 go_co (TransCo c1 c2) = go_co c1 `unionVarSet` go_co c2
1594 go_co (NthCo _ co) = go_co co
1595 go_co (LRCo _ co) = go_co co
1596 go_co (InstCo co arg) = go_co co `unionVarSet` go_co arg
1597 go_co (CoherenceCo c1 c2) = go_co c1 `unionVarSet` go_co c2
1598 go_co (KindCo co) = go_co co
1599 go_co (SubCo co) = go_co co
1600 go_co (AxiomRuleCo _ cs) = go_cos cs
1601
1602 go_cos = foldr (unionVarSet . go_co) emptyVarSet
1603
1604 go_prov UnsafeCoerceProv = emptyVarSet
1605 go_prov (PhantomProv co) = go_co co
1606 go_prov (ProofIrrelProv co) = go_co co
1607 go_prov (PluginProv _) = emptyVarSet
1608 go_prov (HoleProv _) = emptyVarSet
1609
1610 mkFlattenFreshTyName :: Uniquable a => a -> Name
1611 mkFlattenFreshTyName unq
1612 = mkSysTvName (getUnique unq) (fsLit "flt")
1613
1614 mkFlattenFreshCoName :: Name
1615 mkFlattenFreshCoName
1616 = mkSystemVarName (deriveUnique eqPrimTyConKey 71) (fsLit "flc")