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