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