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