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 core types; that is, it ignores PredTypes
 150 -- Watch out if newtypes become transparent agin!
 151 --      this matcher must respect newtypes
 152
 153 match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
 154                          | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
 155
 156 match menv subst (TyVarTy tv1) ty2
 157   | tv1' `elemVarSet` me_tmpls menv
 158   = case lookupVarEnv subst tv1' of
 159         Nothing         -- No existing binding
 160             | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
 161             -> Nothing  -- Occurs check
 162             | otherwise
 163             -> do { subst1 <- match_kind menv subst tv1 ty2
 164                   ; return (extendVarEnv subst tv1' ty2) }
 165
 166         Just ty1'       -- There is an existing binding; check whether ty2 matches it
 167             | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
 168                 -- ty1 has no locally-bound variables, hence nukeRnEnvL
 169                 -- Note tcEqType...we are doing source-type matching here
 170             -> Just subst
 171             | otherwise -> Nothing      -- ty2 doesn't match
 172
 173
 174    | otherwise  -- tv1 is not a template tyvar
 175    = case ty2 of
 176         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
 177         other                                   -> Nothing
 178   where
 179     rn_env = me_env menv
 180     tv1' = rnOccL rn_env tv1
 181
 182 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
 183   = match menv' subst ty1 ty2
 184   where         -- Use the magic of rnBndr2 to go under the binders
 185     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
 186
 187 match menv subst (PredTy p1) (PredTy p2)
 188   = match_pred menv subst p1 p2
 189 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 190   | tc1 == tc2 = match_tys menv subst tys1 tys2
 191 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 192   = do { subst' <- match menv subst ty1a ty2a
 193        ; match menv subst' ty1b ty2b }
 194 match menv subst (AppTy ty1a ty1b) ty2
 195   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 196         -- 'repSplit' used because the tcView stuff is done above
 197   = do { subst' <- match menv subst ty1a ty2a
 198        ; match menv subst' ty1b ty2b }
 199
 200 match menv subst ty1 ty2
 201   = Nothing
 202
 203 --------------
 204 match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
 205 -- Match the kind of the template tyvar with the kind of Type
 206 -- Note [Matching kinds]
 207 match_kind menv subst tv ty
 208   | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
 209                           (ty3,ty4) = coercionKind ty
 210                     ; subst1 <- match menv subst ty1 ty3
 211                     ; match menv subst1 ty2 ty4 }
 212   | otherwise  = if typeKind ty `isSubKind` tyVarKind tv
 213                  then Just subst
 214                  else Nothing
 215
 216 -- Note [Matching kinds]
 217 -- ~~~~~~~~~~~~~~~~~~~~~
 218 -- For ordinary type variables, we don't want (m a) to match (n b)
 219 -- if say (a::*) and (b::*->*).  This is just a yes/no issue.
 220 --
 221 -- For coercion kinds matters are more complicated.  If we have a
 222 -- coercion template variable co::a~[b], where a,b are presumably also
 223 -- template type variables, then we must match co's kind against the
 224 -- kind of the actual argument, so as to give bindings to a,b.
 225 --
 226 -- In fact I have no example in mind that *requires* this kind-matching
 227 -- to instantiate template type variables, but it seems like the right
 228 -- thing to do.  C.f. Note [Matching variable types] in Rules.lhs
 229
 230 --------------
 231 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
 232
 233 --------------
 234 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
 235            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
 236 match_list fn subst []         []         = Just subst
 237 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
 238                                                 ; match_list fn subst' tys1 tys2 }
 239 match_list fn subst tys1       tys2       = Nothing
 240
 241 --------------
 242 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
 243   | c1 == c2 = match_tys menv subst tys1 tys2
 244 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
 245   | n1 == n2 = match menv subst t1 t2
 246 match_pred menv subst p1 p2 = Nothing
 247 \end{code}
 248
 249
 250 %************************************************************************
 251 %*                                                                      *
 252                 GADTs
 253 %*                                                                      *
 254 %************************************************************************
 255
 256 Note [Pruning dead case alternatives]
 257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 258 Consider        data T a where
 259                    T1 :: T Int
 260                    T2 :: T a
 261
 262                 newtype X = MkX Int
 263                 newtype Y = MkY Char
 264
 265                 type family F a
 266                 type instance F Bool = Int
 267
 268 Now consider    case x of { T1 -> e1; T2 -> e2 }
 269
 270 The question before the house is this: if I know something about the type
 271 of x, can I prune away the T1 alternative?
 272
 273 Suppose x::T Char.  It's impossible to construct a (T Char) using T1,
 274         Answer = YES (clearly)
 275
 276 Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
 277 to 'Bool', in which case x::T Int, so
 278         ANSWER = NO (clearly)
 279
 280 Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom)
 281 value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
 282 gives a coercion
 283         CoX :: X ~ Int
 284 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
 285 of type (T X) constructed with T1.  Hence
 286         ANSWER = NO (surprisingly)
 287
 288 Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
 289 mechanism uses a cast, just as above, to move from one dictionary to another,
 290 in effect giving the programmer access to CoX.
 291
 292 Finally, suppose x::T Y.  Then *even in FC* we can't construct a
 293 non-bottom value of type (T Y) using T1.  That's because we can get
 294 from Y to Char, but not to Int.
 295
 296
 297 Here's a related question.      data Eq a b where EQ :: Eq a a
 298 Consider
 299         case x of { EQ -> ... }
 300
 301 Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
 302
 303 What about x::Eq Int a, in a context where we have evidence that a~Char.
 304 Then again the alternative is dead.
 305
 306
 307                         Summary
 308
 309 We are really doing a test for unsatisfiability of the type
 310 constraints implied by the match. And that is clearly, in general, a
 311 hard thing to do.
 312
 313 However, since we are simply dropping dead code, a conservative test
 314 suffices.  There is a continuum of tests, ranging from easy to hard, that
 315 drop more and more dead code.
 316
 317 For now we implement a very simple test: type variables match
 318 anything, type functions (incl newtypes) match anything, and only
 319 distinct data types fail to match.  We can elaborate later.
 320
 321 \begin{code}
 322 dataConCannotMatch :: [Type] -> DataCon -> Bool
 323 -- Returns True iff the data con *definitely cannot* match a
 324 --                  scrutinee of type (T tys)
 325 --                  where T is the type constructor for the data con
 326 --
 327 dataConCannotMatch tys con
 328   | null eq_spec      = False   -- Common
 329   | all isTyVarTy tys = False   -- Also common
 330   | otherwise
 331   = cant_match_s (map (substTyVar subst . fst) eq_spec)
 332                  (map snd eq_spec)
 333   where
 334     dc_tvs  = dataConUnivTyVars con
 335     eq_spec = dataConEqSpec con
 336     subst   = zipTopTvSubst dc_tvs tys
 337
 338     cant_match_s :: [Type] -> [Type] -> Bool
 339     cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
 340                              or (zipWith cant_match tys1 tys2)
 341
 342     cant_match :: Type -> Type -> Bool
 343     cant_match t1 t2
 344         | Just t1' <- coreView t1 = cant_match t1' t2
 345         | Just t2' <- coreView t2 = cant_match t1 t2'
 346
 347     cant_match (FunTy a1 r1) (FunTy a2 r2)
 348         = cant_match a1 a2 || cant_match r1 r2
 349
 350     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 351         | isDataTyCon tc1 && isDataTyCon tc2
 352         = tc1 /= tc2 || cant_match_s tys1 tys2
 353
 354     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
 355     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
 356         -- tc can't be FunTyCon by invariant
 357
 358     cant_match (AppTy f1 a1) ty2
 359         | Just (f2, a2) <- repSplitAppTy_maybe ty2
 360         = cant_match f1 f2 || cant_match a1 a2
 361     cant_match ty1 (AppTy f2 a2)
 362         | Just (f1, a1) <- repSplitAppTy_maybe ty1
 363         = cant_match f1 f2 || cant_match a1 a2
 364
 365     cant_match ty1 ty2 = False  -- Safe!
 366
 367 -- Things we could add;
 368 --      foralls
 369 --      look through newtypes
 370 --      take account of tyvar bindings (EQ example above)
 371 \end{code}