Mainly, rename LiteralTy to LitTy
[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, famInstTyVars,
17         famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon, 
18         famInstLHS,
19         pprFamInst, pprFamInstHdr, pprFamInsts, 
20         mkSynFamInst, mkDataFamInst, mkImportedFamInst,
21
22         FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, 
23         extendFamInstEnv, overwriteFamInstEnv, extendFamInstEnvList, 
24         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 Name
42 import UniqFM
43 import Outputable
44 import Maybes
45 import Util
46 import FastString
47 \end{code}
48
49
50 %************************************************************************
51 %*                                                                      *
52 \subsection{Type checked family instance heads}
53 %*                                                                      *
54 %************************************************************************
55
56 Note [FamInsts and CoAxioms]
57 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
58 * CoAxioms and FamInsts are just like
59   DFunIds  and ClsInsts
60
61 * A CoAxiom is a System-FC thing: it can relate any two types
62
63 * A FamInst is a Haskell source-language thing, corresponding
64   to a type/data family instance declaration.  
65     - The FamInst contains a CoAxiom, which is the evidence
66       for the instance
67
68     - The LHS of the CoAxiom is always of form F ty1 .. tyn
69       where F is a type family
70
71
72 \begin{code}
73 data FamInst  -- See Note [FamInsts and CoAxioms]
74   = FamInst { fi_axiom  :: CoAxiom      -- The new coercion axiom introduced
75                                         -- by this family instance
76             , fi_flavor :: FamFlavor
77
78             -- Everything below here is a redundant, 
79             -- cached version of the two things above
80             , fi_fam   :: Name          -- Family name
81                 -- INVARIANT: fi_fam = name of fi_fam_tc
82
83                 -- Used for "rough matching"; same idea as for class instances
84                 -- See Note [Rough-match field] in InstEnv
85             , fi_tcs   :: [Maybe Name]  -- Top of type args
86                 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
87
88                 -- Used for "proper matching"; ditto
89             , fi_tvs    :: TyVarSet     -- Template tyvars for full match
90             , fi_fam_tc :: TyCon        -- Family tycon
91             , fi_tys    :: [Type]       --   and its arg types
92                 -- INVARIANT: fi_tvs = coAxiomTyVars fi_axiom
93                 --            (fi_fam_tc, fi_tys) = coAxiomSplitLHS fi_axiom
94             }
95
96 data FamFlavor 
97   = SynFamilyInst         -- A synonym family
98   | DataFamilyInst TyCon  -- A data family, with its representation TyCon
99 \end{code}
100
101
102 \begin{code}
103 -- Obtain the axiom of a family instance
104 famInstAxiom :: FamInst -> CoAxiom
105 famInstAxiom = fi_axiom
106
107 famInstLHS :: FamInst -> (TyCon, [Type])
108 famInstLHS (FamInst { fi_fam_tc = tc, fi_tys = tys }) = (tc, tys)
109
110 -- Return the representation TyCons introduced by data family instances, if any
111 famInstsRepTyCons :: [FamInst] -> [TyCon]
112 famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis]
113
114 -- Extracts the TyCon for this *data* (or newtype) instance
115 famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
116 famInstRepTyCon_maybe fi 
117   = case fi_flavor fi of
118        DataFamilyInst tycon -> Just tycon
119        SynFamilyInst        -> Nothing
120
121 dataFamInstRepTyCon :: FamInst -> TyCon
122 dataFamInstRepTyCon fi 
123   = case fi_flavor fi of
124        DataFamilyInst tycon -> tycon
125        SynFamilyInst        -> pprPanic "dataFamInstRepTyCon" (ppr fi)
126
127 famInstTyVars :: FamInst -> TyVarSet
128 famInstTyVars = fi_tvs
129 \end{code}
130
131 \begin{code}
132 instance NamedThing FamInst where
133    getName = coAxiomName . fi_axiom
134
135 instance Outputable FamInst where
136    ppr = pprFamInst
137
138 -- Prints the FamInst as a family instance declaration
139 pprFamInst :: FamInst -> SDoc
140 pprFamInst famInst
141   = hang (pprFamInstHdr famInst)
142        2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> ppr ax)
143                , ifPprDebug (ptext (sLit "RHS:") <+> ppr (coAxiomRHS ax))
144                , ptext (sLit "--") <+> pprDefinedAt (getName famInst)])
145   where
146     ax = fi_axiom famInst
147
148 pprFamInstHdr :: FamInst -> SDoc
149 pprFamInstHdr (FamInst {fi_axiom = axiom, fi_flavor = flavor})
150   = pprTyConSort <+> pp_instance <+> pprHead
151   where
152     (fam_tc, tys) = coAxiomSplitLHS axiom 
153     
154     -- For *associated* types, say "type T Int = blah" 
155     -- For *top level* type instances, say "type instance T Int = blah"
156     pp_instance 
157       | isTyConAssoc fam_tc = empty
158       | otherwise           = ptext (sLit "instance")
159
160     pprHead = 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 overwriteFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
329 overwriteFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
330   = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
331   where
332     add (FamIE items tyvar) _ = FamIE (replaceFInst items)
333                                       (ins_tyvar || tyvar)
334     ins_tyvar = not (any isJust mb_tcs)
335     match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
336     
337     inst_axiom = famInstAxiom ins_item
338     (fam, tys) = coAxiomSplitLHS inst_axiom
339     arity = tyConArity fam
340     n_tys = length tys
341     match_tys 
342         | arity > n_tys = take arity tys
343         | otherwise     = tys
344     rough_tcs = roughMatchTcs match_tys
345     
346     replaceFInst [] = [ins_item]
347     replaceFInst (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, 
348                                   fi_tys = tpl_tys }) : rest)
349         -- Fast check for no match, uses the "rough match" fields
350       | instanceCantMatch rough_tcs mb_tcs
351       = item : replaceFInst rest
352
353         -- Proper check
354       | Just _ <- match item tpl_tvs tpl_tys match_tys
355       = ins_item : rest
356
357         -- No match => try next
358       | otherwise
359       = item : replaceFInst rest
360
361
362
363 \end{code}
364
365 %************************************************************************
366 %*                                                                      *
367                 Looking up a family instance
368 %*                                                                      *
369 %************************************************************************
370
371 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
372 Multiple matches are only possible in case of type families (not data
373 families), and then, it doesn't matter which match we choose (as the
374 instances are guaranteed confluent).
375
376 We return the matching family instances and the type instance at which it
377 matches.  For example, if we lookup 'T [Int]' and have a family instance
378
379   data instance T [a] = ..
380
381 desugared to
382
383   data :R42T a = ..
384   coe :Co:R42T a :: T [a] ~ :R42T a
385
386 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
387
388 \begin{code}
389 type FamInstMatch = (FamInst, [Type])           -- Matching type instance
390   -- See Note [Over-saturated matches]
391
392 lookupFamInstEnv
393     :: FamInstEnvs
394     -> TyCon -> [Type]          -- What we are looking for
395     -> [FamInstMatch]           -- Successful matches
396 -- Precondition: the tycon is saturated (or over-saturated)
397
398 lookupFamInstEnv
399    = lookup_fam_inst_env match True
400    where
401      match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
402
403 lookupFamInstEnvConflicts
404     :: FamInstEnvs
405     -> FamInst          -- Putative new instance
406     -> [TyVar]          -- Unique tyvars, matching arity of FamInst
407     -> [FamInstMatch]   -- Conflicting matches
408 -- E.g. when we are about to add
409 --    f : type instance F [a] = a->a
410 -- we do (lookupFamInstConflicts f [b])
411 -- to find conflicting matches
412 -- The skolem tyvars are needed because we don't have a 
413 -- unique supply to hand
414 --
415 -- Precondition: the tycon is saturated (or over-saturated)
416
417 lookupFamInstEnvConflicts envs fam_inst skol_tvs
418   = lookup_fam_inst_env my_unify False envs fam tys1
419   where
420     inst_axiom = famInstAxiom fam_inst
421     (fam, tys) = famInstLHS fam_inst
422     skol_tys   = mkTyVarTys skol_tvs
423     tys1       = substTys (zipTopTvSubst (coAxiomTyVars inst_axiom) skol_tys) tys
424         -- In example above,   fam tys' = F [b]   
425
426     my_unify old_fam_inst tpl_tvs tpl_tys match_tys
427        = ASSERT2( tyVarsOfTypes tys1 `disjointVarSet` tpl_tvs,
428                   (ppr fam <+> ppr tys1) $$
429                   (ppr tpl_tvs <+> ppr tpl_tys) )
430                 -- Unification will break badly if the variables overlap
431                 -- They shouldn't because we allocate separate uniques for them
432          case tcUnifyTys instanceBindFun tpl_tys match_tys of
433               Just subst | conflicting old_fam_inst subst -> Just subst
434               _other                                      -> Nothing
435
436       -- Note [Family instance overlap conflicts]
437     conflicting old_fam_inst subst 
438       | isAlgTyCon fam = True
439       | otherwise      = not (old_rhs `eqType` new_rhs)
440       where
441         old_axiom = famInstAxiom old_fam_inst
442         old_tvs   = coAxiomTyVars old_axiom
443         old_rhs   = mkAxInstRHS old_axiom  (substTyVars subst old_tvs)
444         new_rhs   = mkAxInstRHS inst_axiom (substTyVars subst skol_tvs)
445
446 -- This variant is called when we want to check if the conflict is only in the
447 -- home environment (see FamInst.addLocalFamInst)
448 lookupFamInstEnvConflicts' :: FamInstEnv -> FamInst -> [TyVar] -> [FamInstMatch]
449 lookupFamInstEnvConflicts' env fam_inst skol_tvs
450   = lookupFamInstEnvConflicts (emptyFamInstEnv, env) fam_inst skol_tvs
451 \end{code}
452
453 Note [Family instance overlap conflicts]
454 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
455 - In the case of data family instances, any overlap is fundamentally a
456   conflict (as these instances imply injective type mappings).
457
458 - In the case of type family instances, overlap is admitted as long as
459   the right-hand sides of the overlapping rules coincide under the
460   overlap substitution.  eg
461        type instance F a Int = a
462        type instance F Int b = b
463   These two overlap on (F Int Int) but then both RHSs are Int, 
464   so all is well. We require that they are syntactically equal;
465   anything else would be difficult to test for at this stage.
466
467
468 While @lookupFamInstEnv@ uses a one-way match, the next function
469 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification).  This is
470 needed to check for overlapping instances.
471
472 For class instances, these two variants of lookup are combined into one
473 function (cf, @InstEnv@).  We don't do that for family instances as the
474 results of matching and unification are used in two different contexts.
475 Moreover, matching is the wildly more frequently used operation in the case of
476 indexed synonyms and we don't want to slow that down by needless unification.
477
478 \begin{code}
479 ------------------------------------------------------------
480 -- Might be a one-way match or a unifier
481 type MatchFun =  FamInst                -- The FamInst template
482               -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
483               -> [Type]                 -- Target to match against
484               -> Maybe TvSubst
485
486 type OneSidedMatch = Bool     -- Are optimisations that are only valid for
487                               -- one sided matches allowed?
488
489 lookup_fam_inst_env'          -- The worker, local to this module
490     :: MatchFun
491     -> OneSidedMatch
492     -> FamInstEnv
493     -> TyCon -> [Type]          -- What we are looking for
494     -> [FamInstMatch]           -- Successful matches
495 lookup_fam_inst_env' match_fun one_sided ie fam tys
496   | not (isFamilyTyCon fam) 
497   = []
498   | otherwise
499   = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys )      -- Family type applications must be saturated
500     lookup ie
501   where
502     -- See Note [Over-saturated matches]
503     arity = tyConArity fam
504     n_tys = length tys
505     extra_tys = drop arity tys
506     (match_tys, add_extra_tys) 
507        | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
508        | otherwise     = (tys,            \res_tys -> res_tys)
509          -- The second case is the common one, hence functional representation
510
511     --------------
512     rough_tcs = roughMatchTcs match_tys
513     all_tvs   = all isNothing rough_tcs && one_sided
514
515     --------------
516     lookup env = case lookupUFM env fam of
517                    Nothing -> []        -- No instances for this class
518                    Just (FamIE insts has_tv_insts)
519                        -- Short cut for common case:
520                        --   The thing we are looking up is of form (C a
521                        --   b c), and the FamIE has no instances of
522                        --   that form, so don't bother to search 
523                      | all_tvs && not has_tv_insts -> []
524                      | otherwise                   -> find insts
525
526     --------------
527     find [] = []
528     find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, 
529                           fi_tys = tpl_tys, fi_axiom = axiom }) : rest)
530         -- Fast check for no match, uses the "rough match" fields
531       | instanceCantMatch rough_tcs mb_tcs
532       = find rest
533
534         -- Proper check
535       | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
536       = (item, add_extra_tys $ substTyVars subst (coAxiomTyVars axiom)) : find rest
537
538         -- No match => try next
539       | otherwise
540       = find rest
541 -- Precondition: the tycon is saturated (or over-saturated)
542
543 lookup_fam_inst_env           -- The worker, local to this module
544     :: MatchFun
545     -> OneSidedMatch
546     -> FamInstEnvs
547     -> TyCon -> [Type]          -- What we are looking for
548     -> [FamInstMatch]           -- Successful matches
549
550 -- Precondition: the tycon is saturated (or over-saturated)
551
552 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys = 
553     lookup_fam_inst_env' match_fun one_sided home_ie fam tys ++
554     lookup_fam_inst_env' match_fun one_sided pkg_ie  fam tys
555
556 \end{code}
557
558 Note [Over-saturated matches]
559 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
560 It's ok to look up an over-saturated type constructor.  E.g.
561      type family F a :: * -> *
562      type instance F (a,b) = Either (a->b)
563
564 The type instance gives rise to a newtype TyCon (at a higher kind
565 which you can't do in Haskell!):
566      newtype FPair a b = FP (Either (a->b))
567
568 Then looking up (F (Int,Bool) Char) will return a FamInstMatch 
569      (FPair, [Int,Bool,Char])
570
571 The "extra" type argument [Char] just stays on the end.
572
573
574
575
576 %************************************************************************
577 %*                                                                      *
578                 Looking up a family instance
579 %*                                                                      *
580 %************************************************************************
581
582 \begin{code}
583 topNormaliseType :: FamInstEnvs
584                  -> Type
585                  -> Maybe (Coercion, Type)
586
587 -- Get rid of *outermost* (or toplevel) 
588 --      * type functions 
589 --      * newtypes
590 -- using appropriate coercions.
591 -- By "outer" we mean that toplevelNormaliseType guarantees to return
592 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
593 -- outermost form.  It *can* return something like (Maybe (F ty)), where
594 -- (F ty) is a redex.
595
596 -- Its a bit like Type.repType, but handles type families too
597
598 topNormaliseType env ty
599   = go [] ty
600   where
601     go :: [TyCon] -> Type -> Maybe (Coercion, Type)
602     go rec_nts ty | Just ty' <- coreView ty     -- Expand synonyms
603         = go rec_nts ty'        
604
605     go rec_nts (TyConApp tc tys)
606         | isNewTyCon tc         -- Expand newtypes
607         = if tc `elem` rec_nts  -- See Note [Expanding newtypes] in Type.lhs
608           then Nothing
609           else let nt_co = mkAxInstCo (newTyConCo tc) tys
610                in add_co nt_co rec_nts' nt_rhs
611
612         | isFamilyTyCon tc              -- Expand open tycons
613         , (co, ty) <- normaliseTcApp env tc tys
614                 -- Note that normaliseType fully normalises 'tys', 
615                 -- It has do to so to be sure that nested calls like
616                 --    F (G Int)
617                 -- are correctly top-normalised
618         , not (isReflCo co)
619         = add_co co rec_nts ty
620         where
621           nt_rhs = newTyConInstRhs tc tys
622           rec_nts' | isRecursiveTyCon tc = tc:rec_nts
623                    | otherwise           = rec_nts
624
625     go _ _ = Nothing
626
627     add_co co rec_nts ty 
628         = case go rec_nts ty of
629                 Nothing         -> Just (co, ty)
630                 Just (co', ty') -> Just (mkTransCo co co', ty')
631          
632
633 ---------------
634 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
635 normaliseTcApp env tc tys
636   | isFamilyTyCon tc
637   , tyConArity tc <= length tys    -- Unsaturated data families are possible
638   , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys 
639   = let    -- A matching family instance exists
640         ax              = famInstAxiom fam_inst
641         co              = mkAxInstCo  ax inst_tys
642         rhs             = mkAxInstRHS ax inst_tys
643         first_coi       = mkTransCo tycon_coi co
644         (rest_coi,nty)  = normaliseType env rhs
645         fix_coi         = mkTransCo first_coi rest_coi
646     in 
647     (fix_coi, nty)
648
649   | otherwise   -- No unique matching family instance exists;
650                 -- we do not do anything
651   = (tycon_coi, TyConApp tc ntys)
652
653   where
654         -- Normalise the arg types so that they'll match 
655         -- when we lookup in in the instance envt
656     (cois, ntys) = mapAndUnzip (normaliseType env) tys
657     tycon_coi    = mkTyConAppCo tc cois
658
659 ---------------
660 normaliseType :: FamInstEnvs            -- environment with family instances
661               -> Type                   -- old type
662               -> (Coercion, Type)       -- (coercion,new type), where
663                                         -- co :: old-type ~ new_type
664 -- Normalise the input type, by eliminating *all* type-function redexes
665 -- Returns with Refl if nothing happens
666
667 normaliseType env ty 
668   | Just ty' <- coreView ty = normaliseType env ty' 
669 normaliseType env (TyConApp tc tys)
670   = normaliseTcApp env tc tys
671 normaliseType _env ty@(LitTy {}) = (Refl ty, ty)
672 normaliseType env (AppTy ty1 ty2)
673   = let (coi1,nty1) = normaliseType env ty1
674         (coi2,nty2) = normaliseType env ty2
675     in  (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
676 normaliseType env (FunTy ty1 ty2)
677   = let (coi1,nty1) = normaliseType env ty1
678         (coi2,nty2) = normaliseType env ty2
679     in  (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
680 normaliseType env (ForAllTy tyvar ty1)
681   = let (coi,nty1) = normaliseType env ty1
682     in  (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
683 normaliseType _   ty@(TyVarTy _)
684   = (Refl ty,ty)
685 \end{code}