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