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