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