62906dd6c8f479055fe6e33bc1c24085e606f2cc
[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 UniqFM
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 contructors
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
364 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
365 -- See Note [FamInstEnv]
366
367 type FamInstEnvs = (FamInstEnv, FamInstEnv)
368 -- External package inst-env, Home-package inst-env
369
370 newtype FamilyInstEnv
371 = FamIE [FamInst] -- The instances for a particular family, in any order
372
373 instance Outputable FamilyInstEnv where
374 ppr (FamIE fs) = text "FamIE" <+> vcat (map ppr fs)
375
376 -- INVARIANTS:
377 -- * The fs_tvs are distinct in each FamInst
378 -- of a range value of the map (so we can safely unify them)
379
380 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
381 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
382
383 emptyFamInstEnv :: FamInstEnv
384 emptyFamInstEnv = emptyUFM
385
386 famInstEnvElts :: FamInstEnv -> [FamInst]
387 famInstEnvElts fi = [elt | FamIE elts <- eltsUFM fi, elt <- elts]
388
389 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
390 familyInstances (pkg_fie, home_fie) fam
391 = get home_fie ++ get pkg_fie
392 where
393 get env = case lookupUFM env fam of
394 Just (FamIE insts) -> insts
395 Nothing -> []
396
397 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
398 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
399
400 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
401 extendFamInstEnv inst_env
402 ins_item@(FamInst {fi_fam = cls_nm})
403 = addToUFM_C add inst_env cls_nm (FamIE [ins_item])
404 where
405 add (FamIE items) _ = FamIE (ins_item:items)
406
407 deleteFromFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
408 -- Used only for overriding in GHCi
409 deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm})
410 = adjustUFM adjust inst_env fam_nm
411 where
412 adjust :: FamilyInstEnv -> FamilyInstEnv
413 adjust (FamIE items)
414 = FamIE (filterOut (identicalFamInstHead fam_inst) items)
415
416 identicalFamInstHead :: FamInst -> FamInst -> Bool
417 -- ^ True when the LHSs are identical
418 -- Used for overriding in GHCi
419 identicalFamInstHead (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
420 = coAxiomTyCon ax1 == coAxiomTyCon ax2
421 && numBranches brs1 == numBranches brs2
422 && and ((zipWith identical_branch `on` fromBranches) brs1 brs2)
423 where
424 brs1 = coAxiomBranches ax1
425 brs2 = coAxiomBranches ax2
426
427 identical_branch br1 br2
428 = isJust (tcMatchTys lhs1 lhs2)
429 && isJust (tcMatchTys lhs2 lhs1)
430 where
431 lhs1 = coAxBranchLHS br1
432 lhs2 = coAxBranchLHS br2
433
434 {-
435 ************************************************************************
436 * *
437 Compatibility
438 * *
439 ************************************************************************
440
441 Note [Apartness]
442 ~~~~~~~~~~~~~~~~
443 In dealing with closed type families, we must be able to check that one type
444 will never reduce to another. This check is called /apartness/. The check
445 is always between a target (which may be an arbitrary type) and a pattern.
446 Here is how we do it:
447
448 apart(target, pattern) = not (unify(flatten(target), pattern))
449
450 where flatten (implemented in flattenTys, below) converts all type-family
451 applications into fresh variables. (See Note [Flattening].)
452
453 Note [Compatibility]
454 ~~~~~~~~~~~~~~~~~~~~
455 Two patterns are /compatible/ if either of the following conditions hold:
456 1) The patterns are apart.
457 2) The patterns unify with a substitution S, and their right hand sides
458 equal under that substitution.
459
460 For open type families, only compatible instances are allowed. For closed
461 type families, the story is slightly more complicated. Consider the following:
462
463 type family F a where
464 F Int = Bool
465 F a = Int
466
467 g :: Show a => a -> F a
468 g x = length (show x)
469
470 Should that type-check? No. We need to allow for the possibility that 'a'
471 might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
472 only when we can be sure that 'a' is not Int.
473
474 To achieve this, after finding a possible match within the equations, we have to
475 go back to all previous equations and check that, under the
476 substitution induced by the match, other branches are surely apart. (See
477 Note [Apartness].) This is similar to what happens with class
478 instance selection, when we need to guarantee that there is only a match and
479 no unifiers. The exact algorithm is different here because the the
480 potentially-overlapping group is closed.
481
482 As another example, consider this:
483
484 type family G x where
485 G Int = Bool
486 G a = Double
487
488 type family H y
489 -- no instances
490
491 Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
492 simplify to be Int. So, (G (H Char)) is stuck, for now.
493
494 While everything above is quite sound, it isn't as expressive as we'd like.
495 Consider this:
496
497 type family J a where
498 J Int = Int
499 J a = a
500
501 Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
502 b is instantiated with Int, but the RHSs coincide there, so it's all OK.
503
504 So, the rule is this: when looking up a branch in a closed type family, we
505 find a branch that matches the target, but then we make sure that the target
506 is apart from every previous *incompatible* branch. We don't check the
507 branches that are compatible with the matching branch, because they are either
508 irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
509 -}
510
511 -- See Note [Compatibility]
512 compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
513 compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
514 (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
515 = case tcUnifyTysFG (const BindMe) lhs1 lhs2 of
516 SurelyApart -> True
517 Unifiable subst
518 | Type.substTyAddInScope subst rhs1 `eqType`
519 Type.substTyAddInScope subst rhs2
520 -> True
521 _ -> False
522
523 -- | Result of testing two type family equations for injectiviy.
524 data InjectivityCheckResult
525 = InjectivityAccepted
526 -- ^ Either RHSs are distinct or unification of RHSs leads to unification of
527 -- LHSs
528 | InjectivityUnified CoAxBranch CoAxBranch
529 -- ^ RHSs unify but LHSs don't unify under that substitution. Relevant for
530 -- closed type families where equation after unification might be
531 -- overlpapped (in which case it is OK if they don't unify). Constructor
532 -- stores axioms after unification.
533
534 -- | Check whether two type family axioms don't violate injectivity annotation.
535 injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch
536 -> InjectivityCheckResult
537 injectiveBranches injectivity
538 ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
539 ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
540 -- See Note [Verifying injectivity annotation]. This function implements first
541 -- check described there.
542 = let getInjArgs = filterByList injectivity
543 in case tcUnifyTyWithTFs True rhs1 rhs2 of -- True = two-way pre-unification
544 Nothing -> InjectivityAccepted -- RHS are different, so equations are
545 -- injective.
546 Just subst -> -- RHS unify under a substitution
547 let lhs1Subst = Type.substTys subst (getInjArgs lhs1)
548 lhs2Subst = Type.substTys subst (getInjArgs lhs2)
549 -- If LHSs are equal under the substitution used for RHSs then this pair
550 -- of equations does not violate injectivity annotation. If LHSs are not
551 -- equal under that substitution then this pair of equations violates
552 -- injectivity annotation, but for closed type families it still might
553 -- be the case that one LHS after substitution is unreachable.
554 in if eqTypes lhs1Subst lhs2Subst
555 then InjectivityAccepted
556 else InjectivityUnified ( ax1 { cab_lhs = Type.substTys subst lhs1
557 , cab_rhs = Type.substTy subst rhs1 })
558 ( ax2 { cab_lhs = Type.substTys subst lhs2
559 , cab_rhs = Type.substTy subst rhs2 })
560
561 -- takes a CoAxiom with unknown branch incompatibilities and computes
562 -- the compatibilities
563 -- See Note [Storing compatibility] in CoAxiom
564 computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
565 computeAxiomIncomps branches
566 = snd (mapAccumL go [] branches)
567 where
568 go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
569 go prev_brs cur_br
570 = (cur_br : prev_brs, new_br)
571 where
572 new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
573
574 mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
575 mk_incomps prev_brs cur_br
576 = filter (not . compatibleBranches cur_br) prev_brs
577
578 {-
579 ************************************************************************
580 * *
581 Constructing axioms
582 These functions are here because tidyType / tcUnifyTysFG
583 are not available in CoAxiom
584
585 Also computeAxiomIncomps is too sophisticated for CoAxiom
586 * *
587 ************************************************************************
588
589 Note [Tidy axioms when we build them]
590 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
591 We print out axioms and don't want to print stuff like
592 F k k a b = ...
593 Instead we must tidy those kind variables. See Trac #7524.
594 -}
595
596 -- all axiom roles are Nominal, as this is only used with type families
597 mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
598 -> [CoVar] -- possibly stale covars
599 -> [Type] -- LHS patterns
600 -> Type -- RHS
601 -> [Role]
602 -> SrcSpan
603 -> CoAxBranch
604 mkCoAxBranch tvs cvs lhs rhs roles loc
605 = CoAxBranch { cab_tvs = tvs1
606 , cab_cvs = cvs1
607 , cab_lhs = tidyTypes env lhs
608 , cab_roles = roles
609 , cab_rhs = tidyType env rhs
610 , cab_loc = loc
611 , cab_incomps = placeHolderIncomps }
612 where
613 (env1, tvs1) = tidyTyCoVarBndrs emptyTidyEnv tvs
614 (env, cvs1) = tidyTyCoVarBndrs env1 cvs
615 -- See Note [Tidy axioms when we build them]
616
617 -- all of the following code is here to avoid mutual dependencies with
618 -- Coercion
619 mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
620 mkBranchedCoAxiom ax_name fam_tc branches
621 = CoAxiom { co_ax_unique = nameUnique ax_name
622 , co_ax_name = ax_name
623 , co_ax_tc = fam_tc
624 , co_ax_role = Nominal
625 , co_ax_implicit = False
626 , co_ax_branches = manyBranches (computeAxiomIncomps branches) }
627
628 mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
629 mkUnbranchedCoAxiom ax_name fam_tc branch
630 = CoAxiom { co_ax_unique = nameUnique ax_name
631 , co_ax_name = ax_name
632 , co_ax_tc = fam_tc
633 , co_ax_role = Nominal
634 , co_ax_implicit = False
635 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
636
637 mkSingleCoAxiom :: Role -> Name
638 -> [TyVar] -> [CoVar] -> TyCon -> [Type] -> Type
639 -> CoAxiom Unbranched
640 -- Make a single-branch CoAxiom, incluidng making the branch itself
641 -- Used for both type family (Nominal) and data family (Representational)
642 -- axioms, hence passing in the Role
643 mkSingleCoAxiom role ax_name tvs cvs fam_tc lhs_tys rhs_ty
644 = CoAxiom { co_ax_unique = nameUnique ax_name
645 , co_ax_name = ax_name
646 , co_ax_tc = fam_tc
647 , co_ax_role = role
648 , co_ax_implicit = False
649 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
650 where
651 branch = mkCoAxBranch tvs cvs lhs_tys rhs_ty
652 (map (const Nominal) tvs)
653 (getSrcSpan ax_name)
654
655 -- | Create a coercion constructor (axiom) suitable for the given
656 -- newtype 'TyCon'. The 'Name' should be that of a new coercion
657 -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
658 -- the type the appropriate right hand side of the @newtype@, with
659 -- the free variables a subset of those 'TyVar's.
660 mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
661 mkNewTypeCoAxiom name tycon tvs roles rhs_ty
662 = CoAxiom { co_ax_unique = nameUnique name
663 , co_ax_name = name
664 , co_ax_implicit = True -- See Note [Implicit axioms] in TyCon
665 , co_ax_role = Representational
666 , co_ax_tc = tycon
667 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
668 where
669 branch = mkCoAxBranch tvs [] (mkTyVarTys tvs) rhs_ty
670 roles (getSrcSpan name)
671
672 {-
673 ************************************************************************
674 * *
675 Looking up a family instance
676 * *
677 ************************************************************************
678
679 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
680 Multiple matches are only possible in case of type families (not data
681 families), and then, it doesn't matter which match we choose (as the
682 instances are guaranteed confluent).
683
684 We return the matching family instances and the type instance at which it
685 matches. For example, if we lookup 'T [Int]' and have a family instance
686
687 data instance T [a] = ..
688
689 desugared to
690
691 data :R42T a = ..
692 coe :Co:R42T a :: T [a] ~ :R42T a
693
694 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
695 -}
696
697 -- when matching a type family application, we get a FamInst,
698 -- and the list of types the axiom should be applied to
699 data FamInstMatch = FamInstMatch { fim_instance :: FamInst
700 , fim_tys :: [Type]
701 , fim_cos :: [Coercion]
702 }
703 -- See Note [Over-saturated matches]
704
705 instance Outputable FamInstMatch where
706 ppr (FamInstMatch { fim_instance = inst
707 , fim_tys = tys
708 , fim_cos = cos })
709 = text "match with" <+> parens (ppr inst) <+> ppr tys <+> ppr cos
710
711 lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
712 lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc
713 = get pkg_ie ++ get home_ie
714 where
715 get ie = case lookupUFM ie fam_tc of
716 Nothing -> []
717 Just (FamIE fis) -> fis
718
719 lookupFamInstEnv
720 :: FamInstEnvs
721 -> TyCon -> [Type] -- What we are looking for
722 -> [FamInstMatch] -- Successful matches
723 -- Precondition: the tycon is saturated (or over-saturated)
724
725 lookupFamInstEnv
726 = lookup_fam_inst_env match
727 where
728 match _ _ tpl_tys tys = tcMatchTys tpl_tys tys
729
730 lookupFamInstEnvConflicts
731 :: FamInstEnvs
732 -> FamInst -- Putative new instance
733 -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field)
734 -- E.g. when we are about to add
735 -- f : type instance F [a] = a->a
736 -- we do (lookupFamInstConflicts f [b])
737 -- to find conflicting matches
738 --
739 -- Precondition: the tycon is saturated (or over-saturated)
740
741 lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
742 = lookup_fam_inst_env my_unify envs fam tys
743 where
744 (fam, tys) = famInstSplitLHS fam_inst
745 -- In example above, fam tys' = F [b]
746
747 my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
748 = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs,
749 (ppr fam <+> ppr tys) $$
750 (ppr tpl_tvs <+> ppr tpl_tys) )
751 -- Unification will break badly if the variables overlap
752 -- They shouldn't because we allocate separate uniques for them
753 if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
754 then Nothing
755 else Just noSubst
756 -- Note [Family instance overlap conflicts]
757
758 noSubst = panic "lookupFamInstEnvConflicts noSubst"
759 new_branch = coAxiomSingleBranch new_axiom
760
761 --------------------------------------------------------------------------------
762 -- Type family injectivity checking bits --
763 --------------------------------------------------------------------------------
764
765 {- Note [Verifying injectivity annotation]
766 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
767
768 Injectivity means that the RHS of a type family uniquely determines the LHS (see
769 Note [Type inference for type families with injectivity]). User informs about
770 injectivity using an injectivity annotation and it is GHC's task to verify that
771 that annotation is correct wrt. to type family equations. Whenever we see a new
772 equation of a type family we need to make sure that adding this equation to
773 already known equations of a type family does not violate injectivity annotation
774 supplied by the user (see Note [Injectivity annotation]). Of course if the type
775 family has no injectivity annotation then no check is required. But if a type
776 family has injectivity annotation we need to make sure that the following
777 conditions hold:
778
779 1. For each pair of *different* equations of a type family, one of the following
780 conditions holds:
781
782 A: RHSs are different.
783
784 B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution
785 then it must be possible to unify the LHSs under the same substitution.
786 Example:
787
788 type family FunnyId a = r | r -> a
789 type instance FunnyId Int = Int
790 type instance FunnyId a = a
791
792 RHSs of these two equations unify under [ a |-> Int ] substitution.
793 Under this substitution LHSs are equal therefore these equations don't
794 violate injectivity annotation.
795
796 B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some
797 substitution then either the LHSs unify under the same substitution or
798 the LHS of the latter equation is overlapped by earlier equations.
799 Example 1:
800
801 type family SwapIntChar a = r | r -> a where
802 SwapIntChar Int = Char
803 SwapIntChar Char = Int
804 SwapIntChar a = a
805
806 Say we are checking the last two equations. RHSs unify under [ a |->
807 Int ] substitution but LHSs don't. So we apply the substitution to LHS
808 of last equation and check whether it is overlapped by any of previous
809 equations. Since it is overlapped by the first equation we conclude
810 that pair of last two equations does not violate injectivity
811 annotation.
812
813 A special case of B is when RHSs unify with an empty substitution ie. they
814 are identical.
815
816 If any of the above two conditions holds we conclude that the pair of
817 equations does not violate injectivity annotation. But if we find a pair
818 of equations where neither of the above holds we report that this pair
819 violates injectivity annotation because for a given RHS we don't have a
820 unique LHS. (Note that (B) actually implies (A).)
821
822 Note that we only take into account these LHS patterns that were declared
823 as injective.
824
825 2. If a RHS of a type family equation is a bare type variable then
826 all LHS variables (including implicit kind variables) also have to be bare.
827 In other words, this has to be a sole equation of that type family and it has
828 to cover all possible patterns. So for example this definition will be
829 rejected:
830
831 type family W1 a = r | r -> a
832 type instance W1 [a] = a
833
834 If it were accepted we could call `W1 [W1 Int]`, which would reduce to
835 `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`,
836 which is bogus.
837
838 3. If a RHS of a type family equation is a type family application then the type
839 family is rejected as not injective.
840
841 4. If a LHS type variable that is declared as injective is not mentioned on
842 injective position in the RHS then the type family is rejected as not
843 injective. "Injective position" means either an argument to a type
844 constructor or argument to a type family on injective position.
845
846 See also Note [Injective type families] in TyCon
847 -}
848
849
850 -- | Check whether an open type family equation can be added to already existing
851 -- instance environment without causing conflicts with supplied injectivity
852 -- annotations. Returns list of conflicting axioms (type instance
853 -- declarations).
854 lookupFamInstEnvInjectivityConflicts
855 :: [Bool] -- injectivity annotation for this type family instance
856 -- INVARIANT: list contains at least one True value
857 -> FamInstEnvs -- all type instances seens so far
858 -> FamInst -- new type instance that we're checking
859 -> [CoAxBranch] -- conflicting instance delcarations
860 lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie)
861 fam_inst@(FamInst { fi_axiom = new_axiom })
862 -- See Note [Verifying injectivity annotation]. This function implements
863 -- check (1.B1) for open type families described there.
864 = lookup_inj_fam_conflicts home_ie ++ lookup_inj_fam_conflicts pkg_ie
865 where
866 fam = famInstTyCon fam_inst
867 new_branch = coAxiomSingleBranch new_axiom
868
869 -- filtering function used by `lookup_inj_fam_conflicts` to check whether
870 -- a pair of equations conflicts with the injectivity annotation.
871 isInjConflict (FamInst { fi_axiom = old_axiom })
872 | InjectivityAccepted <-
873 injectiveBranches injList (coAxiomSingleBranch old_axiom) new_branch
874 = False -- no conflict
875 | otherwise = True
876
877 lookup_inj_fam_conflicts ie
878 | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUFM ie fam
879 = map (coAxiomSingleBranch . fi_axiom) $
880 filter isInjConflict insts
881 | otherwise = []
882
883
884 --------------------------------------------------------------------------------
885 -- Type family overlap checking bits --
886 --------------------------------------------------------------------------------
887
888 {-
889 Note [Family instance overlap conflicts]
890 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
891 - In the case of data family instances, any overlap is fundamentally a
892 conflict (as these instances imply injective type mappings).
893
894 - In the case of type family instances, overlap is admitted as long as
895 the right-hand sides of the overlapping rules coincide under the
896 overlap substitution. eg
897 type instance F a Int = a
898 type instance F Int b = b
899 These two overlap on (F Int Int) but then both RHSs are Int,
900 so all is well. We require that they are syntactically equal;
901 anything else would be difficult to test for at this stage.
902 -}
903
904 ------------------------------------------------------------
905 -- Might be a one-way match or a unifier
906 type MatchFun = FamInst -- The FamInst template
907 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
908 -> [Type] -- Target to match against
909 -> Maybe TCvSubst
910
911 lookup_fam_inst_env' -- The worker, local to this module
912 :: MatchFun
913 -> FamInstEnv
914 -> TyCon -> [Type] -- What we are looking for
915 -> [FamInstMatch]
916 lookup_fam_inst_env' match_fun ie fam match_tys
917 | isOpenFamilyTyCon fam
918 , Just (FamIE insts) <- lookupUFM ie fam
919 = find insts -- The common case
920 | otherwise = []
921 where
922
923 find [] = []
924 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs
925 , fi_tys = tpl_tys }) : rest)
926 -- Fast check for no match, uses the "rough match" fields
927 | instanceCantMatch rough_tcs mb_tcs
928 = find rest
929
930 -- Proper check
931 | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
932 = (FamInstMatch { fim_instance = item
933 , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2
934 , fim_cos = ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
935 substCoVars subst tpl_cvs
936 })
937 : find rest
938
939 -- No match => try next
940 | otherwise
941 = find rest
942
943 where
944 (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
945
946 -- Precondition: the tycon is saturated (or over-saturated)
947
948 -- Deal with over-saturation
949 -- See Note [Over-saturated matches]
950 split_tys tpl_tys
951 | isTypeFamilyTyCon fam
952 = pre_rough_split_tys
953
954 | otherwise
955 = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
956 rough_tcs = roughMatchTcs match_tys1
957 in (rough_tcs, match_tys1, match_tys2)
958
959 (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
960 pre_rough_split_tys
961 = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
962
963 lookup_fam_inst_env -- The worker, local to this module
964 :: MatchFun
965 -> FamInstEnvs
966 -> TyCon -> [Type] -- What we are looking for
967 -> [FamInstMatch] -- Successful matches
968
969 -- Precondition: the tycon is saturated (or over-saturated)
970
971 lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
972 = lookup_fam_inst_env' match_fun home_ie fam tys
973 ++ lookup_fam_inst_env' match_fun pkg_ie fam tys
974
975 {-
976 Note [Over-saturated matches]
977 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
978 It's ok to look up an over-saturated type constructor. E.g.
979 type family F a :: * -> *
980 type instance F (a,b) = Either (a->b)
981
982 The type instance gives rise to a newtype TyCon (at a higher kind
983 which you can't do in Haskell!):
984 newtype FPair a b = FP (Either (a->b))
985
986 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
987 (FPair, [Int,Bool,Char])
988 The "extra" type argument [Char] just stays on the end.
989
990 We handle data families and type families separately here:
991
992 * For type families, all instances of a type family must have the
993 same arity, so we can precompute the split between the match_tys
994 and the overflow tys. This is done in pre_rough_split_tys.
995
996 * For data family instances, though, we need to re-split for each
997 instance, because the breakdown might be different for each
998 instance. Why? Because of eta reduction; see
999 Note [Eta reduction for data families].
1000 -}
1001
1002 -- checks if one LHS is dominated by a list of other branches
1003 -- in other words, if an application would match the first LHS, it is guaranteed
1004 -- to match at least one of the others. The RHSs are ignored.
1005 -- This algorithm is conservative:
1006 -- True -> the LHS is definitely covered by the others
1007 -- False -> no information
1008 -- It is currently (Oct 2012) used only for generating errors for
1009 -- inaccessible branches. If these errors go unreported, no harm done.
1010 -- This is defined here to avoid a dependency from CoAxiom to Unify
1011 isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
1012 isDominatedBy branch branches
1013 = or $ map match branches
1014 where
1015 lhs = coAxBranchLHS branch
1016 match (CoAxBranch { cab_lhs = tys })
1017 = isJust $ tcMatchTys tys lhs
1018
1019 {-
1020 ************************************************************************
1021 * *
1022 Choosing an axiom application
1023 * *
1024 ************************************************************************
1025
1026 The lookupFamInstEnv function does a nice job for *open* type families,
1027 but we also need to handle closed ones when normalising a type:
1028 -}
1029
1030 reduceTyFamApp_maybe :: FamInstEnvs
1031 -> Role -- Desired role of result coercion
1032 -> TyCon -> [Type]
1033 -> Maybe (Coercion, Type)
1034 -- Attempt to do a *one-step* reduction of a type-family application
1035 -- but *not* newtypes
1036 -- Works on type-synonym families always; data-families only if
1037 -- the role we seek is representational
1038 -- It does *not* normlise the type arguments first, so this may not
1039 -- go as far as you want. If you want normalised type arguments,
1040 -- use normaliseTcArgs first.
1041 --
1042 -- The TyCon can be oversaturated.
1043 -- Works on both open and closed families
1044 --
1045 -- Always returns a *homogeneous* coercion -- type family reductions are always
1046 -- homogeneous
1047 reduceTyFamApp_maybe envs role tc tys
1048 | Phantom <- role
1049 = Nothing
1050
1051 | case role of
1052 Representational -> isOpenFamilyTyCon tc
1053 _ -> isOpenTypeFamilyTyCon tc
1054 -- If we seek a representational coercion
1055 -- (e.g. the call in topNormaliseType_maybe) then we can
1056 -- unwrap data families as well as type-synonym families;
1057 -- otherwise only type-synonym families
1058 , FamInstMatch { fim_instance = FamInst { fi_axiom = ax }
1059 , fim_tys = inst_tys
1060 , fim_cos = inst_cos } : _ <- lookupFamInstEnv envs tc tys
1061 -- NB: Allow multiple matches because of compatible overlap
1062
1063 = let co = mkUnbranchedAxInstCo role ax inst_tys inst_cos
1064 ty = pSnd (coercionKind co)
1065 in Just (co, ty)
1066
1067 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
1068 , Just (ind, inst_tys, inst_cos) <- chooseBranch ax tys
1069 = let co = mkAxInstCo role ax ind inst_tys inst_cos
1070 ty = pSnd (coercionKind co)
1071 in Just (co, ty)
1072
1073 | Just ax <- isBuiltInSynFamTyCon_maybe tc
1074 , Just (coax,ts,ty) <- sfMatchFam ax tys
1075 = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
1076 in Just (co, ty)
1077
1078 | otherwise
1079 = Nothing
1080
1081 -- The axiom can be oversaturated. (Closed families only.)
1082 chooseBranch :: CoAxiom Branched -> [Type]
1083 -> Maybe (BranchIndex, [Type], [Coercion]) -- found match, with args
1084 chooseBranch axiom tys
1085 = do { let num_pats = coAxiomNumPats axiom
1086 (target_tys, extra_tys) = splitAt num_pats tys
1087 branches = coAxiomBranches axiom
1088 ; (ind, inst_tys, inst_cos)
1089 <- findBranch (fromBranches branches) target_tys
1090 ; return ( ind, inst_tys `chkAppend` extra_tys, inst_cos ) }
1091
1092 -- The axiom must *not* be oversaturated
1093 findBranch :: [CoAxBranch] -- branches to check
1094 -> [Type] -- target types
1095 -> Maybe (BranchIndex, [Type], [Coercion])
1096 -- coercions relate requested types to returned axiom LHS at role N
1097 findBranch branches target_tys
1098 = go 0 branches
1099 where
1100 go ind (branch@(CoAxBranch { cab_tvs = tpl_tvs, cab_cvs = tpl_cvs
1101 , cab_lhs = tpl_lhs
1102 , cab_incomps = incomps }) : rest)
1103 = let in_scope = mkInScopeSet (unionVarSets $
1104 map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
1105 -- See Note [Flattening] below
1106 flattened_target = flattenTys in_scope target_tys
1107 in case tcMatchTys tpl_lhs target_tys of
1108 Just subst -- matching worked. now, check for apartness.
1109 | apartnessCheck flattened_target branch
1110 -> -- matching worked & we're apart from all incompatible branches.
1111 -- success
1112 ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
1113 Just (ind, substTyVars subst tpl_tvs, substCoVars subst tpl_cvs)
1114
1115 -- failure. keep looking
1116 _ -> go (ind+1) rest
1117
1118 -- fail if no branches left
1119 go _ [] = Nothing
1120
1121 -- | Do an apartness check, as described in the "Closed Type Families" paper
1122 -- (POPL '14). This should be used when determining if an equation
1123 -- ('CoAxBranch') of a closed type family can be used to reduce a certain target
1124 -- type family application.
1125 apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure
1126 -- they're flattened! See Note [Flattening].
1127 -- (NB: This "flat" is a different
1128 -- "flat" than is used in TcFlatten.)
1129 -> CoAxBranch -- ^ the candidate equation we wish to use
1130 -- Precondition: this matches the target
1131 -> Bool -- ^ True <=> equation can fire
1132 apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps })
1133 = all (isSurelyApart
1134 . tcUnifyTysFG (const BindMe) flattened_target
1135 . coAxBranchLHS) incomps
1136 where
1137 isSurelyApart SurelyApart = True
1138 isSurelyApart _ = False
1139
1140 {-
1141 ************************************************************************
1142 * *
1143 Looking up a family instance
1144 * *
1145 ************************************************************************
1146
1147 Note [Normalising types]
1148 ~~~~~~~~~~~~~~~~~~~~~~~~
1149 The topNormaliseType function removes all occurrences of type families
1150 and newtypes from the top-level structure of a type. normaliseTcApp does
1151 the type family lookup and is fairly straightforward. normaliseType is
1152 a little more involved.
1153
1154 The complication comes from the fact that a type family might be used in the
1155 kind of a variable bound in a forall. We wish to remove this type family
1156 application, but that means coming up with a fresh variable (with the new
1157 kind). Thus, we need a substitution to be built up as we recur through the
1158 type. However, an ordinary TCvSubst just won't do: when we hit a type variable
1159 whose kind has changed during normalisation, we need both the new type
1160 variable *and* the coercion. We could conjure up a new VarEnv with just this
1161 property, but a usable substitution environment already exists:
1162 LiftingContexts from the liftCoSubst family of functions, defined in Coercion.
1163 A LiftingContext maps a type variable to a coercion and a coercion variable to
1164 a pair of coercions. Let's ignore coercion variables for now. Because the
1165 coercion a type variable maps to contains the destination type (via
1166 coercionKind), we don't need to store that destination type separately. Thus,
1167 a LiftingContext has what we need: a map from type variables to (Coercion,
1168 Type) pairs.
1169
1170 We also benefit because we can piggyback on the liftCoSubstVarBndr function to
1171 deal with binders. However, I had to modify that function to work with this
1172 application. Thus, we now have liftCoSubstVarBndrCallback, which takes
1173 a function used to process the kind of the binder. We don't wish
1174 to lift the kind, but instead normalise it. So, we pass in a callback function
1175 that processes the kind of the binder.
1176
1177 After that brilliant explanation of all this, I'm sure you've forgotten the
1178 dangling reference to coercion variables. What do we do with those? Nothing at
1179 all. The point of normalising types is to remove type family applications, but
1180 there's no sense in removing these from coercions. We would just get back a
1181 new coercion witnessing the equality between the same types as the original
1182 coercion. Because coercions are irrelevant anyway, there is no point in doing
1183 this. So, whenever we encounter a coercion, we just say that it won't change.
1184 That's what the CoercionTy case is doing within normalise_type.
1185
1186 -}
1187
1188 topNormaliseType :: FamInstEnvs -> Type -> Type
1189 topNormaliseType env ty = case topNormaliseType_maybe env ty of
1190 Just (_co, ty') -> ty'
1191 Nothing -> ty
1192
1193 topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
1194
1195 -- ^ Get rid of *outermost* (or toplevel)
1196 -- * type function redex
1197 -- * data family redex
1198 -- * newtypes
1199 -- returning an appropriate Representational coercion. Specifically, if
1200 -- topNormaliseType_maybe env ty = Maybe (co, ty')
1201 -- then
1202 -- (a) co :: ty ~R ty'
1203 -- (b) ty' is not a newtype, and is not a type-family or data-family redex
1204 --
1205 -- However, ty' can be something like (Maybe (F ty)), where
1206 -- (F ty) is a redex.
1207 --
1208 -- Its a bit like Type.repType, but handles type families too
1209
1210 topNormaliseType_maybe env ty
1211 = topNormaliseTypeX_maybe stepper ty
1212 where
1213 stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
1214
1215 tyFamStepper rec_nts tc tys -- Try to step a type/data familiy
1216 = let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
1217 -- NB: It's OK to use normaliseTcArgs here instead of
1218 -- normalise_tc_args (which takes the LiftingContext described
1219 -- in Note [Normalising types]) because the reduceTyFamApp below
1220 -- works only at top level. We'll never recur in this function
1221 -- after reducing the kind of a bound tyvar.
1222
1223 case reduceTyFamApp_maybe env Representational tc ntys of
1224 Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
1225 _ -> NS_Done
1226
1227 ---------------
1228 normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
1229 -- See comments on normaliseType for the arguments of this function
1230 normaliseTcApp env role tc tys
1231 = initNormM env role (tyCoVarsOfTypes tys) $
1232 normalise_tc_app tc tys
1233
1234 -- See Note [Normalising types] about the LiftingContext
1235 normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type)
1236 normalise_tc_app tc tys
1237 = do { (args_co, ntys) <- normalise_tc_args tc tys
1238 ; case expandSynTyCon_maybe tc ntys of
1239 { Just (tenv, rhs, ntys') ->
1240 do { (co2, ninst_rhs)
1241 <- normalise_type (substTy (mkTvSubstPrs tenv) rhs)
1242 ; return $
1243 if isReflCo co2
1244 then (args_co, mkTyConApp tc ntys)
1245 else (args_co `mkTransCo` co2, mkAppTys ninst_rhs ntys') }
1246 ; Nothing ->
1247 do { env <- getEnv
1248 ; role <- getRole
1249 ; case reduceTyFamApp_maybe env role tc ntys of
1250 Just (first_co, ty')
1251 -> do { (rest_co,nty) <- normalise_type ty'
1252 ; return ( args_co `mkTransCo` first_co `mkTransCo` rest_co
1253 , nty ) }
1254 _ -> -- No unique matching family instance exists;
1255 -- we do not do anything
1256 return (args_co, mkTyConApp tc ntys) }}}
1257
1258 ---------------
1259 -- | Normalise arguments to a tycon
1260 normaliseTcArgs :: FamInstEnvs -- ^ env't with family instances
1261 -> Role -- ^ desired role of output coercion
1262 -> TyCon -- ^ tc
1263 -> [Type] -- ^ tys
1264 -> (Coercion, [Type]) -- ^ co :: tc tys ~ tc new_tys
1265 normaliseTcArgs env role tc tys
1266 = initNormM env role (tyCoVarsOfTypes tys) $
1267 normalise_tc_args tc tys
1268
1269 normalise_tc_args :: TyCon -> [Type] -- tc tys
1270 -> NormM (Coercion, [Type]) -- (co, new_tys), where
1271 -- co :: tc tys ~ tc new_tys
1272 normalise_tc_args tc tys
1273 = do { role <- getRole
1274 ; (cois, ntys) <- zipWithAndUnzipM normalise_type_role
1275 tys (tyConRolesX role tc)
1276 ; return (mkTyConAppCo role tc cois, ntys) }
1277 where
1278 normalise_type_role ty r = withRole r $ normalise_type ty
1279
1280 ---------------
1281 normaliseType :: FamInstEnvs
1282 -> Role -- desired role of coercion
1283 -> Type -> (Coercion, Type)
1284 normaliseType env role ty
1285 = initNormM env role (tyCoVarsOfType ty) $ normalise_type ty
1286
1287 normalise_type :: Type -- old type
1288 -> NormM (Coercion, Type) -- (coercion,new type), where
1289 -- co :: old-type ~ new_type
1290 -- Normalise the input type, by eliminating *all* type-function redexes
1291 -- but *not* newtypes (which are visible to the programmer)
1292 -- Returns with Refl if nothing happens
1293 -- Does nothing to newtypes
1294 -- The returned coercion *must* be *homogeneous*
1295 -- See Note [Normalising types]
1296 -- Try to not to disturb type synonyms if possible
1297
1298 normalise_type
1299 = go
1300 where
1301 go (TyConApp tc tys) = normalise_tc_app tc tys
1302 go ty@(LitTy {}) = do { r <- getRole
1303 ; return (mkReflCo r ty, ty) }
1304 go (AppTy ty1 ty2)
1305 = do { (co, nty1) <- go ty1
1306 ; (arg, nty2) <- withRole Nominal $ go ty2
1307 ; return (mkAppCo co arg, mkAppTy nty1 nty2) }
1308 go (ForAllTy (Anon ty1) ty2)
1309 = do { (co1, nty1) <- go ty1
1310 ; (co2, nty2) <- go ty2
1311 ; r <- getRole
1312 ; return (mkFunCo r co1 co2, mkFunTy nty1 nty2) }
1313 go (ForAllTy (Named tyvar vis) ty)
1314 = do { (lc', tv', h, ki') <- normalise_tyvar_bndr tyvar
1315 ; (co, nty) <- withLC lc' $ normalise_type ty
1316 ; let tv2 = setTyVarKind tv' ki'
1317 ; return (mkForAllCo tv' h co, mkNamedForAllTy tv2 vis nty) }
1318 go (TyVarTy tv) = normalise_tyvar tv
1319 go (CastTy ty co)
1320 = do { (nco, nty) <- go ty
1321 ; lc <- getLC
1322 ; let co' = substRightCo lc co
1323 ; return (castCoercionKind nco co co', mkCastTy nty co') }
1324 go (CoercionTy co)
1325 = do { lc <- getLC
1326 ; r <- getRole
1327 ; let right_co = substRightCo lc co
1328 ; return ( mkProofIrrelCo r
1329 (liftCoSubst Nominal lc (coercionType co))
1330 co right_co
1331 , mkCoercionTy right_co ) }
1332
1333 normalise_tyvar :: TyVar -> NormM (Coercion, Type)
1334 normalise_tyvar tv
1335 = ASSERT( isTyVar tv )
1336 do { lc <- getLC
1337 ; r <- getRole
1338 ; return $ case liftCoSubstTyVar lc r tv of
1339 Just co -> (co, pSnd $ coercionKind co)
1340 Nothing -> (mkReflCo r ty, ty) }
1341 where ty = mkTyVarTy tv
1342
1343 normalise_tyvar_bndr :: TyVar -> NormM (LiftingContext, TyVar, Coercion, Kind)
1344 normalise_tyvar_bndr tv
1345 = do { lc1 <- getLC
1346 ; env <- getEnv
1347 ; let callback lc ki = runNormM (normalise_type ki) env lc Nominal
1348 ; return $ liftCoSubstVarBndrCallback callback lc1 tv }
1349
1350 -- | a monad for the normalisation functions, reading 'FamInstEnvs',
1351 -- a 'LiftingContext', and a 'Role'.
1352 newtype NormM a = NormM { runNormM ::
1353 FamInstEnvs -> LiftingContext -> Role -> a }
1354
1355 initNormM :: FamInstEnvs -> Role
1356 -> TyCoVarSet -- the in-scope variables
1357 -> NormM a -> a
1358 initNormM env role vars (NormM thing_inside)
1359 = thing_inside env lc role
1360 where
1361 in_scope = mkInScopeSet vars
1362 lc = emptyLiftingContext in_scope
1363
1364 getRole :: NormM Role
1365 getRole = NormM (\ _ _ r -> r)
1366
1367 getLC :: NormM LiftingContext
1368 getLC = NormM (\ _ lc _ -> lc)
1369
1370 getEnv :: NormM FamInstEnvs
1371 getEnv = NormM (\ env _ _ -> env)
1372
1373 withRole :: Role -> NormM a -> NormM a
1374 withRole r thing = NormM $ \ envs lc _old_r -> runNormM thing envs lc r
1375
1376 withLC :: LiftingContext -> NormM a -> NormM a
1377 withLC lc thing = NormM $ \ envs _old_lc r -> runNormM thing envs lc r
1378
1379 instance Monad NormM where
1380 ma >>= fmb = NormM $ \env lc r ->
1381 let a = runNormM ma env lc r in
1382 runNormM (fmb a) env lc r
1383
1384 instance Functor NormM where
1385 fmap = liftM
1386 instance Applicative NormM where
1387 pure x = NormM $ \ _ _ _ -> x
1388 (<*>) = ap
1389
1390 {-
1391 ************************************************************************
1392 * *
1393 Flattening
1394 * *
1395 ************************************************************************
1396
1397 Note [Flattening]
1398 ~~~~~~~~~~~~~~~~~
1399 As described in "Closed type families with overlapping equations"
1400 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
1401 we need to flatten core types before unifying them, when checking for "surely-apart"
1402 against earlier equations of a closed type family.
1403 Flattening means replacing all top-level uses of type functions with
1404 fresh variables, *taking care to preserve sharing*. That is, the type
1405 (Either (F a b) (F a b)) should flatten to (Either c c), never (Either
1406 c d).
1407
1408 Here is a nice example of why it's all necessary:
1409
1410 type family F a b where
1411 F Int Bool = Char
1412 F a b = Double
1413 type family G a -- open, no instances
1414
1415 How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
1416 while the second equation does. But, before reducing, we must make sure that the
1417 target can never become (F Int Bool). Well, no matter what G Float becomes, it
1418 certainly won't become *both* Int and Bool, so indeed we're safe reducing
1419 (F (G Float) (G Float)) to Double.
1420
1421 This is necessary not only to get more reductions (which we might be
1422 willing to give up on), but for substitutivity. If we have (F x x), we
1423 can see that (F x x) can reduce to Double. So, it had better be the
1424 case that (F blah blah) can reduce to Double, no matter what (blah)
1425 is! Flattening as done below ensures this.
1426
1427 flattenTys is defined here because of module dependencies.
1428 -}
1429
1430 data FlattenEnv = FlattenEnv { fe_type_map :: TypeMap TyVar
1431 , fe_subst :: TCvSubst }
1432
1433 emptyFlattenEnv :: InScopeSet -> FlattenEnv
1434 emptyFlattenEnv in_scope
1435 = FlattenEnv { fe_type_map = emptyTypeMap
1436 , fe_subst = mkEmptyTCvSubst in_scope }
1437
1438 -- See Note [Flattening]
1439 flattenTys :: InScopeSet -> [Type] -> [Type]
1440 flattenTys in_scope tys = snd $ coreFlattenTys env tys
1441 where
1442 -- when we hit a type function, we replace it with a fresh variable
1443 -- but, we need to make sure that this fresh variable isn't mentioned
1444 -- *anywhere* in the types we're flattening, even if locally-bound in
1445 -- a forall. That way, we can ensure consistency both within and outside
1446 -- of that forall.
1447 all_in_scope = in_scope `extendInScopeSetSet` allTyVarsInTys tys
1448 env = emptyFlattenEnv all_in_scope
1449
1450 coreFlattenTys :: FlattenEnv -> [Type] -> (FlattenEnv, [Type])
1451 coreFlattenTys = go []
1452 where
1453 go rtys env [] = (env, reverse rtys)
1454 go rtys env (ty : tys)
1455 = let (env', ty') = coreFlattenTy env ty in
1456 go (ty' : rtys) env' tys
1457
1458 coreFlattenTy :: FlattenEnv -> Type -> (FlattenEnv, Type)
1459 coreFlattenTy = go
1460 where
1461 go env ty | Just ty' <- coreView ty = go env ty'
1462
1463 go env (TyVarTy tv) = (env, substTyVar (fe_subst env) tv)
1464 go env (AppTy ty1 ty2) = let (env1, ty1') = go env ty1
1465 (env2, ty2') = go env1 ty2 in
1466 (env2, AppTy ty1' ty2')
1467 go env (TyConApp tc tys)
1468 -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
1469 -- which are generative and thus can be preserved during flattening
1470 | not (isGenerativeTyCon tc Nominal)
1471 = let (env', tv) = coreFlattenTyFamApp env tc tys in
1472 (env', mkTyVarTy tv)
1473
1474 | otherwise
1475 = let (env', tys') = coreFlattenTys env tys in
1476 (env', mkTyConApp tc tys')
1477
1478 go env (ForAllTy (Anon ty1) ty2) = let (env1, ty1') = go env ty1
1479 (env2, ty2') = go env1 ty2 in
1480 (env2, mkFunTy ty1' ty2')
1481
1482 go env (ForAllTy (Named tv vis) ty)
1483 = let (env1, tv') = coreFlattenVarBndr env tv
1484 (env2, ty') = go env1 ty in
1485 (env2, mkNamedForAllTy tv' vis ty')
1486
1487 go env ty@(LitTy {}) = (env, ty)
1488
1489 go env (CastTy ty co) = let (env1, ty') = go env ty
1490 (env2, co') = coreFlattenCo env1 co in
1491 (env2, CastTy ty' co')
1492
1493 go env (CoercionTy co) = let (env', co') = coreFlattenCo env co in
1494 (env', CoercionTy co')
1495
1496 -- when flattening, we don't care about the contents of coercions.
1497 -- so, just return a fresh variable of the right (flattened) type
1498 coreFlattenCo :: FlattenEnv -> Coercion -> (FlattenEnv, Coercion)
1499 coreFlattenCo env co
1500 = (env2, mkCoVarCo covar)
1501 where
1502 (env1, kind') = coreFlattenTy env (coercionType co)
1503 fresh_name = mkFlattenFreshCoName
1504 subst1 = fe_subst env1
1505 in_scope = getTCvInScope subst1
1506 covar = uniqAway in_scope (mkCoVar fresh_name kind')
1507 env2 = env1 { fe_subst = subst1 `extendTCvInScope` covar }
1508
1509 coreFlattenVarBndr :: FlattenEnv -> TyVar -> (FlattenEnv, TyVar)
1510 coreFlattenVarBndr env tv
1511 | kind' `eqType` kind
1512 = ( env { fe_subst = extendTvSubst old_subst tv (mkTyVarTy tv) }
1513 -- override any previous binding for tv
1514 , tv)
1515
1516 | otherwise
1517 = let new_tv = uniqAway (getTCvInScope old_subst) (setTyVarKind tv kind')
1518 new_subst = extendTvSubstWithClone old_subst tv new_tv
1519 in
1520 (env' { fe_subst = new_subst }, new_tv)
1521 where
1522 kind = tyVarKind tv
1523 (env', kind') = coreFlattenTy env kind
1524 old_subst = fe_subst env
1525
1526 coreFlattenTyFamApp :: FlattenEnv
1527 -> TyCon -- type family tycon
1528 -> [Type] -- args
1529 -> (FlattenEnv, TyVar)
1530 coreFlattenTyFamApp env fam_tc fam_args
1531 = case lookupTypeMap type_map fam_ty of
1532 Just tv -> (env, tv)
1533 -- we need fresh variables here, but this is called far from
1534 -- any good source of uniques. So, we just use the fam_tc's unique
1535 -- and trust uniqAway to avoid clashes. Recall that the in_scope set
1536 -- contains *all* tyvars, even locally bound ones elsewhere in the
1537 -- overall type, so this really is fresh.
1538 Nothing -> let tyvar_name = mkFlattenFreshTyName fam_tc
1539 tv = uniqAway (getTCvInScope subst) $
1540 mkTyVar tyvar_name (typeKind fam_ty)
1541 env' = env { fe_type_map = extendTypeMap type_map fam_ty tv
1542 , fe_subst = extendTCvInScope subst tv }
1543 in (env', tv)
1544 where fam_ty = mkTyConApp fam_tc fam_args
1545 FlattenEnv { fe_type_map = type_map
1546 , fe_subst = subst } = env
1547
1548 -- | Get the set of all type variables mentioned anywhere in the list
1549 -- of types. These variables are not necessarily free.
1550 allTyVarsInTys :: [Type] -> VarSet
1551 allTyVarsInTys [] = emptyVarSet
1552 allTyVarsInTys (ty:tys) = allTyVarsInTy ty `unionVarSet` allTyVarsInTys tys
1553
1554 -- | Get the set of all type variables mentioned anywhere in a type.
1555 allTyVarsInTy :: Type -> VarSet
1556 allTyVarsInTy = go
1557 where
1558 go (TyVarTy tv) = unitVarSet tv
1559 go (AppTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1560 go (TyConApp _ tys) = allTyVarsInTys tys
1561 go (ForAllTy bndr ty) =
1562 caseBinder bndr (\tv -> unitVarSet tv) (const emptyVarSet)
1563 `unionVarSet` go (binderType bndr) `unionVarSet` go ty
1564 -- don't remove the tv from the set!
1565 go (LitTy {}) = emptyVarSet
1566 go (CastTy ty co) = go ty `unionVarSet` go_co co
1567 go (CoercionTy co) = go_co co
1568
1569 go_co (Refl _ ty) = go ty
1570 go_co (TyConAppCo _ _ args) = go_cos args
1571 go_co (AppCo co arg) = go_co co `unionVarSet` go_co arg
1572 go_co (ForAllCo tv h co)
1573 = unionVarSets [unitVarSet tv, go_co co, go_co h]
1574 go_co (CoVarCo cv) = unitVarSet cv
1575 go_co (AxiomInstCo _ _ cos) = go_cos cos
1576 go_co (UnivCo p _ t1 t2) = go_prov p `unionVarSet` go t1 `unionVarSet` go t2
1577 go_co (SymCo co) = go_co co
1578 go_co (TransCo c1 c2) = go_co c1 `unionVarSet` go_co c2
1579 go_co (NthCo _ co) = go_co co
1580 go_co (LRCo _ co) = go_co co
1581 go_co (InstCo co arg) = go_co co `unionVarSet` go_co arg
1582 go_co (CoherenceCo c1 c2) = go_co c1 `unionVarSet` go_co c2
1583 go_co (KindCo co) = go_co co
1584 go_co (SubCo co) = go_co co
1585 go_co (AxiomRuleCo _ cs) = go_cos cs
1586
1587 go_cos = foldr (unionVarSet . go_co) emptyVarSet
1588
1589 go_prov UnsafeCoerceProv = emptyVarSet
1590 go_prov (PhantomProv co) = go_co co
1591 go_prov (ProofIrrelProv co) = go_co co
1592 go_prov (PluginProv _) = emptyVarSet
1593 go_prov (HoleProv _) = emptyVarSet
1594
1595 mkFlattenFreshTyName :: Uniquable a => a -> Name
1596 mkFlattenFreshTyName unq
1597 = mkSysTvName (getUnique unq) (fsLit "flt")
1598
1599 mkFlattenFreshCoName :: Name
1600 mkFlattenFreshCoName
1601 = mkSystemVarName (deriveUnique eqPrimTyConKey 71) (fsLit "flc")