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