compiler/types/Unify.lhs

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