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