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