compiler/types/Unify.lhs

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