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