Merge branch 'master' of http://darcs.haskell.org/ghc
[ghc.git] / compiler / types / FamInstEnv.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 FamInstEnv: Type checked family instance declarations
6
7 \begin{code}
8 module FamInstEnv (
9         FamInst(..), FamFlavor(..), famInstAxiom,
10         famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
11         famInstLHS,
12         pprFamInst, pprFamInstHdr, pprFamInsts,
13         mkSynFamInst, mkDataFamInst, mkImportedFamInst,
14
15         FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
16         extendFamInstEnv, deleteFromFamInstEnv, extendFamInstEnvList,
17         identicalFamInst, famInstEnvElts, familyInstances,
18
19         lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvConflicts',
20
21         -- Normalisation
22         topNormaliseType, normaliseType, normaliseTcApp
23     ) where
24
25 #include "HsVersions.h"
26
27 import InstEnv
28 import Unify
29 import Type
30 import TypeRep
31 import TyCon
32 import Coercion
33 import VarSet
34 import VarEnv
35 import Name
36 import UniqFM
37 import Outputable
38 import Maybes
39 import Util
40 import FastString
41 \end{code}
42
43
44 %************************************************************************
45 %*                                                                      *
46 \subsection{Type checked family instance heads}
47 %*                                                                      *
48 %************************************************************************
49
50 Note [FamInsts and CoAxioms]
51 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
52 * CoAxioms and FamInsts are just like
53   DFunIds  and ClsInsts
54
55 * A CoAxiom is a System-FC thing: it can relate any two types
56
57 * A FamInst is a Haskell source-language thing, corresponding
58   to a type/data family instance declaration.
59     - The FamInst contains a CoAxiom, which is the evidence
60       for the instance
61
62     - The LHS of the CoAxiom is always of form F ty1 .. tyn
63       where F is a type family
64
65
66 \begin{code}
67 data FamInst  -- See Note [FamInsts and CoAxioms]
68   = FamInst { fi_axiom  :: CoAxiom      -- The new coercion axiom introduced
69                                         -- by this family instance
70             , fi_flavor :: FamFlavor
71
72             -- Everything below here is a redundant,
73             -- cached version of the two things above
74             , fi_fam   :: Name          -- Family name
75                 -- INVARIANT: fi_fam = name of fi_fam_tc
76
77                 -- Used for "rough matching"; same idea as for class instances
78                 -- See Note [Rough-match field] in InstEnv
79             , fi_tcs   :: [Maybe Name]  -- Top of type args
80                 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
81
82                 -- Used for "proper matching"; ditto
83             , fi_tvs    :: TyVarSet     -- Template tyvars for full match
84             , fi_fam_tc :: TyCon        -- Family tycon
85             , fi_tys    :: [Type]       --   and its arg types
86                 -- INVARIANT: fi_tvs = coAxiomTyVars fi_axiom
87                 --            (fi_fam_tc, fi_tys) = coAxiomSplitLHS fi_axiom
88             }
89
90 data FamFlavor
91   = SynFamilyInst         -- A synonym family
92   | DataFamilyInst TyCon  -- A data family, with its representation TyCon
93 \end{code}
94
95
96 \begin{code}
97 -- Obtain the axiom of a family instance
98 famInstAxiom :: FamInst -> CoAxiom
99 famInstAxiom = fi_axiom
100
101 famInstLHS :: FamInst -> (TyCon, [Type])
102 famInstLHS (FamInst { fi_fam_tc = tc, fi_tys = tys }) = (tc, tys)
103
104 -- Return the representation TyCons introduced by data family instances, if any
105 famInstsRepTyCons :: [FamInst] -> [TyCon]
106 famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis]
107
108 -- Extracts the TyCon for this *data* (or newtype) instance
109 famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
110 famInstRepTyCon_maybe fi
111   = case fi_flavor fi of
112        DataFamilyInst tycon -> Just tycon
113        SynFamilyInst        -> Nothing
114
115 dataFamInstRepTyCon :: FamInst -> TyCon
116 dataFamInstRepTyCon fi
117   = case fi_flavor fi of
118        DataFamilyInst tycon -> tycon
119        SynFamilyInst        -> pprPanic "dataFamInstRepTyCon" (ppr fi)
120 \end{code}
121
122 \begin{code}
123 instance NamedThing FamInst where
124    getName = coAxiomName . fi_axiom
125
126 instance Outputable FamInst where
127    ppr = pprFamInst
128
129 -- Prints the FamInst as a family instance declaration
130 pprFamInst :: FamInst -> SDoc
131 pprFamInst famInst
132   = hang (pprFamInstHdr famInst)
133        2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> ppr ax)
134                , ifPprDebug (ptext (sLit "RHS:") <+> ppr (coAxiomRHS ax))
135                , ptext (sLit "--") <+> pprDefinedAt (getName famInst)])
136   where
137     ax = fi_axiom famInst
138
139 pprFamInstHdr :: FamInst -> SDoc
140 pprFamInstHdr (FamInst {fi_axiom = axiom, fi_flavor = flavor})
141   = pprTyConSort <+> pp_instance <+> pprHead
142   where
143     (fam_tc, tys) = coAxiomSplitLHS axiom
144
145     -- For *associated* types, say "type T Int = blah"
146     -- For *top level* type instances, say "type instance T Int = blah"
147     pp_instance
148       | isTyConAssoc fam_tc = empty
149       | otherwise           = ptext (sLit "instance")
150
151     pprHead = sep [ ifPprDebug (ptext (sLit "forall")
152                        <+> pprTvBndrs (coAxiomTyVars axiom))
153                   , pprTypeApp fam_tc tys ]
154     pprTyConSort = case flavor of
155                      SynFamilyInst        -> ptext (sLit "type")
156                      DataFamilyInst tycon
157                        | isDataTyCon     tycon -> ptext (sLit "data")
158                        | isNewTyCon      tycon -> ptext (sLit "newtype")
159                        | isAbstractTyCon tycon -> ptext (sLit "data")
160                        | otherwise             -> ptext (sLit "WEIRD") <+> ppr tycon
161
162 pprFamInsts :: [FamInst] -> SDoc
163 pprFamInsts finsts = vcat (map pprFamInst finsts)
164
165 -- | Create a coercion identifying a @type@ family instance.
166 -- It has the form @Co tvs :: F ts ~ R@, where @Co@ is
167 -- the coercion constructor built here, @F@ the family tycon and @R@ the
168 -- right-hand side of the type family instance.
169 mkSynFamInst :: Name       -- ^ Unique name for the coercion tycon
170              -> [TyVar]    -- ^ Type parameters of the coercion (@tvs@)
171              -> TyCon      -- ^ Family tycon (@F@)
172              -> [Type]     -- ^ Type instance (@ts@)
173              -> Type       -- ^ Representation tycon (@R@)
174              -> FamInst
175 mkSynFamInst name tvs fam_tc inst_tys rep_ty
176   = FamInst { fi_fam    = tyConName fam_tc,
177               fi_fam_tc = fam_tc,
178               fi_tcs    = roughMatchTcs inst_tys,
179               fi_tvs    = mkVarSet tvs,
180               fi_tys    = inst_tys,
181               fi_flavor = SynFamilyInst,
182               fi_axiom  = axiom }
183   where
184     axiom = CoAxiom { co_ax_unique   = nameUnique name
185                     , co_ax_name     = name
186                     , co_ax_implicit = False
187                     , co_ax_tvs      = tvs
188                     , co_ax_lhs      = mkTyConApp fam_tc inst_tys
189                     , co_ax_rhs      = rep_ty }
190
191 -- | Create a coercion identifying a @data@ or @newtype@ representation type
192 -- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@,
193 -- where @Co@ is the coercion constructor built here, @F@ the family tycon
194 -- and @R@ the (derived) representation tycon.
195 mkDataFamInst :: Name         -- ^ Unique name for the coercion tycon
196               -> [TyVar]      -- ^ Type parameters of the coercion (@tvs@)
197               -> TyCon        -- ^ Family tycon (@F@)
198               -> [Type]       -- ^ Type instance (@ts@)
199               -> TyCon        -- ^ Representation tycon (@R@)
200               -> FamInst
201 mkDataFamInst name tvs fam_tc inst_tys rep_tc
202   = FamInst { fi_fam    = tyConName fam_tc,
203               fi_fam_tc = fam_tc,
204               fi_tcs    = roughMatchTcs inst_tys,
205               fi_tvs    = mkVarSet tvs,
206               fi_tys    = inst_tys,
207               fi_flavor = DataFamilyInst rep_tc,
208               fi_axiom  = axiom }
209   where
210     axiom = CoAxiom { co_ax_unique   = nameUnique name
211                     , co_ax_name     = name
212                     , co_ax_implicit = False
213                     , co_ax_tvs      = tvs
214                     , co_ax_lhs      = mkTyConApp fam_tc inst_tys
215                     , co_ax_rhs      = mkTyConApp rep_tc (mkTyVarTys tvs) }
216
217 -- Make a family instance representation from the information found in an
218 -- interface file.  In particular, we get the rough match info from the iface
219 -- (instead of computing it here).
220 mkImportedFamInst :: Name               -- Name of the family
221                   -> [Maybe Name]       -- Rough match info
222                   -> CoAxiom            -- Axiom introduced
223                   -> FamInst            -- Resulting family instance
224 mkImportedFamInst fam mb_tcs axiom
225   = FamInst {
226       fi_fam    = fam,
227       fi_fam_tc = fam_tc,
228       fi_tcs    = mb_tcs,
229       fi_tvs    = mkVarSet . coAxiomTyVars $ axiom,
230       fi_tys    = tys,
231       fi_axiom  = axiom,
232       fi_flavor = flavor }
233   where
234      (fam_tc, tys) = coAxiomSplitLHS axiom
235
236          -- Derive the flavor for an imported FamInst rather disgustingly
237          -- Maybe we should store it in the IfaceFamInst?
238      flavor = case splitTyConApp_maybe (coAxiomRHS axiom) of
239                 Just (tc, _)
240                   | Just ax' <- tyConFamilyCoercion_maybe tc
241                   , ax' == axiom
242                   -> DataFamilyInst tc
243                 _ -> SynFamilyInst
244 \end{code}
245
246
247
248 %************************************************************************
249 %*                                                                      *
250                 FamInstEnv
251 %*                                                                      *
252 %************************************************************************
253
254 Note [FamInstEnv]
255 ~~~~~~~~~~~~~~~~~~~~~
256 A FamInstEnv maps a family name to the list of known instances for that family.
257
258 The same FamInstEnv includes both 'data family' and 'type family' instances.
259 Type families are reduced during type inference, but not data families;
260 the user explains when to use a data family instance by using contructors
261 and pattern matching.
262
263 Neverthless it is still useful to have data families in the FamInstEnv:
264
265  - For finding overlaps and conflicts
266
267  - For finding the representation type...see FamInstEnv.topNormaliseType
268    and its call site in Simplify
269
270  - In standalone deriving instance Eq (T [Int]) we need to find the
271    representation type for T [Int]
272
273 \begin{code}
274 type FamInstEnv = UniqFM FamilyInstEnv  -- Maps a family to its instances
275      -- See Note [FamInstEnv]
276
277 type FamInstEnvs = (FamInstEnv, FamInstEnv)
278      -- External package inst-env, Home-package inst-env
279
280 data FamilyInstEnv
281   = FamIE [FamInst]     -- The instances for a particular family, in any order
282           Bool          -- True <=> there is an instance of form T a b c
283                         --      If *not* then the common case of looking up
284                         --      (T a b c) can fail immediately
285
286 instance Outputable FamilyInstEnv where
287   ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs)
288
289 -- INVARIANTS:
290 --  * The fs_tvs are distinct in each FamInst
291 --      of a range value of the map (so we can safely unify them)
292
293 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
294 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
295
296 emptyFamInstEnv :: FamInstEnv
297 emptyFamInstEnv = emptyUFM
298
299 famInstEnvElts :: FamInstEnv -> [FamInst]
300 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
301
302 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
303 familyInstances (pkg_fie, home_fie) fam
304   = get home_fie ++ get pkg_fie
305   where
306     get env = case lookupUFM env fam of
307                 Just (FamIE insts _) -> insts
308                 Nothing              -> []
309
310 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
311 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
312
313 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
314 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
315   = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
316   where
317     add (FamIE items tyvar) _ = FamIE (ins_item:items)
318                                       (ins_tyvar || tyvar)
319     ins_tyvar = not (any isJust mb_tcs)
320
321 deleteFromFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
322 deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm})
323  = adjustUFM adjust inst_env fam_nm
324  where
325    adjust :: FamilyInstEnv -> FamilyInstEnv
326    adjust (FamIE items tyvars)
327      = FamIE (filterOut (identicalFamInst fam_inst) items) tyvars
328
329 identicalFamInst :: FamInst -> FamInst -> Bool
330 -- Same LHS, *and* the instance is defined in the same module
331 -- Used for overriding in GHCi
332 identicalFamInst (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
333   =  nameModule (coAxiomName ax1) == nameModule (coAxiomName ax2)
334   && eqTypeX rn_env (coAxiomLHS ax1) (coAxiomLHS ax2)
335   where
336      tvs1 = coAxiomTyVars ax1
337      tvs2 = coAxiomTyVars ax2
338      rn_env = ASSERT( equalLength tvs1 tvs2 )
339               rnBndrs2 (mkRnEnv2 emptyInScopeSet) tvs1 tvs2
340
341 \end{code}
342
343 %************************************************************************
344 %*                                                                      *
345                 Looking up a family instance
346 %*                                                                      *
347 %************************************************************************
348
349 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
350 Multiple matches are only possible in case of type families (not data
351 families), and then, it doesn't matter which match we choose (as the
352 instances are guaranteed confluent).
353
354 We return the matching family instances and the type instance at which it
355 matches.  For example, if we lookup 'T [Int]' and have a family instance
356
357   data instance T [a] = ..
358
359 desugared to
360
361   data :R42T a = ..
362   coe :Co:R42T a :: T [a] ~ :R42T a
363
364 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
365
366 \begin{code}
367 type FamInstMatch = (FamInst, [Type])           -- Matching type instance
368   -- See Note [Over-saturated matches]
369
370 lookupFamInstEnv
371     :: FamInstEnvs
372     -> TyCon -> [Type]          -- What we are looking for
373     -> [FamInstMatch]           -- Successful matches
374 -- Precondition: the tycon is saturated (or over-saturated)
375
376 lookupFamInstEnv
377    = lookup_fam_inst_env match True
378    where
379      match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
380
381 lookupFamInstEnvConflicts
382     :: FamInstEnvs
383     -> FamInst          -- Putative new instance
384     -> [TyVar]          -- Unique tyvars, matching arity of FamInst
385     -> [FamInstMatch]   -- Conflicting matches
386 -- E.g. when we are about to add
387 --    f : type instance F [a] = a->a
388 -- we do (lookupFamInstConflicts f [b])
389 -- to find conflicting matches
390 -- The skolem tyvars are needed because we don't have a
391 -- unique supply to hand
392 --
393 -- Precondition: the tycon is saturated (or over-saturated)
394
395 lookupFamInstEnvConflicts envs fam_inst skol_tvs
396   = lookup_fam_inst_env my_unify False envs fam tys1
397   where
398     inst_axiom = famInstAxiom fam_inst
399     (fam, tys) = famInstLHS fam_inst
400     skol_tys   = mkTyVarTys skol_tvs
401     ax_tvs     = coAxiomTyVars inst_axiom
402     tys1       = ASSERT2( length ax_tvs == length skol_tys, ppr inst_axiom $$ ppr skol_tys )
403                  substTys (zipTopTvSubst ax_tvs skol_tys) tys
404         -- In example above,   fam tys' = F [b]
405
406     my_unify old_fam_inst tpl_tvs tpl_tys match_tys
407        = ASSERT2( tyVarsOfTypes tys1 `disjointVarSet` tpl_tvs,
408                   (ppr fam <+> ppr tys1) $$
409                   (ppr tpl_tvs <+> ppr tpl_tys) )
410                 -- Unification will break badly if the variables overlap
411                 -- They shouldn't because we allocate separate uniques for them
412          case tcUnifyTys instanceBindFun tpl_tys match_tys of
413               Just subst | conflicting old_fam_inst subst -> Just subst
414               _other                                      -> Nothing
415
416       -- Note [Family instance overlap conflicts]
417     conflicting old_fam_inst subst
418       | isAlgTyCon fam = True
419       | otherwise      = not (old_rhs `eqType` new_rhs)
420       where
421         old_axiom = famInstAxiom old_fam_inst
422         old_tvs   = coAxiomTyVars old_axiom
423         old_rhs   = mkAxInstRHS old_axiom  (substTyVars subst old_tvs)
424         new_rhs   = mkAxInstRHS inst_axiom (substTyVars subst skol_tvs)
425
426 -- This variant is called when we want to check if the conflict is only in the
427 -- home environment (see FamInst.addLocalFamInst)
428 lookupFamInstEnvConflicts' :: FamInstEnv -> FamInst -> [TyVar] -> [FamInstMatch]
429 lookupFamInstEnvConflicts' env fam_inst skol_tvs
430   = lookupFamInstEnvConflicts (emptyFamInstEnv, env) fam_inst skol_tvs
431 \end{code}
432
433 Note [Family instance overlap conflicts]
434 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
435 - In the case of data family instances, any overlap is fundamentally a
436   conflict (as these instances imply injective type mappings).
437
438 - In the case of type family instances, overlap is admitted as long as
439   the right-hand sides of the overlapping rules coincide under the
440   overlap substitution.  eg
441        type instance F a Int = a
442        type instance F Int b = b
443   These two overlap on (F Int Int) but then both RHSs are Int,
444   so all is well. We require that they are syntactically equal;
445   anything else would be difficult to test for at this stage.
446
447
448 While @lookupFamInstEnv@ uses a one-way match, the next function
449 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification).  This is
450 needed to check for overlapping instances.
451
452 For class instances, these two variants of lookup are combined into one
453 function (cf, @InstEnv@).  We don't do that for family instances as the
454 results of matching and unification are used in two different contexts.
455 Moreover, matching is the wildly more frequently used operation in the case of
456 indexed synonyms and we don't want to slow that down by needless unification.
457
458 \begin{code}
459 ------------------------------------------------------------
460 -- Might be a one-way match or a unifier
461 type MatchFun =  FamInst                -- The FamInst template
462               -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
463               -> [Type]                 -- Target to match against
464               -> Maybe TvSubst
465
466 type OneSidedMatch = Bool     -- Are optimisations that are only valid for
467                               -- one sided matches allowed?
468
469 lookup_fam_inst_env'          -- The worker, local to this module
470     :: MatchFun
471     -> OneSidedMatch
472     -> FamInstEnv
473     -> TyCon -> [Type]          -- What we are looking for
474     -> [FamInstMatch]           -- Successful matches
475 lookup_fam_inst_env' match_fun one_sided ie fam tys
476   | not (isFamilyTyCon fam)
477   = []
478   | otherwise
479   = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys )      -- Family type applications must be saturated
480     lookup ie
481   where
482     -- See Note [Over-saturated matches]
483     arity = tyConArity fam
484     n_tys = length tys
485     extra_tys = drop arity tys
486     (match_tys, add_extra_tys)
487        | arity < n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
488        | otherwise     = (tys,            \res_tys -> res_tys)
489          -- The second case is the common one, hence functional representation
490
491     --------------
492     rough_tcs = roughMatchTcs match_tys
493     all_tvs   = all isNothing rough_tcs && one_sided
494
495     --------------
496     lookup env = case lookupUFM env fam of
497                    Nothing -> []        -- No instances for this class
498                    Just (FamIE insts has_tv_insts)
499                        -- Short cut for common case:
500                        --   The thing we are looking up is of form (C a
501                        --   b c), and the FamIE has no instances of
502                        --   that form, so don't bother to search
503                      | all_tvs && not has_tv_insts -> []
504                      | otherwise                   -> find insts
505
506     --------------
507     find [] = []
508     find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
509                           fi_tys = tpl_tys, fi_axiom = axiom }) : rest)
510         -- Fast check for no match, uses the "rough match" fields
511       | instanceCantMatch rough_tcs mb_tcs
512       = find rest
513
514         -- Proper check
515       | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
516       = (item, add_extra_tys $ substTyVars subst (coAxiomTyVars axiom)) : find rest
517
518         -- No match => try next
519       | otherwise
520       = find rest
521 -- Precondition: the tycon is saturated (or over-saturated)
522
523 lookup_fam_inst_env           -- The worker, local to this module
524     :: MatchFun
525     -> OneSidedMatch
526     -> FamInstEnvs
527     -> TyCon -> [Type]          -- What we are looking for
528     -> [FamInstMatch]           -- Successful matches
529
530 -- Precondition: the tycon is saturated (or over-saturated)
531
532 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys =
533     lookup_fam_inst_env' match_fun one_sided home_ie fam tys ++
534     lookup_fam_inst_env' match_fun one_sided pkg_ie  fam tys
535
536 \end{code}
537
538 Note [Over-saturated matches]
539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
540 It's ok to look up an over-saturated type constructor.  E.g.
541      type family F a :: * -> *
542      type instance F (a,b) = Either (a->b)
543
544 The type instance gives rise to a newtype TyCon (at a higher kind
545 which you can't do in Haskell!):
546      newtype FPair a b = FP (Either (a->b))
547
548 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
549      (FPair, [Int,Bool,Char])
550
551 The "extra" type argument [Char] just stays on the end.
552
553
554
555
556 %************************************************************************
557 %*                                                                      *
558                 Looking up a family instance
559 %*                                                                      *
560 %************************************************************************
561
562 \begin{code}
563 topNormaliseType :: FamInstEnvs
564                  -> Type
565                  -> Maybe (Coercion, Type)
566
567 -- Get rid of *outermost* (or toplevel)
568 --      * type functions
569 --      * newtypes
570 -- using appropriate coercions.
571 -- By "outer" we mean that toplevelNormaliseType guarantees to return
572 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
573 -- outermost form.  It *can* return something like (Maybe (F ty)), where
574 -- (F ty) is a redex.
575
576 -- Its a bit like Type.repType, but handles type families too
577
578 topNormaliseType env ty
579   = go [] ty
580   where
581     go :: [TyCon] -> Type -> Maybe (Coercion, Type)
582     go rec_nts ty | Just ty' <- coreView ty     -- Expand synonyms
583         = go rec_nts ty'
584
585     go rec_nts (TyConApp tc tys)
586         | isNewTyCon tc         -- Expand newtypes
587         = if tc `elem` rec_nts  -- See Note [Expanding newtypes] in Type.lhs
588           then Nothing
589           else let nt_co = mkAxInstCo (newTyConCo tc) tys
590                in add_co nt_co rec_nts' nt_rhs
591
592         | isFamilyTyCon tc              -- Expand open tycons
593         , (co, ty) <- normaliseTcApp env tc tys
594                 -- Note that normaliseType fully normalises 'tys',
595                 -- It has do to so to be sure that nested calls like
596                 --    F (G Int)
597                 -- are correctly top-normalised
598         , not (isReflCo co)
599         = add_co co rec_nts ty
600         where
601           nt_rhs = newTyConInstRhs tc tys
602           rec_nts' | isRecursiveTyCon tc = tc:rec_nts
603                    | otherwise           = rec_nts
604
605     go _ _ = Nothing
606
607     add_co co rec_nts ty
608         = case go rec_nts ty of
609                 Nothing         -> Just (co, ty)
610                 Just (co', ty') -> Just (mkTransCo co co', ty')
611
612
613 ---------------
614 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
615 normaliseTcApp env tc tys
616   | isFamilyTyCon tc
617   , tyConArity tc <= length tys    -- Unsaturated data families are possible
618   , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys
619   = let    -- A matching family instance exists
620         ax              = famInstAxiom fam_inst
621         co              = mkAxInstCo  ax inst_tys
622         rhs             = mkAxInstRHS ax inst_tys
623         first_coi       = mkTransCo tycon_coi co
624         (rest_coi,nty)  = normaliseType env rhs
625         fix_coi         = mkTransCo first_coi rest_coi
626     in
627     (fix_coi, nty)
628
629   | otherwise   -- No unique matching family instance exists;
630                 -- we do not do anything
631   = (tycon_coi, TyConApp tc ntys)
632
633   where
634         -- Normalise the arg types so that they'll match
635         -- when we lookup in in the instance envt
636     (cois, ntys) = mapAndUnzip (normaliseType env) tys
637     tycon_coi    = mkTyConAppCo tc cois
638
639 ---------------
640 normaliseType :: FamInstEnvs            -- environment with family instances
641               -> Type                   -- old type
642               -> (Coercion, Type)       -- (coercion,new type), where
643                                         -- co :: old-type ~ new_type
644 -- Normalise the input type, by eliminating *all* type-function redexes
645 -- Returns with Refl if nothing happens
646
647 normaliseType env ty
648   | Just ty' <- coreView ty = normaliseType env ty'
649 normaliseType env (TyConApp tc tys)
650   = normaliseTcApp env tc tys
651 normaliseType _env ty@(LitTy {}) = (Refl ty, ty)
652 normaliseType env (AppTy ty1 ty2)
653   = let (coi1,nty1) = normaliseType env ty1
654         (coi2,nty2) = normaliseType env ty2
655     in  (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
656 normaliseType env (FunTy ty1 ty2)
657   = let (coi1,nty1) = normaliseType env ty1
658         (coi2,nty2) = normaliseType env ty2
659     in  (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
660 normaliseType env (ForAllTy tyvar ty1)
661   = let (coi,nty1) = normaliseType env ty1
662     in  (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
663 normaliseType _   ty@(TyVarTy _)
664   = (Refl ty,ty)
665 \end{code}