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,
  14         extendFamInstEnv, extendFamInstEnvList,
  15         famInstEnvElts, familyInstances,
  16
  17         lookupFamInstEnv, lookupFamInstEnvUnify,
  18
  19         -- Normalisation
  20         toplevelNormaliseFamInst
  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 OccName
  37 import SrcLoc
  38 import UniqFM
  39 import Outputable
  40 import Maybes
  41 import Util
  42
  43 import Maybe
  44 \end{code}
  45
  46
  47 %************************************************************************
  48 %*                                                                      *
  49 \subsection{Type checked family instance heads}
  50 %*                                                                      *
  51 %************************************************************************
  52
  53 \begin{code}
  54 data FamInst
  55   = FamInst { fi_fam   :: Name          -- Family name
  56                 -- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of
  57                 --                         Just (tc, tys) -> tc
  58
  59                 -- Used for "rough matching"; same idea as for class instances
  60             , fi_tcs   :: [Maybe Name]  -- Top of type args
  61                 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
  62
  63                 -- Used for "proper matching"; ditto
  64             , fi_tvs   :: TyVarSet      -- Template tyvars for full match
  65             , fi_tys   :: [Type]        -- Full arg types
  66                 -- INVARIANT: fi_tvs = tyConTyVars fi_tycon
  67                 --            fi_tys = case tyConFamInst_maybe fi_tycon of
  68                 --                         Just (_, tys) -> tys
  69
  70             , fi_tycon :: TyCon         -- Representation tycon
  71             }
  72
  73 -- Obtain the representation tycon of a family instance.
  74 --
  75 famInstTyCon :: FamInst -> TyCon
  76 famInstTyCon = fi_tycon
  77
  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("--") <+> (pprDefnLoc (getSrcSpan 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 (parenSymOcc (getOccName 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 emptyFamInstEnv :: FamInstEnv
 172 emptyFamInstEnv = emptyUFM
 173
 174 famInstEnvElts :: FamInstEnv -> [FamInst]
 175 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
 176
 177 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
 178 familyInstances (pkg_fie, home_fie) fam
 179   = get home_fie ++ get pkg_fie
 180   where
 181     get env = case lookupUFM env fam of
 182                 Just (FamIE insts _) -> insts
 183                 Nothing              -> []
 184
 185 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
 186 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
 187
 188 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
 189 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
 190   = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
 191   where
 192     add (FamIE items tyvar) _ = FamIE (ins_item:items)
 193                                       (ins_tyvar || tyvar)
 194     ins_tyvar = not (any isJust mb_tcs)
 195 \end{code}
 196
 197 %************************************************************************
 198 %*                                                                      *
 199 \subsection{Looking up a family instance}
 200 %*                                                                      *
 201 %************************************************************************
 202
 203 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
 204 Multiple matches are only possible in case of type families (not data
 205 families), and then, it doesn't matter which match we choose (as the
 206 instances are guaranteed confluent).
 207
 208 We return the matching family instances and the type instance at which it
 209 matches.  For example, if we lookup 'T [Int]' and have a family instance
 210
 211   data instance T [a] = ..
 212
 213 desugared to
 214
 215   data :R42T a = ..
 216   coe :Co:R42T a :: T [a] ~ :R42T a
 217
 218 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
 219
 220 \begin{code}
 221 type FamInstMatch = (FamInst, [Type])           -- Matching type instance
 222
 223 lookupFamInstEnv :: FamInstEnvs
 224                  -> TyCon -> [Type]             -- What we are looking for
 225                  -> [FamInstMatch]              -- Successful matches
 226 lookupFamInstEnv (pkg_ie, home_ie) fam tys
 227   = home_matches ++ pkg_matches
 228   where
 229     rough_tcs    = roughMatchTcs tys
 230     all_tvs      = all isNothing rough_tcs
 231     home_matches = lookup home_ie
 232     pkg_matches  = lookup pkg_ie
 233
 234     --------------
 235     lookup env = case lookupUFM env fam of
 236                    Nothing -> []        -- No instances for this class
 237                    Just (FamIE insts has_tv_insts)
 238                        -- Short cut for common case:
 239                        --   The thing we are looking up is of form (C a
 240                        --   b c), and the FamIE has no instances of
 241                        --   that form, so don't bother to search
 242                      | all_tvs && not has_tv_insts -> []
 243                      | otherwise                   -> find insts
 244
 245     --------------
 246     find [] = []
 247     find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
 248                           fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
 249         -- Fast check for no match, uses the "rough match" fields
 250       | instanceCantMatch rough_tcs mb_tcs
 251       = find rest
 252
 253         -- Proper check
 254       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
 255       = (item, substTyVars subst (tyConTyVars tycon)) : find rest
 256
 257         -- No match => try next
 258       | otherwise
 259       = find rest
 260 \end{code}
 261
 262 While @lookupFamInstEnv@ uses a one-way match, the next function
 263 @lookupFamInstEnvUnify@ uses two-way matching (ie, unification).  This is
 264 needed to check for overlapping instances.
 265
 266 For class instances, these two variants of lookup are combined into one
 267 function (cf, @InstEnv@).  We don't do that for family instances as the
 268 results of matching and unification are used in two different contexts.
 269 Moreover, matching is the wildly more frequently used operation in the case of
 270 indexed synonyms and we don't want to slow that down by needless unification.
 271
 272 \begin{code}
 273 lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
 274                       -> [(FamInstMatch)]
 275 lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
 276   = home_matches ++ pkg_matches
 277   where
 278     rough_tcs    = roughMatchTcs tys
 279     all_tvs      = all isNothing rough_tcs
 280     home_matches = lookup home_ie
 281     pkg_matches  = lookup pkg_ie
 282
 283     --------------
 284     lookup env = case lookupUFM env fam of
 285                    Nothing -> []        -- No instances for this class
 286                    Just (FamIE insts has_tv_insts)
 287                        -- Short cut for common case:
 288                        --   The thing we are looking up is of form (C a
 289                        --   b c), and the FamIE has no instances of
 290                        --   that form, so don't bother to search
 291                      | all_tvs && not has_tv_insts -> []
 292                      | otherwise                   -> find insts
 293
 294     --------------
 295     find [] = []
 296     find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
 297                           fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
 298         -- Fast check for no match, uses the "rough match" fields
 299       | instanceCantMatch rough_tcs mb_tcs
 300       = find rest
 301
 302       | otherwise
 303       = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
 304                  (ppr fam <+> ppr tys <+> ppr all_tvs) $$
 305                  (ppr tycon <+> ppr tpl_tvs <+> ppr tpl_tys)
 306                 )
 307                 -- Unification will break badly if the variables overlap
 308                 -- They shouldn't because we allocate separate uniques for them
 309         case tcUnifyTys bind_fn tpl_tys tys of
 310             Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
 311                           in
 312                           (item, rep_tys) : find rest
 313             Nothing    -> find rest
 314
 315 -- See explanation at @InstEnv.bind_fn@.
 316 --
 317 bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
 318            | otherwise                             = BindMe
 319 \end{code}
 320
 321 --------------------------------------
 322 -- Normalisation
 323
 324 \begin{code}
 325         -- get rid of TOPLEVEL type functions by rewriting them
 326         -- i.e. treating their equations as a TRS
 327 toplevelNormaliseFamInst :: FamInstEnvs ->
 328                             Type ->
 329                             (CoercionI,Type)
 330 toplevelNormaliseFamInst env ty
 331         | Just ty' <- tcView ty = normaliseFamInst env ty'
 332 toplevelNormaliseFamInst env ty@(TyConApp tyCon tys)
 333         | isOpenTyCon tyCon
 334         = normaliseFamInst env ty
 335 toplevelNormaliseFamInst env ty
 336         = (IdCo,ty)
 337
 338
 339         -- get rid of ALL type functions by rewriting them
 340         -- i.e. treating their equations as a TRS
 341 normaliseFamInst :: FamInstEnvs ->      -- environment with family instances
 342                     Type ->             -- old type
 343                     (CoercionI,Type)    -- (coercion,new type)
 344 normaliseFamInst env ty
 345         | Just ty' <- tcView ty = normaliseFamInst env ty'
 346 normaliseFamInst env ty@(TyConApp tyCon tys) =
 347         let (cois,ntys) = mapAndUnzip (normaliseFamInst env) tys
 348             tycon_coi   = mkTyConAppCoI tyCon ntys cois
 349             maybe_ty_co = lookupFamInst env tyCon ntys
 350          in case maybe_ty_co of
 351                 -- a matching family instance exists
 352                 Just (ty',co) ->
 353                         let first_coi      = mkTransCoI tycon_coi (ACo co)
 354                             (rest_coi,nty) = normaliseFamInst env ty'
 355                             fix_coi        = mkTransCoI first_coi rest_coi
 356                         in (fix_coi,nty)
 357                 -- no matching family instance exists
 358                 -- we do not do anything
 359                 Nothing ->
 360                         (tycon_coi,TyConApp tyCon ntys)
 361 normaliseFamInst env ty@(AppTy ty1 ty2) =
 362         let (coi1,nty1) = normaliseFamInst env ty1
 363             (coi2,nty2) = normaliseFamInst env ty2
 364         in  (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
 365 normaliseFamInst env ty@(FunTy ty1 ty2) =
 366         let (coi1,nty1) = normaliseFamInst env ty1
 367             (coi2,nty2) = normaliseFamInst env ty2
 368         in  (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
 369 normaliseFamInst env ty@(ForAllTy tyvar ty1)    =
 370         let (coi,nty1) = normaliseFamInst env ty1
 371         in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
 372 normaliseFamInst env ty@(NoteTy note ty1)       =
 373         let (coi,nty1) = normaliseFamInst env ty1
 374         in  (mkNoteTyCoI note coi,NoteTy note nty1)
 375 normaliseFamInst env ty@(TyVarTy _) =
 376         (IdCo,ty)
 377 normaliseFamInst env (PredTy predty) =
 378         normaliseFamInstPred env predty
 379
 380 normaliseFamInstPred :: FamInstEnvs -> PredType -> (CoercionI,Type)
 381 normaliseFamInstPred env (ClassP cls tys) =
 382         let (cois,tys') = mapAndUnzip (normaliseFamInst env) tys
 383         in  (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
 384 normaliseFamInstPred env (IParam ipn ty) =
 385         let (coi,ty') = normaliseFamInst env ty
 386         in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
 387 normaliseFamInstPred env (EqPred ty1 ty2) =
 388         let (coi1,ty1') = normaliseFamInst env ty1
 389             (coi2,ty2') = normaliseFamInst env ty2
 390         in  (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')
 391
 392 lookupFamInst :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type,Coercion)
 393
 394 -- (lookupFamInst F tys) looks for a top-level instance
 395 --      co : forall a. F tys' = G a
 396 --   (The rhs is always of form G a; see Note [The FamInst structure]
 397 --      in FamInst.)
 398 -- where we can instantiate 'a' with t to make tys'[t/a] = tys
 399 -- Hence   (co t) : F tys ~ G t
 400 -- Then we return (Just (G t, co t))
 401
 402 lookupFamInst env tycon tys
 403   | not (isOpenTyCon tycon)             -- Dead code; fix.
 404   = Nothing
 405   | otherwise
 406   = case lookupFamInstEnv env tycon tys of
 407            [(subst, fam_inst)] ->
 408              Just (mkTyConApp rep_tc substituted_vars, mkTyConApp coercion_tycon substituted_vars)
 409                 where   -- NB: invariant of lookupFamInstEnv is that (tyConTyVars rep_tc)
 410                         --     is in the domain of the substitution
 411                   rep_tc           = famInstTyCon fam_inst
 412                   coercion_tycon   = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
 413                   substituted_vars = substTyVars subst (tyConTyVars rep_tc)
 414            other -> Nothing
 415 \end{code}