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