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