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