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                  | isAbstractTyCon tycon = ptext (sLit "data instance")
  99                  | otherwise             = panic "FamInstEnv.pprFamInstHdr"
 100
 101 pprFamInsts :: [FamInst] -> SDoc
 102 pprFamInsts finsts = vcat (map pprFamInst finsts)
 103
 104 famInstHead :: FamInst -> ([TyVar], TyCon, [Type])
 105 famInstHead (FamInst {fi_tycon = tycon})
 106   = case tyConFamInst_maybe tycon of
 107       Nothing         -> panic "FamInstEnv.famInstHead"
 108       Just (fam, tys) -> (tyConTyVars tycon, fam, tys)
 109
 110 -- Make a family instance representation from a tycon.  This is used for local
 111 -- instances, where we can safely pull on the tycon.
 112 --
 113 mkLocalFamInst :: TyCon -> FamInst
 114 mkLocalFamInst tycon
 115   = case tyConFamInst_maybe tycon of
 116            Nothing         -> panic "FamInstEnv.mkLocalFamInst"
 117            Just (fam, tys) ->
 118              FamInst {
 119                fi_fam   = tyConName fam,
 120                fi_tcs   = roughMatchTcs tys,
 121                fi_tvs   = mkVarSet . tyConTyVars $ tycon,
 122                fi_tys   = tys,
 123                fi_tycon = tycon
 124              }
 125
 126 -- Make a family instance representation from the information found in an
 127 -- unterface file.  In particular, we get the rough match info from the iface
 128 -- (instead of computing it here).
 129 --
 130 mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
 131 mkImportedFamInst fam mb_tcs tycon
 132   = FamInst {
 133       fi_fam   = fam,
 134       fi_tcs   = mb_tcs,
 135       fi_tvs   = mkVarSet . tyConTyVars $ tycon,
 136       fi_tys   = case tyConFamInst_maybe tycon of
 137                    Nothing       -> panic "FamInstEnv.mkImportedFamInst"
 138                    Just (_, tys) -> tys,
 139       fi_tycon = tycon
 140     }
 141 \end{code}
 142
 143
 144 %************************************************************************
 145 %*                                                                      *
 146                 FamInstEnv
 147 %*                                                                      *
 148 %************************************************************************
 149
 150 InstEnv maps a family name to the list of known instances for that family.
 151
 152 \begin{code}
 153 type FamInstEnv = UniqFM FamilyInstEnv  -- Maps a family to its instances
 154
 155 type FamInstEnvs = (FamInstEnv, FamInstEnv)
 156         -- External package inst-env, Home-package inst-env
 157
 158 data FamilyInstEnv
 159   = FamIE [FamInst]     -- The instances for a particular family, in any order
 160           Bool          -- True <=> there is an instance of form T a b c
 161                         --      If *not* then the common case of looking up
 162                         --      (T a b c) can fail immediately
 163
 164 -- INVARIANTS:
 165 --  * The fs_tvs are distinct in each FamInst
 166 --      of a range value of the map (so we can safely unify them)
 167
 168 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
 169 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
 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                 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   -- See Note [Over-saturated matches]
 223
 224 lookupFamInstEnv
 225     :: FamInstEnvs
 226     -> TyCon -> [Type]          -- What we are looking for
 227     -> [FamInstMatch]           -- Successful matches
 228
 229 lookupFamInstEnv
 230    = lookup_fam_inst_env match True
 231    where
 232      match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
 233
 234 lookupFamInstEnvConflicts
 235     :: FamInstEnvs
 236     -> FamInst          -- Putative new instance
 237     -> [TyVar]          -- Unique tyvars, matching arity of FamInst
 238     -> [FamInstMatch]   -- Conflicting matches
 239 -- E.g. when we are about to add
 240 --    f : type instance F [a] = a->a
 241 -- we do (lookupFamInstConflicts f [b])
 242 -- to find conflicting matches
 243 -- The skolem tyvars are needed because we don't have a
 244 -- unique supply to hand
 245
 246 lookupFamInstEnvConflicts envs fam_inst skol_tvs
 247   = lookup_fam_inst_env my_unify False envs fam tys'
 248   where
 249     inst_tycon = famInstTyCon fam_inst
 250     (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
 251                             (tyConFamInst_maybe inst_tycon)
 252     skol_tys = mkTyVarTys skol_tvs
 253     tys'     = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
 254         -- In example above,   fam tys' = F [b]
 255
 256     my_unify old_fam_inst tpl_tvs tpl_tys match_tys
 257        = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
 258                   (ppr fam <+> ppr tys) $$
 259                   (ppr tpl_tvs <+> ppr tpl_tys) )
 260                 -- Unification will break badly if the variables overlap
 261                 -- They shouldn't because we allocate separate uniques for them
 262          case tcUnifyTys instanceBindFun tpl_tys match_tys of
 263               Just subst | conflicting old_fam_inst subst -> Just subst
 264               _other                                      -> Nothing
 265
 266       -- - In the case of data family instances, any overlap is fundamentally a
 267       --   conflict (as these instances imply injective type mappings).
 268       -- - In the case of type family instances, overlap is admitted as long as
 269       --   the right-hand sides of the overlapping rules coincide under the
 270       --   overlap substitution.  We require that they are syntactically equal;
 271       --   anything else would be difficult to test for at this stage.
 272     conflicting old_fam_inst subst
 273       | isAlgTyCon fam = True
 274       | otherwise      = not (old_rhs `tcEqType` new_rhs)
 275       where
 276         old_tycon = famInstTyCon old_fam_inst
 277         old_tvs   = tyConTyVars old_tycon
 278         old_rhs   = mkTyConApp old_tycon  (substTyVars subst old_tvs)
 279         new_rhs   = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
 280 \end{code}
 281
 282 While @lookupFamInstEnv@ uses a one-way match, the next function
 283 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification).  This is
 284 needed to check for overlapping instances.
 285
 286 For class instances, these two variants of lookup are combined into one
 287 function (cf, @InstEnv@).  We don't do that for family instances as the
 288 results of matching and unification are used in two different contexts.
 289 Moreover, matching is the wildly more frequently used operation in the case of
 290 indexed synonyms and we don't want to slow that down by needless unification.
 291
 292 \begin{code}
 293 ------------------------------------------------------------
 294 -- Might be a one-way match or a unifier
 295 type MatchFun =  FamInst                -- The FamInst template
 296               -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
 297               -> [Type]                 -- Target to match against
 298               -> Maybe TvSubst
 299
 300 type OneSidedMatch = Bool     -- Are optimisations that are only valid for
 301                               -- one sided matches allowed?
 302
 303 lookup_fam_inst_env           -- The worker, local to this module
 304     :: MatchFun
 305     -> OneSidedMatch
 306     -> FamInstEnvs
 307     -> TyCon -> [Type]          -- What we are looking for
 308     -> [FamInstMatch]           -- Successful matches
 309 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
 310   | not (isFamilyTyCon fam)
 311   = []
 312   | otherwise
 313   = ASSERT( n_tys >= arity )    -- Family type applications must be saturated
 314     home_matches ++ pkg_matches
 315   where
 316     home_matches = lookup home_ie
 317     pkg_matches  = lookup pkg_ie
 318
 319     -- See Note [Over-saturated matches]
 320     arity = tyConArity fam
 321     n_tys = length tys
 322     extra_tys = drop arity tys
 323     (match_tys, add_extra_tys)
 324        | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
 325        | otherwise     = (tys,            \res_tys -> res_tys)
 326          -- The second case is the common one, hence functional representation
 327
 328     --------------
 329     rough_tcs = roughMatchTcs match_tys
 330     all_tvs   = all isNothing rough_tcs && one_sided
 331
 332     --------------
 333     lookup env = case lookupUFM env fam of
 334                    Nothing -> []        -- No instances for this class
 335                    Just (FamIE insts has_tv_insts)
 336                        -- Short cut for common case:
 337                        --   The thing we are looking up is of form (C a
 338                        --   b c), and the FamIE has no instances of
 339                        --   that form, so don't bother to search
 340                      | all_tvs && not has_tv_insts -> []
 341                      | otherwise                   -> find insts
 342
 343     --------------
 344     find [] = []
 345     find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
 346                           fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
 347         -- Fast check for no match, uses the "rough match" fields
 348       | instanceCantMatch rough_tcs mb_tcs
 349       = find rest
 350
 351         -- Proper check
 352       | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
 353       = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
 354
 355         -- No match => try next
 356       | otherwise
 357       = find rest
 358 \end{code}
 359
 360 Note [Over-saturated matches]
 361 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 362 It's ok to look up an over-saturated type constructor.  E.g.
 363      type family F a :: * -> *
 364      type instance F (a,b) = Either (a->b)
 365
 366 The type instance gives rise to a newtype TyCon (at a higher kind
 367 which you can't do in Haskell!):
 368      newtype FPair a b = FP (Either (a->b))
 369
 370 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
 371      (FPair, [Int,Bool,Char])
 372
 373 The "extra" type argument [Char] just stays on the end.
 374
 375
 376
 377
 378 %************************************************************************
 379 %*                                                                      *
 380                 Looking up a family instance
 381 %*                                                                      *
 382 %************************************************************************
 383
 384 \begin{code}
 385 topNormaliseType :: FamInstEnvs
 386                  -> Type
 387                  -> Maybe (Coercion, Type)
 388
 389 -- Get rid of *outermost* (or toplevel)
 390 --      * type functions
 391 --      * newtypes
 392 -- using appropriate coercions.
 393 -- By "outer" we mean that toplevelNormaliseType guarantees to return
 394 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
 395 -- outermost form.  It *can* return something like (Maybe (F ty)), where
 396 -- (F ty) is a redex.
 397
 398 -- Its a bit like Type.repType, but handles type families too
 399
 400 topNormaliseType env ty
 401   = go [] ty
 402   where
 403     go :: [TyCon] -> Type -> Maybe (Coercion, Type)
 404     go rec_nts ty | Just ty' <- coreView ty     -- Expand synonyms
 405         = go rec_nts ty'
 406
 407     go rec_nts (TyConApp tc tys)                -- Expand newtypes
 408         | Just co_con <- newTyConCo_maybe tc    -- See Note [Expanding newtypes]
 409         = if tc `elem` rec_nts                  --  in Type.lhs
 410           then Nothing
 411           else let nt_co = mkTyConApp co_con tys
 412                in add_co nt_co rec_nts' nt_rhs
 413         where
 414           nt_rhs = newTyConInstRhs tc tys
 415           rec_nts' | isRecursiveTyCon tc = tc:rec_nts
 416                    | otherwise           = rec_nts
 417
 418     go rec_nts (TyConApp tc tys)                -- Expand open tycons
 419         | isFamilyTyCon tc
 420         , (ACo co, ty) <- normaliseTcApp env tc tys
 421         =       -- The ACo says "something happened"
 422                 -- Note that normaliseType fully normalises, but it has do to so
 423                 -- to be sure that
 424            add_co co rec_nts ty
 425
 426     go _ _ = Nothing
 427
 428     add_co co rec_nts ty
 429         = case go rec_nts ty of
 430                 Nothing         -> Just (co, ty)
 431                 Just (co', ty') -> Just (mkTransCoercion co co', ty')
 432
 433
 434 ---------------
 435 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
 436 normaliseTcApp env tc tys
 437   = let -- First normalise the arg types so that they'll match
 438         -- when we lookup in in the instance envt
 439         (cois, ntys) = mapAndUnzip (normaliseType env) tys
 440         tycon_coi    = mkTyConAppCoI tc cois
 441     in  -- Now try the top-level redex
 442     case lookupFamInstEnv env tc ntys of
 443                 -- A matching family instance exists
 444         [(fam_inst, tys)] -> (fix_coi, nty)
 445             where
 446                 rep_tc         = famInstTyCon fam_inst
 447                 co_tycon       = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
 448                 co             = mkTyConApp co_tycon tys
 449                 first_coi      = mkTransCoI tycon_coi (ACo co)
 450                 (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
 451                 fix_coi        = mkTransCoI first_coi rest_coi
 452
 453                 -- No unique matching family instance exists;
 454                 -- we do not do anything
 455         _ -> (tycon_coi, TyConApp tc ntys)
 456 ---------------
 457 normaliseType :: FamInstEnvs            -- environment with family instances
 458               -> Type                   -- old type
 459               -> (CoercionI, Type)      -- (coercion,new type), where
 460                                         -- co :: old-type ~ new_type
 461 -- Normalise the input type, by eliminating *all* type-function redexes
 462 -- Returns with IdCo if nothing happens
 463
 464 normaliseType env ty
 465   | Just ty' <- coreView ty = normaliseType env ty'
 466 normaliseType env (TyConApp tc tys)
 467   = normaliseTcApp env tc tys
 468 normaliseType env (AppTy ty1 ty2)
 469   = let (coi1,nty1) = normaliseType env ty1
 470         (coi2,nty2) = normaliseType env ty2
 471     in  (mkAppTyCoI coi1 coi2, AppTy nty1 nty2)
 472 normaliseType env (FunTy ty1 ty2)
 473   = let (coi1,nty1) = normaliseType env ty1
 474         (coi2,nty2) = normaliseType env ty2
 475     in  (mkFunTyCoI coi1 coi2, FunTy nty1 nty2)
 476 normaliseType env (ForAllTy tyvar ty1)
 477   = let (coi,nty1) = normaliseType env ty1
 478     in  (mkForAllTyCoI tyvar coi, ForAllTy tyvar nty1)
 479 normaliseType _   ty@(TyVarTy _)
 480   = (IdCo ty,ty)
 481 normaliseType env (PredTy predty)
 482   = normalisePred env predty
 483
 484 ---------------
 485 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
 486 normalisePred env (ClassP cls tys)
 487   =     let (cois,tys') = mapAndUnzip (normaliseType env) tys
 488         in  (mkClassPPredCoI cls cois, PredTy $ ClassP cls tys')
 489 normalisePred env (IParam ipn ty)
 490   =     let (coi,ty') = normaliseType env ty
 491         in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
 492 normalisePred env (EqPred ty1 ty2)
 493   =     let (coi1,ty1') = normaliseType env ty1
 494             (coi2,ty2') = normaliseType env ty2
 495         in  (mkEqPredCoI coi1 coi2, PredTy $ EqPred ty1' ty2')
 496 \end{code}