compiler/types/Unify.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 \begin{code}
   6 {-# OPTIONS -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/Commentary/CodingStyle#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 Coercion
  30 import TyCon
  31 import DataCon
  32 import TypeRep
  33 import Outputable
  34 import Util
  35 import Maybes
  36 \end{code}
  37
  38
  39 %************************************************************************
  40 %*                                                                      *
  41                 Matching
  42 %*                                                                      *
  43 %************************************************************************
  44
  45
  46 Matching is much tricker than you might think.
  47
  48 1. The substitution we generate binds the *template type variables*
  49    which are given to us explicitly.
  50
  51 2. We want to match in the presence of foralls;
  52         e.g     (forall a. t1) ~ (forall b. t2)
  53
  54    That is what the RnEnv2 is for; it does the alpha-renaming
  55    that makes it as if a and b were the same variable.
  56    Initialising the RnEnv2, so that it can generate a fresh
  57    binder when necessary, entails knowing the free variables of
  58    both types.
  59
  60 3. We must be careful not to bind a template type variable to a
  61    locally bound variable.  E.g.
  62         (forall a. x) ~ (forall b. b)
  63    where x is the template type variable.  Then we do not want to
  64    bind x to a/b!  This is a kind of occurs check.
  65    The necessary locals accumulate in the RnEnv2.
  66
  67
  68 \begin{code}
  69 data MatchEnv
  70   = ME  { me_tmpls :: VarSet    -- Template tyvars
  71         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
  72         }                       --   In-scope set includes template tyvars
  73
  74 tcMatchTy :: TyVarSet           -- Template tyvars
  75           -> Type               -- Template
  76           -> Type               -- Target
  77           -> Maybe TvSubst      -- One-shot; in principle the template
  78                                 -- variables could be free in the target
  79
  80 tcMatchTy tmpls ty1 ty2
  81   = case match menv emptyTvSubstEnv 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     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
  87         -- We're assuming that all the interesting
  88         -- tyvars in tys1 are in tmpls
  89
  90 tcMatchTys :: TyVarSet          -- Template tyvars
  91            -> [Type]            -- Template
  92            -> [Type]            -- Target
  93            -> Maybe TvSubst     -- One-shot; in principle the template
  94                                 -- variables could be free in the target
  95
  96 tcMatchTys tmpls tys1 tys2
  97   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
  98         Just subst_env -> Just (TvSubst in_scope subst_env)
  99         Nothing        -> Nothing
 100   where
 101     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
 102     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
 103         -- We're assuming that all the interesting
 104         -- tyvars in tys1 are in tmpls
 105
 106 -- This is similar, but extends a substitution
 107 tcMatchTyX :: TyVarSet          -- Template tyvars
 108            -> TvSubst           -- Substitution to extend
 109            -> Type              -- Template
 110            -> Type              -- Target
 111            -> Maybe TvSubst
 112 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
 113   = case match menv subst_env ty1 ty2 of
 114         Just subst_env -> Just (TvSubst in_scope subst_env)
 115         Nothing        -> Nothing
 116   where
 117     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
 118
 119 tcMatchPreds
 120         :: [TyVar]                      -- Bind these
 121         -> [PredType] -> [PredType]
 122         -> Maybe TvSubstEnv
 123 tcMatchPreds tmpls ps1 ps2
 124   = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
 125   where
 126     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
 127     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
 128
 129 -- This one is called from the expression matcher, which already has a MatchEnv in hand
 130 ruleMatchTyX :: MatchEnv
 131          -> TvSubstEnv          -- Substitution to extend
 132          -> Type                -- Template
 133          -> Type                -- Target
 134          -> Maybe TvSubstEnv
 135
 136 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
 137 \end{code}
 138
 139 Now the internals of matching
 140
 141 \begin{code}
 142 match :: MatchEnv       -- For the most part this is pushed downwards
 143       -> TvSubstEnv     -- Substitution so far:
 144                         --   Domain is subset of template tyvars
 145                         --   Free vars of range is subset of
 146                         --      in-scope set of the RnEnv2
 147       -> Type -> Type   -- Template and target respectively
 148       -> Maybe TvSubstEnv
 149 -- This matcher works on source types; that is,
 150 -- it respects NewTypes and PredType
 151
 152 match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2
 153                          | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
 154
 155 match menv subst (TyVarTy tv1) ty2
 156   | tv1' `elemVarSet` me_tmpls menv
 157   = case lookupVarEnv subst tv1' of
 158         Nothing         -- No existing binding
 159             | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
 160             -> Nothing  -- Occurs check
 161             | otherwise
 162             -> do { subst1 <- match_kind menv subst tv1 ty2
 163                   ; return (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_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
 204 -- Match the kind of the template tyvar with the kind of Type
 205 -- Note [Matching kinds]
 206 match_kind menv subst tv ty
 207   | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
 208                           (ty3,ty4) = coercionKind ty
 209                     ; subst1 <- match menv subst ty1 ty3
 210                     ; match menv subst1 ty2 ty4 }
 211   | otherwise  = if typeKind ty `isSubKind` tyVarKind tv
 212                  then Just subst
 213                  else Nothing
 214
 215 -- Note [Matching kinds]
 216 -- ~~~~~~~~~~~~~~~~~~~~~
 217 -- For ordinary type variables, we don't want (m a) to match (n b)
 218 -- if say (a::*) and (b::*->*).  This is just a yes/no issue.
 219 --
 220 -- For coercion kinds matters are more complicated.  If we have a
 221 -- coercion template variable co::a~[b], where a,b are presumably also
 222 -- template type variables, then we must match co's kind against the
 223 -- kind of the actual argument, so as to give bindings to a,b.
 224 --
 225 -- In fact I have no example in mind that *requires* this kind-matching
 226 -- to instantiate template type variables, but it seems like the right
 227 -- thing to do.  C.f. Note [Matching variable types] in Rules.lhs
 228
 229 --------------
 230 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
 231
 232 --------------
 233 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
 234            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
 235 match_list fn subst []         []         = Just subst
 236 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
 237                                                 ; match_list fn subst' tys1 tys2 }
 238 match_list fn subst tys1       tys2       = Nothing
 239
 240 --------------
 241 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
 242   | c1 == c2 = match_tys menv subst tys1 tys2
 243 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
 244   | n1 == n2 = match menv subst t1 t2
 245 match_pred menv subst p1 p2 = Nothing
 246 \end{code}
 247
 248
 249 %************************************************************************
 250 %*                                                                      *
 251                 GADTs
 252 %*                                                                      *
 253 %************************************************************************
 254
 255 Note [Pruning dead case alternatives]
 256 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 257 Consider        data T a where
 258                    T1 :: T Int
 259                    T2 :: T a
 260
 261                 newtype X = MkX Int
 262                 newtype Y = MkY Char
 263
 264                 type family F a
 265                 type instance F Bool = Int
 266
 267 Now consider    case x of { T1 -> e1; T2 -> e2 }
 268
 269 The question before the house is this: if I know something about the type
 270 of x, can I prune away the T1 alternative?
 271
 272 Suppose x::T Char.  It's impossible to construct a (T Char) using T1,
 273         Answer = YES (clearly)
 274
 275 Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
 276 to 'Bool', in which case x::T Int, so
 277         ANSWER = NO (clearly)
 278
 279 Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom)
 280 value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
 281 gives a coercion
 282         CoX :: X ~ Int
 283 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
 284 of type (T X) constructed with T1.  Hence
 285         ANSWER = NO (surprisingly)
 286
 287 Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
 288 mechanism uses a cast, just as above, to move from one dictionary to another,
 289 in effect giving the programmer access to CoX.
 290
 291 Finally, suppose x::T Y.  Then *even in FC* we can't construct a
 292 non-bottom value of type (T Y) using T1.  That's because we can get
 293 from Y to Char, but not to Int.
 294
 295
 296 Here's a related question.      data Eq a b where EQ :: Eq a a
 297 Consider
 298         case x of { EQ -> ... }
 299
 300 Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
 301
 302 What about x::Eq Int a, in a context where we have evidence that a~Char.
 303 Then again the alternative is dead.
 304
 305
 306                         Summary
 307
 308 We are really doing a test for unsatisfiability of the type
 309 constraints implied by the match. And that is clearly, in general, a
 310 hard thing to do.
 311
 312 However, since we are simply dropping dead code, a conservative test
 313 suffices.  There is a continuum of tests, ranging from easy to hard, that
 314 drop more and more dead code.
 315
 316 For now we implement a very simple test: type variables match
 317 anything, type functions (incl newtypes) match anything, and only
 318 distinct data types fail to match.  We can elaborate later.
 319
 320 \begin{code}
 321 dataConCannotMatch :: [Type] -> DataCon -> Bool
 322 -- Returns True iff the data con *definitely cannot* match a
 323 --                  scrutinee of type (T tys)
 324 --                  where T is the type constructor for the data con
 325 --
 326 dataConCannotMatch tys con
 327   | null eq_spec      = False   -- Common
 328   | all isTyVarTy tys = False   -- Also common
 329   | otherwise
 330   = cant_match_s (map (substTyVar subst . fst) eq_spec)
 331                  (map snd eq_spec)
 332   where
 333     dc_tvs  = dataConUnivTyVars con
 334     eq_spec = dataConEqSpec con
 335     subst   = zipTopTvSubst dc_tvs tys
 336
 337     cant_match_s :: [Type] -> [Type] -> Bool
 338     cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
 339                              or (zipWith cant_match tys1 tys2)
 340
 341     cant_match :: Type -> Type -> Bool
 342     cant_match t1 t2
 343         | Just t1' <- coreView t1 = cant_match t1' t2
 344         | Just t2' <- coreView t2 = cant_match t1 t2'
 345
 346     cant_match (FunTy a1 r1) (FunTy a2 r2)
 347         = cant_match a1 a2 || cant_match r1 r2
 348
 349     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 350         | isDataTyCon tc1 && isDataTyCon tc2
 351         = tc1 /= tc2 || cant_match_s tys1 tys2
 352
 353     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
 354     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
 355         -- tc can't be FunTyCon by invariant
 356
 357     cant_match (AppTy f1 a1) ty2
 358         | Just (f2, a2) <- repSplitAppTy_maybe ty2
 359         = cant_match f1 f2 || cant_match a1 a2
 360     cant_match ty1 (AppTy f2 a2)
 361         | Just (f1, a1) <- repSplitAppTy_maybe ty1
 362         = cant_match f1 f2 || cant_match a1 a2
 363
 364     cant_match ty1 ty2 = False  -- Safe!
 365
 366 -- Things we could add;
 367 --      foralls
 368 --      look through newtypes
 369 --      take account of tyvar bindings (EQ example above)
 370 \end{code}