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