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
  13         dataConCannotMatch
  14    ) where
  15
  16 #include "HsVersions.h"
  17
  18 import Var
  19 import VarEnv
  20 import VarSet
  21 import Type
  22 import TyCon
  23 import DataCon
  24 import TypeRep
  25 import Outputable
  26 import Util
  27 import Maybes
  28 \end{code}
  29
  30
  31 %************************************************************************
  32 %*                                                                      *
  33                 Matching
  34 %*                                                                      *
  35 %************************************************************************
  36
  37
  38 Matching is much tricker than you might think.
  39
  40 1. The substitution we generate binds the *template type variables*
  41    which are given to us explicitly.
  42
  43 2. We want to match in the presence of foralls;
  44         e.g     (forall a. t1) ~ (forall b. t2)
  45
  46    That is what the RnEnv2 is for; it does the alpha-renaming
  47    that makes it as if a and b were the same variable.
  48    Initialising the RnEnv2, so that it can generate a fresh
  49    binder when necessary, entails knowing the free variables of
  50    both types.
  51
  52 3. We must be careful not to bind a template type variable to a
  53    locally bound variable.  E.g.
  54         (forall a. x) ~ (forall b. b)
  55    where x is the template type variable.  Then we do not want to
  56    bind x to a/b!  This is a kind of occurs check.
  57    The necessary locals accumulate in the RnEnv2.
  58
  59
  60 \begin{code}
  61 data MatchEnv
  62   = ME  { me_tmpls :: VarSet    -- Template tyvars
  63         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
  64         }                       --   In-scope set includes template tyvars
  65
  66 tcMatchTy :: TyVarSet           -- Template tyvars
  67           -> Type               -- Template
  68           -> Type               -- Target
  69           -> Maybe TvSubst      -- One-shot; in principle the template
  70                                 -- variables could be free in the target
  71
  72 tcMatchTy tmpls ty1 ty2
  73   = case match menv emptyTvSubstEnv ty1 ty2 of
  74         Just subst_env -> Just (TvSubst in_scope subst_env)
  75         Nothing        -> Nothing
  76   where
  77     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
  78     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
  79         -- We're assuming that all the interesting
  80         -- tyvars in tys1 are in tmpls
  81
  82 tcMatchTys :: TyVarSet          -- Template tyvars
  83            -> [Type]            -- Template
  84            -> [Type]            -- Target
  85            -> Maybe TvSubst     -- One-shot; in principle the template
  86                                 -- variables could be free in the target
  87
  88 tcMatchTys tmpls tys1 tys2
  89   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
  90         Just subst_env -> Just (TvSubst in_scope subst_env)
  91         Nothing        -> Nothing
  92   where
  93     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
  94     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
  95         -- We're assuming that all the interesting
  96         -- tyvars in tys1 are in tmpls
  97
  98 -- This is similar, but extends a substitution
  99 tcMatchTyX :: TyVarSet          -- Template tyvars
 100            -> TvSubst           -- Substitution to extend
 101            -> Type              -- Template
 102            -> Type              -- Target
 103            -> Maybe TvSubst
 104 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
 105   = case match menv subst_env ty1 ty2 of
 106         Just subst_env -> Just (TvSubst in_scope subst_env)
 107         Nothing        -> Nothing
 108   where
 109     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
 110
 111 tcMatchPreds
 112         :: [TyVar]                      -- Bind these
 113         -> [PredType] -> [PredType]
 114         -> Maybe TvSubstEnv
 115 tcMatchPreds tmpls ps1 ps2
 116   = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
 117   where
 118     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
 119     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
 120
 121 -- This one is called from the expression matcher, which already has a MatchEnv in hand
 122 ruleMatchTyX :: MatchEnv
 123          -> TvSubstEnv          -- Substitution to extend
 124          -> Type                -- Template
 125          -> Type                -- Target
 126          -> Maybe TvSubstEnv
 127
 128 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
 129 \end{code}
 130
 131 Now the internals of matching
 132
 133 \begin{code}
 134 match :: MatchEnv       -- For the most part this is pushed downwards
 135       -> TvSubstEnv     -- Substitution so far:
 136                         --   Domain is subset of template tyvars
 137                         --   Free vars of range is subset of
 138                         --      in-scope set of the RnEnv2
 139       -> Type -> Type   -- Template and target respectively
 140       -> Maybe TvSubstEnv
 141 -- This matcher works on source types; that is,
 142 -- it respects NewTypes and PredType
 143
 144 match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2
 145                           | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
 146
 147 match menv subst (TyVarTy tv1) ty2
 148   | tv1' `elemVarSet` me_tmpls menv
 149   = case lookupVarEnv subst tv1' of
 150         Nothing         -- No existing binding
 151             | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
 152             -> Nothing  -- Occurs check
 153             | not (typeKind ty2 `isSubKind` tyVarKind tv1)
 154             -> Nothing  -- Kind mis-match
 155             | otherwise
 156             -> Just (extendVarEnv subst tv1' ty2)
 157
 158         Just ty1'       -- There is an existing binding; check whether ty2 matches it
 159             | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
 160                 -- ty1 has no locally-bound variables, hence nukeRnEnvL
 161                 -- Note tcEqType...we are doing source-type matching here
 162             -> Just subst
 163             | otherwise -> Nothing      -- ty2 doesn't match
 164
 165
 166    | otherwise  -- tv1 is not a template tyvar
 167    = case ty2 of
 168         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
 169         other                                   -> Nothing
 170   where
 171     rn_env = me_env menv
 172     tv1' = rnOccL rn_env tv1
 173
 174 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
 175   = match menv' subst ty1 ty2
 176   where         -- Use the magic of rnBndr2 to go under the binders
 177     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
 178
 179 match menv subst (PredTy p1) (PredTy p2)
 180   = match_pred menv subst p1 p2
 181 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 182   | tc1 == tc2 = match_tys menv subst tys1 tys2
 183 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 184   = do { subst' <- match menv subst ty1a ty2a
 185        ; match menv subst' ty1b ty2b }
 186 match menv subst (AppTy ty1a ty1b) ty2
 187   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 188         -- 'repSplit' used because the tcView stuff is done above
 189   = do { subst' <- match menv subst ty1a ty2a
 190        ; match menv subst' ty1b ty2b }
 191
 192 match menv subst ty1 ty2
 193   = Nothing
 194
 195 --------------
 196 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
 197
 198 --------------
 199 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
 200            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
 201 match_list fn subst []         []         = Just subst
 202 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
 203                                                 ; match_list fn subst' tys1 tys2 }
 204 match_list fn subst tys1       tys2       = Nothing
 205
 206 --------------
 207 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
 208   | c1 == c2 = match_tys menv subst tys1 tys2
 209 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
 210   | n1 == n2 = match menv subst t1 t2
 211 match_pred menv subst p1 p2 = Nothing
 212 \end{code}
 213
 214
 215 %************************************************************************
 216 %*                                                                      *
 217                 GADTs
 218 %*                                                                      *
 219 %************************************************************************
 220
 221 Note [Pruning dead case alternatives]
 222 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 223 Consider        data T a where
 224                    T1 :: T Int
 225                    T2 :: T a
 226
 227                 newtype X = MkX Int
 228                 newtype Y = MkY Char
 229
 230                 type family F a
 231                 type instance F Bool = Int
 232
 233 Now consider    case x of { T1 -> e1; T2 -> e2 }
 234
 235 The question before the house is this: if I know something about the type
 236 of x, can I prune away the T1 alternative?
 237
 238 Suppose x::T Char.  It's impossible to construct a (T Char) using T1,
 239         Answer = YES (clearly)
 240
 241 Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
 242 to 'Bool', in which case x::T Int, so
 243         ANSWER = NO (clearly)
 244
 245 Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom)
 246 value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
 247 gives a coercion
 248         CoX :: X ~ Int
 249 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
 250 of type (T X) constructed with T1.  Hence
 251         ANSWER = NO (surprisingly)
 252
 253 Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
 254 mechanism uses a cast, just as above, to move from one dictionary to another,
 255 in effect giving the programmer access to CoX.
 256
 257 Finally, suppose x::T Y.  Then *even in FC* we can't construct a
 258 non-bottom value of type (T Y) using T1.  That's because we can get
 259 from Y to Char, but not to Int.
 260
 261
 262 Here's a related question.      data Eq a b where EQ :: Eq a a
 263 Consider
 264         case x of { EQ -> ... }
 265
 266 Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
 267
 268 What about x::Eq Int a, in a context where we have evidence that a~Char.
 269 Then again the alternative is dead.
 270
 271
 272                         Summary
 273
 274 We are really doing a test for unsatisfiability of the type
 275 constraints implied by the match. And that is clearly, in general, a
 276 hard thing to do.
 277
 278 However, since we are simply dropping dead code, a conservative test
 279 suffices.  There is a continuum of tests, ranging from easy to hard, that
 280 drop more and more dead code.
 281
 282 For now we implement a very simple test: type variables match
 283 anything, type functions (incl newtypes) match anything, and only
 284 distinct data types fail to match.  We can elaborate later.
 285
 286 \begin{code}
 287 dataConCannotMatch :: [Type] -> DataCon -> Bool
 288 -- Returns True iff the data con *definitely cannot* match a
 289 --                  scrutinee of type (T tys)
 290 --                  where T is the type constructor for the data con
 291 --
 292 dataConCannotMatch tys con
 293   | null eq_spec      = False   -- Common
 294   | all isTyVarTy tys = False   -- Also common
 295   | otherwise
 296   = cant_match_s (map (substTyVar subst . fst) eq_spec)
 297                  (map snd eq_spec)
 298   where
 299     dc_tvs  = dataConUnivTyVars con
 300     eq_spec = dataConEqSpec con
 301     subst   = zipTopTvSubst dc_tvs tys
 302
 303     cant_match_s :: [Type] -> [Type] -> Bool
 304     cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
 305                              or (zipWith cant_match tys1 tys2)
 306
 307     cant_match :: Type -> Type -> Bool
 308     cant_match t1 t2
 309         | Just t1' <- coreView t1 = cant_match t1' t2
 310         | Just t2' <- coreView t2 = cant_match t1 t2'
 311
 312     cant_match (FunTy a1 r1) (FunTy a2 r2)
 313         = cant_match a1 a2 || cant_match r1 r2
 314
 315     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 316         | isDataTyCon tc1 && isDataTyCon tc2
 317         = tc1 /= tc2 || cant_match_s tys1 tys2
 318
 319     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
 320     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
 321         -- tc can't be FunTyCon by invariant
 322
 323     cant_match (AppTy f1 a1) ty2
 324         | Just (f2, a2) <- repSplitAppTy_maybe ty2
 325         = cant_match f1 f2 || cant_match a1 a2
 326     cant_match ty1 (AppTy f2 a2)
 327         | Just (f1, a1) <- repSplitAppTy_maybe ty1
 328         = cant_match f1 f2 || cant_match a1 a2
 329
 330     cant_match ty1 ty2 = False  -- Safe!
 331
 332 -- Things we could add;
 333 --      foralls
 334 --      look through newtypes
 335 --      take account of tyvar bindings (EQ example above)
 336 \end{code}