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