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