compiler/types/Unify.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 \begin{code}
   6 module Unify (
   7         -- Matching of types:
   8         --      the "tc" prefix indicates that matching always
   9         --      respects newtypes (rather than looking through them)
  10         tcMatchTy, tcMatchTys, tcMatchTyX,
  11         ruleMatchTyX, tcMatchPreds, MatchEnv(..)
  12    ) where
  13
  14 #include "HsVersions.h"
  15
  16 import Var
  17 import VarEnv
  18 import VarSet
  19 import Type
  20 import TypeRep
  21 import Outputable
  22 import Maybes
  23 \end{code}
  24
  25
  26 %************************************************************************
  27 %*                                                                      *
  28                 Matching
  29 %*                                                                      *
  30 %************************************************************************
  31
  32
  33 Matching is much tricker than you might think.
  34
  35 1. The substitution we generate binds the *template type variables*
  36    which are given to us explicitly.
  37
  38 2. We want to match in the presence of foralls;
  39         e.g     (forall a. t1) ~ (forall b. t2)
  40
  41    That is what the RnEnv2 is for; it does the alpha-renaming
  42    that makes it as if a and b were the same variable.
  43    Initialising the RnEnv2, so that it can generate a fresh
  44    binder when necessary, entails knowing the free variables of
  45    both types.
  46
  47 3. We must be careful not to bind a template type variable to a
  48    locally bound variable.  E.g.
  49         (forall a. x) ~ (forall b. b)
  50    where x is the template type variable.  Then we do not want to
  51    bind x to a/b!  This is a kind of occurs check.
  52    The necessary locals accumulate in the RnEnv2.
  53
  54
  55 \begin{code}
  56 data MatchEnv
  57   = ME  { me_tmpls :: VarSet    -- Template tyvars
  58         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
  59         }                       --   In-scope set includes template tyvars
  60
  61 tcMatchTy :: TyVarSet           -- Template tyvars
  62           -> Type               -- Template
  63           -> Type               -- Target
  64           -> Maybe TvSubst      -- One-shot; in principle the template
  65                                 -- variables could be free in the target
  66
  67 tcMatchTy tmpls ty1 ty2
  68   = case match menv emptyTvSubstEnv ty1 ty2 of
  69         Just subst_env -> Just (TvSubst in_scope subst_env)
  70         Nothing        -> Nothing
  71   where
  72     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
  73     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
  74         -- We're assuming that all the interesting
  75         -- tyvars in tys1 are in tmpls
  76
  77 tcMatchTys :: TyVarSet          -- Template tyvars
  78            -> [Type]            -- Template
  79            -> [Type]            -- Target
  80            -> Maybe TvSubst     -- One-shot; in principle the template
  81                                 -- variables could be free in the target
  82
  83 tcMatchTys tmpls tys1 tys2
  84   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
  85         Just subst_env -> Just (TvSubst in_scope subst_env)
  86         Nothing        -> Nothing
  87   where
  88     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
  89     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
  90         -- We're assuming that all the interesting
  91         -- tyvars in tys1 are in tmpls
  92
  93 -- This is similar, but extends a substitution
  94 tcMatchTyX :: TyVarSet          -- Template tyvars
  95            -> TvSubst           -- Substitution to extend
  96            -> Type              -- Template
  97            -> Type              -- Target
  98            -> Maybe TvSubst
  99 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
 100   = case match menv subst_env ty1 ty2 of
 101         Just subst_env -> Just (TvSubst in_scope subst_env)
 102         Nothing        -> Nothing
 103   where
 104     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
 105
 106 tcMatchPreds
 107         :: [TyVar]                      -- Bind these
 108         -> [PredType] -> [PredType]
 109         -> Maybe TvSubstEnv
 110 tcMatchPreds tmpls ps1 ps2
 111   = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
 112   where
 113     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
 114     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
 115
 116 -- This one is called from the expression matcher, which already has a MatchEnv in hand
 117 ruleMatchTyX :: MatchEnv
 118          -> TvSubstEnv          -- Substitution to extend
 119          -> Type                -- Template
 120          -> Type                -- Target
 121          -> Maybe TvSubstEnv
 122
 123 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
 124 \end{code}
 125
 126 Now the internals of matching
 127
 128 \begin{code}
 129 match :: MatchEnv       -- For the most part this is pushed downwards
 130       -> TvSubstEnv     -- Substitution so far:
 131                         --   Domain is subset of template tyvars
 132                         --   Free vars of range is subset of
 133                         --      in-scope set of the RnEnv2
 134       -> Type -> Type   -- Template and target respectively
 135       -> Maybe TvSubstEnv
 136 -- This matcher works on source types; that is,
 137 -- it respects NewTypes and PredType
 138
 139 match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2
 140                           | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
 141
 142 match menv subst (TyVarTy tv1) ty2
 143   | tv1' `elemVarSet` me_tmpls menv
 144   = case lookupVarEnv subst tv1' of
 145         Nothing         -- No existing binding
 146             | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
 147             -> Nothing  -- Occurs check
 148             | not (typeKind ty2 `isSubKind` tyVarKind tv1)
 149             -> Nothing  -- Kind mis-match
 150             | otherwise
 151             -> Just (extendVarEnv subst tv1' ty2)
 152
 153         Just ty1'       -- There is an existing binding; check whether ty2 matches it
 154             | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
 155                 -- ty1 has no locally-bound variables, hence nukeRnEnvL
 156                 -- Note tcEqType...we are doing source-type matching here
 157             -> Just subst
 158             | otherwise -> Nothing      -- ty2 doesn't match
 159
 160
 161    | otherwise  -- tv1 is not a template tyvar
 162    = case ty2 of
 163         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
 164         other                                   -> Nothing
 165   where
 166     rn_env = me_env menv
 167     tv1' = rnOccL rn_env tv1
 168
 169 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
 170   = match menv' subst ty1 ty2
 171   where         -- Use the magic of rnBndr2 to go under the binders
 172     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
 173
 174 match menv subst (PredTy p1) (PredTy p2)
 175   = match_pred menv subst p1 p2
 176 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 177   | tc1 == tc2 = match_tys menv subst tys1 tys2
 178 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 179   = do { subst' <- match menv subst ty1a ty2a
 180        ; match menv subst' ty1b ty2b }
 181 match menv subst (AppTy ty1a ty1b) ty2
 182   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 183         -- 'repSplit' used because the tcView stuff is done above
 184   = do { subst' <- match menv subst ty1a ty2a
 185        ; match menv subst' ty1b ty2b }
 186
 187 match menv subst ty1 ty2
 188   = Nothing
 189
 190 --------------
 191 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
 192
 193 --------------
 194 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
 195            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
 196 match_list fn subst []         []         = Just subst
 197 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
 198                                                 ; match_list fn subst' tys1 tys2 }
 199 match_list fn subst tys1       tys2       = Nothing
 200
 201 --------------
 202 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
 203   | c1 == c2 = match_tys menv subst tys1 tys2
 204 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
 205   | n1 == n2 = match menv subst t1 t2
 206 match_pred menv subst p1 p2 = Nothing
 207 \end{code}
 208
 209