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