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
  15         -- GADT type refinement
  16         Refinement, emptyRefinement, isEmptyRefinement,
  17         matchRefine, refineType, refinePred, refineResType,
  18
  19         -- side-effect free unification
  20         tcUnifyTys, BindFlag(..)
  21
  22    ) where
  23
  24 #include "HsVersions.h"
  25
  26 import Var
  27 import VarEnv
  28 import VarSet
  29 import Type
  30 import Coercion
  31 import TyCon
  32 import DataCon
  33 import TypeRep
  34 import Outputable
  35 import ErrUtils
  36 import Util
  37 import Maybes
  38 import UniqFM
  39 import FastString
  40 \end{code}
  41
  42
  43 %************************************************************************
  44 %*                                                                      *
  45                 Matching
  46 %*                                                                      *
  47 %************************************************************************
  48
  49
  50 Matching is much tricker than you might think.
  51
  52 1. The substitution we generate binds the *template type variables*
  53    which are given to us explicitly.
  54
  55 2. We want to match in the presence of foralls;
  56         e.g     (forall a. t1) ~ (forall b. t2)
  57
  58    That is what the RnEnv2 is for; it does the alpha-renaming
  59    that makes it as if a and b were the same variable.
  60    Initialising the RnEnv2, so that it can generate a fresh
  61    binder when necessary, entails knowing the free variables of
  62    both types.
  63
  64 3. We must be careful not to bind a template type variable to a
  65    locally bound variable.  E.g.
  66         (forall a. x) ~ (forall b. b)
  67    where x is the template type variable.  Then we do not want to
  68    bind x to a/b!  This is a kind of occurs check.
  69    The necessary locals accumulate in the RnEnv2.
  70
  71
  72 \begin{code}
  73 data MatchEnv
  74   = ME  { me_tmpls :: VarSet    -- Template tyvars
  75         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
  76         }                       --   In-scope set includes template tyvars
  77
  78 tcMatchTy :: TyVarSet           -- Template tyvars
  79           -> Type               -- Template
  80           -> Type               -- Target
  81           -> Maybe TvSubst      -- One-shot; in principle the template
  82                                 -- variables could be free in the target
  83
  84 tcMatchTy tmpls ty1 ty2
  85   = case match menv emptyTvSubstEnv ty1 ty2 of
  86         Just subst_env -> Just (TvSubst in_scope subst_env)
  87         Nothing        -> Nothing
  88   where
  89     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
  90     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
  91         -- We're assuming that all the interesting
  92         -- tyvars in tys1 are in tmpls
  93
  94 tcMatchTys :: TyVarSet          -- Template tyvars
  95            -> [Type]            -- Template
  96            -> [Type]            -- Target
  97            -> Maybe TvSubst     -- One-shot; in principle the template
  98                                 -- variables could be free in the target
  99
 100 tcMatchTys tmpls tys1 tys2
 101   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
 102         Just subst_env -> Just (TvSubst in_scope subst_env)
 103         Nothing        -> Nothing
 104   where
 105     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
 106     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
 107         -- We're assuming that all the interesting
 108         -- tyvars in tys1 are in tmpls
 109
 110 -- This is similar, but extends a substitution
 111 tcMatchTyX :: TyVarSet          -- Template tyvars
 112            -> TvSubst           -- Substitution to extend
 113            -> Type              -- Template
 114            -> Type              -- Target
 115            -> Maybe TvSubst
 116 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
 117   = case match menv subst_env ty1 ty2 of
 118         Just subst_env -> Just (TvSubst in_scope subst_env)
 119         Nothing        -> Nothing
 120   where
 121     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
 122
 123 tcMatchPreds
 124         :: [TyVar]                      -- Bind these
 125         -> [PredType] -> [PredType]
 126         -> Maybe TvSubstEnv
 127 tcMatchPreds tmpls ps1 ps2
 128   = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
 129   where
 130     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
 131     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
 132
 133 -- This one is called from the expression matcher, which already has a MatchEnv in hand
 134 ruleMatchTyX :: MatchEnv
 135          -> TvSubstEnv          -- Substitution to extend
 136          -> Type                -- Template
 137          -> Type                -- Target
 138          -> Maybe TvSubstEnv
 139
 140 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
 141 \end{code}
 142
 143 Now the internals of matching
 144
 145 \begin{code}
 146 match :: MatchEnv       -- For the most part this is pushed downwards
 147       -> TvSubstEnv     -- Substitution so far:
 148                         --   Domain is subset of template tyvars
 149                         --   Free vars of range is subset of
 150                         --      in-scope set of the RnEnv2
 151       -> Type -> Type   -- Template and target respectively
 152       -> Maybe TvSubstEnv
 153 -- This matcher works on core types; that is, it ignores PredTypes
 154 -- Watch out if newtypes become transparent agin!
 155 --      this matcher must respect newtypes
 156
 157 match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
 158                          | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
 159
 160 match menv subst (TyVarTy tv1) ty2
 161   | tv1' `elemVarSet` me_tmpls menv
 162   = case lookupVarEnv subst tv1' of
 163         Nothing         -- No existing binding
 164             | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
 165             -> Nothing  -- Occurs check
 166             | otherwise
 167             -> do { subst1 <- match_kind menv subst tv1 ty2
 168                   ; return (extendVarEnv subst1 tv1' ty2) }
 169                         -- Note [Matching kinds]
 170
 171         Just ty1'       -- There is an existing binding; check whether ty2 matches it
 172             | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
 173                 -- ty1 has no locally-bound variables, hence nukeRnEnvL
 174                 -- Note tcEqType...we are doing source-type matching here
 175             -> Just subst
 176             | otherwise -> Nothing      -- ty2 doesn't match
 177
 178
 179    | otherwise  -- tv1 is not a template tyvar
 180    = case ty2 of
 181         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
 182         _                                       -> Nothing
 183   where
 184     rn_env = me_env menv
 185     tv1' = rnOccL rn_env tv1
 186
 187 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
 188   = match menv' subst ty1 ty2
 189   where         -- Use the magic of rnBndr2 to go under the binders
 190     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
 191
 192 match menv subst (PredTy p1) (PredTy p2)
 193   = match_pred menv subst p1 p2
 194 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 195   | tc1 == tc2 = match_tys menv subst tys1 tys2
 196 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 197   = do { subst' <- match menv subst ty1a ty2a
 198        ; match menv subst' ty1b ty2b }
 199 match menv subst (AppTy ty1a ty1b) ty2
 200   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 201         -- 'repSplit' used because the tcView stuff is done above
 202   = do { subst' <- match menv subst ty1a ty2a
 203        ; match menv subst' ty1b ty2b }
 204
 205 match _ _ _ _
 206   = Nothing
 207
 208 --------------
 209 match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
 210 -- Match the kind of the template tyvar with the kind of Type
 211 -- Note [Matching kinds]
 212 match_kind menv subst tv ty
 213   | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
 214                           (ty3,ty4) = coercionKind ty
 215                     ; subst1 <- match menv subst ty1 ty3
 216                     ; match menv subst1 ty2 ty4 }
 217   | otherwise  = if typeKind ty `isSubKind` tyVarKind tv
 218                  then Just subst
 219                  else Nothing
 220
 221 -- Note [Matching kinds]
 222 -- ~~~~~~~~~~~~~~~~~~~~~
 223 -- For ordinary type variables, we don't want (m a) to match (n b)
 224 -- if say (a::*) and (b::*->*).  This is just a yes/no issue.
 225 --
 226 -- For coercion kinds matters are more complicated.  If we have a
 227 -- coercion template variable co::a~[b], where a,b are presumably also
 228 -- template type variables, then we must match co's kind against the
 229 -- kind of the actual argument, so as to give bindings to a,b.
 230 --
 231 -- In fact I have no example in mind that *requires* this kind-matching
 232 -- to instantiate template type variables, but it seems like the right
 233 -- thing to do.  C.f. Note [Matching variable types] in Rules.lhs
 234
 235 --------------
 236 match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
 237 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
 238
 239 --------------
 240 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
 241            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
 242 match_list _  subst []         []         = Just subst
 243 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
 244                                                 ; match_list fn subst' tys1 tys2 }
 245 match_list _  _     _          _          = Nothing
 246
 247 --------------
 248 match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
 249 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
 250   | c1 == c2 = match_tys menv subst tys1 tys2
 251 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
 252   | n1 == n2 = match menv subst t1 t2
 253 match_pred _    _     _ _ = Nothing
 254 \end{code}
 255
 256
 257 %************************************************************************
 258 %*                                                                      *
 259                 GADTs
 260 %*                                                                      *
 261 %************************************************************************
 262
 263 Note [Pruning dead case alternatives]
 264 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 265 Consider        data T a where
 266                    T1 :: T Int
 267                    T2 :: T a
 268
 269                 newtype X = MkX Int
 270                 newtype Y = MkY Char
 271
 272                 type family F a
 273                 type instance F Bool = Int
 274
 275 Now consider    case x of { T1 -> e1; T2 -> e2 }
 276
 277 The question before the house is this: if I know something about the type
 278 of x, can I prune away the T1 alternative?
 279
 280 Suppose x::T Char.  It's impossible to construct a (T Char) using T1,
 281         Answer = YES (clearly)
 282
 283 Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
 284 to 'Bool', in which case x::T Int, so
 285         ANSWER = NO (clearly)
 286
 287 Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom)
 288 value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
 289 gives a coercion
 290         CoX :: X ~ Int
 291 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
 292 of type (T X) constructed with T1.  Hence
 293         ANSWER = NO (surprisingly)
 294
 295 Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
 296 mechanism uses a cast, just as above, to move from one dictionary to another,
 297 in effect giving the programmer access to CoX.
 298
 299 Finally, suppose x::T Y.  Then *even in FC* we can't construct a
 300 non-bottom value of type (T Y) using T1.  That's because we can get
 301 from Y to Char, but not to Int.
 302
 303
 304 Here's a related question.      data Eq a b where EQ :: Eq a a
 305 Consider
 306         case x of { EQ -> ... }
 307
 308 Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
 309
 310 What about x::Eq Int a, in a context where we have evidence that a~Char.
 311 Then again the alternative is dead.
 312
 313
 314                         Summary
 315
 316 We are really doing a test for unsatisfiability of the type
 317 constraints implied by the match. And that is clearly, in general, a
 318 hard thing to do.
 319
 320 However, since we are simply dropping dead code, a conservative test
 321 suffices.  There is a continuum of tests, ranging from easy to hard, that
 322 drop more and more dead code.
 323
 324 For now we implement a very simple test: type variables match
 325 anything, type functions (incl newtypes) match anything, and only
 326 distinct data types fail to match.  We can elaborate later.
 327
 328 \begin{code}
 329 dataConCannotMatch :: [Type] -> DataCon -> Bool
 330 -- Returns True iff the data con *definitely cannot* match a
 331 --                  scrutinee of type (T tys)
 332 --                  where T is the type constructor for the data con
 333 --
 334 dataConCannotMatch tys con
 335   | null eq_spec      = False   -- Common
 336   | all isTyVarTy tys = False   -- Also common
 337   | otherwise
 338   = cant_match_s (map (substTyVar subst . fst) eq_spec)
 339                  (map snd eq_spec)
 340   where
 341     dc_tvs  = dataConUnivTyVars con
 342     eq_spec = dataConEqSpec con
 343     subst   = zipTopTvSubst dc_tvs tys
 344
 345     cant_match_s :: [Type] -> [Type] -> Bool
 346     cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
 347                              or (zipWith cant_match tys1 tys2)
 348
 349     cant_match :: Type -> Type -> Bool
 350     cant_match t1 t2
 351         | Just t1' <- coreView t1 = cant_match t1' t2
 352         | Just t2' <- coreView t2 = cant_match t1 t2'
 353
 354     cant_match (FunTy a1 r1) (FunTy a2 r2)
 355         = cant_match a1 a2 || cant_match r1 r2
 356
 357     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 358         | isDataTyCon tc1 && isDataTyCon tc2
 359         = tc1 /= tc2 || cant_match_s tys1 tys2
 360
 361     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
 362     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
 363         -- tc can't be FunTyCon by invariant
 364
 365     cant_match (AppTy f1 a1) ty2
 366         | Just (f2, a2) <- repSplitAppTy_maybe ty2
 367         = cant_match f1 f2 || cant_match a1 a2
 368     cant_match ty1 (AppTy f2 a2)
 369         | Just (f1, a1) <- repSplitAppTy_maybe ty1
 370         = cant_match f1 f2 || cant_match a1 a2
 371
 372     cant_match _ _ = False      -- Safe!
 373
 374 -- Things we could add;
 375 --      foralls
 376 --      look through newtypes
 377 --      take account of tyvar bindings (EQ example above)
 378 \end{code}
 379
 380
 381 %************************************************************************
 382 %*                                                                      *
 383                 What a refinement is
 384 %*                                                                      *
 385 %************************************************************************
 386
 387 \begin{code}
 388 data Refinement = Reft InScopeSet InternalReft
 389
 390 type InternalReft = TyVarEnv (Coercion, Type)
 391 -- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
 392 -- Not necessarily idemopotent
 393
 394 instance Outputable Refinement where
 395   ppr (Reft _in_scope env)
 396     = ptext SLIT("Refinement") <+>
 397         braces (ppr env)
 398
 399 emptyRefinement :: Refinement
 400 emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
 401
 402 isEmptyRefinement :: Refinement -> Bool
 403 isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
 404
 405 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
 406 -- Apply the refinement to the type.
 407 -- If (refineType r ty) = (co, ty')
 408 -- Then co :: ty:=:ty'
 409 -- Nothing => the refinement does nothing to this type
 410 refineType (Reft in_scope env) ty
 411   | not (isEmptyVarEnv env),            -- Common case
 412     any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
 413   = Just (substTy co_subst ty, substTy tv_subst ty)
 414   | otherwise
 415   = Nothing     -- The type doesn't mention any refined type variables
 416   where
 417     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
 418     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
 419
 420 refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
 421 refinePred (Reft in_scope env) pred
 422   | not (isEmptyVarEnv env),            -- Common case
 423     any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
 424   = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
 425   | otherwise
 426   = Nothing     -- The type doesn't mention any refined type variables
 427   where
 428     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
 429     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
 430
 431 refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
 432 -- Like refineType, but returns the 'sym' coercion
 433 -- If (refineResType r ty) = (co, ty')
 434 -- Then co :: ty':=:ty
 435 refineResType reft ty
 436   = case refineType reft ty of
 437       Just (co, ty1) -> Just (mkSymCoercion co, ty1)
 438       Nothing        -> Nothing
 439 \end{code}
 440
 441
 442 %************************************************************************
 443 %*                                                                      *
 444                 Simple generation of a type refinement
 445 %*                                                                      *
 446 %************************************************************************
 447
 448 \begin{code}
 449 matchRefine :: [CoVar] -> Refinement
 450 \end{code}
 451
 452 Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
 453 is a specialisation of ty1, produce a type refinement that maps the variables
 454 of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
 455
 456   matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
 457     = { right (left (right co)) :: a ~ c
 458       , right (right co)        :: b ~ Maybe d
 459       }
 460
 461 Precondition: The rhs types must indeed be a specialisation of the lhs types;
 462   i.e., some free variables of the lhs are replaced with either distinct free
 463   variables or proper type terms to obtain the rhs.  (We don't perform full
 464   unification or type matching here!)
 465
 466 NB: matchRefine does *not* expand the type synonyms.
 467
 468 \begin{code}
 469 matchRefine co_vars
 470   = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
 471   where
 472     in_scope = foldr extend emptyInScopeSet co_vars
 473
 474         -- For each co_var, add it *and* the tyvars it mentions, to in_scope
 475     extend co_var in_scope
 476       = extendInScopeSetSet in_scope $
 477           extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
 478
 479     refineOne co_var = refine (TyVarTy co_var) ty1 ty2
 480       where
 481         (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
 482
 483     refine co (TyVarTy tv) ty                     = unitVarEnv tv (co, ty)
 484     refine co (TyConApp _ tys) (TyConApp _ tys')  = refineArgs co tys tys'
 485     refine _  (PredTy _) (PredTy _)               =
 486       error "Unify.matchRefine: PredTy"
 487     refine co (FunTy arg res) (FunTy arg' res')   =
 488       refine (mkRightCoercion (mkLeftCoercion co)) arg arg'
 489       `plusVarEnv`
 490       refine (mkRightCoercion co) res res'
 491     refine co (AppTy fun arg) (AppTy fun' arg')   =
 492       refine (mkLeftCoercion co) fun fun'
 493       `plusVarEnv`
 494       refine (mkRightCoercion co) arg arg'
 495     refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
 496       refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
 497     refine _ _ _ = error "RcGadt.matchRefine: mismatch"
 498
 499     refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
 500     refineArgs co tys tys' =
 501       fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
 502       where
 503         refineArg (ty, ty') (reft, coWrapper)
 504           = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
 505              mkLeftCoercion . coWrapper)
 506 \end{code}
 507
 508
 509 %************************************************************************
 510 %*                                                                      *
 511                 Unification
 512 %*                                                                      *
 513 %************************************************************************
 514
 515 \begin{code}
 516 tcUnifyTys :: (TyVar -> BindFlag)
 517            -> [Type] -> [Type]
 518            -> Maybe TvSubst     -- A regular one-shot substitution
 519 -- The two types may have common type variables, and indeed do so in the
 520 -- second call to tcUnifyTys in FunDeps.checkClsFD
 521 --
 522 tcUnifyTys bind_fn tys1 tys2
 523   = maybeErrToMaybe $ initUM bind_fn $
 524     do { subst <- unifyList emptyTvSubstEnv tys1 tys2
 525
 526         -- Find the fixed point of the resulting non-idempotent substitution
 527         ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
 528               tv_env   = fixTvSubstEnv in_scope subst
 529
 530         ; return (mkTvSubst in_scope tv_env) }
 531   where
 532     tvs1 = tyVarsOfTypes tys1
 533     tvs2 = tyVarsOfTypes tys2
 534
 535 ----------------------------
 536 -- XXX Can we do this more nicely, by exploiting laziness?
 537 -- Or avoid needing it in the first place?
 538 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
 539 fixTvSubstEnv in_scope env = f env
 540   where
 541     f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
 542           in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
 543              then e
 544              else f e'
 545
 546 \end{code}
 547
 548
 549 %************************************************************************
 550 %*                                                                      *
 551                 The workhorse
 552 %*                                                                      *
 553 %************************************************************************
 554
 555 \begin{code}
 556 unify :: TvSubstEnv     -- An existing substitution to extend
 557       -> Type -> Type   -- Types to be unified, and witness of their equality
 558       -> UM TvSubstEnv          -- Just the extended substitution,
 559                                 -- Nothing if unification failed
 560 -- We do not require the incoming substitution to be idempotent,
 561 -- nor guarantee that the outgoing one is.  That's fixed up by
 562 -- the wrappers.
 563
 564 -- Respects newtypes, PredTypes
 565
 566 -- in unify, any NewTcApps/Preds should be taken at face value
 567 unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
 568 unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
 569
 570 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
 571 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
 572
 573 unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
 574
 575 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
 576   | tyc1 == tyc2 = unify_tys subst tys1 tys2
 577
 578 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 579   = do  { subst' <- unify subst ty1a ty2a
 580         ; unify subst' ty1b ty2b }
 581
 582         -- Applications need a bit of care!
 583         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 584         -- NB: we've already dealt with type variables and Notes,
 585         -- so if one type is an App the other one jolly well better be too
 586 unify subst (AppTy ty1a ty1b) ty2
 587   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 588   = do  { subst' <- unify subst ty1a ty2a
 589         ; unify subst' ty1b ty2b }
 590
 591 unify subst ty1 (AppTy ty2a ty2b)
 592   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 593   = do  { subst' <- unify subst ty1a ty2a
 594         ; unify subst' ty1b ty2b }
 595
 596 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
 597         -- ForAlls??
 598
 599 ------------------------------
 600 unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
 601 unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
 602   | c1 == c2 = unify_tys subst tys1 tys2
 603 unify_pred subst (IParam n1 t1) (IParam n2 t2)
 604   | n1 == n2 = unify subst t1 t2
 605 unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 606
 607 ------------------------------
 608 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 609 unify_tys subst xs ys = unifyList subst xs ys
 610
 611 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 612 unifyList subst orig_xs orig_ys
 613   = go subst orig_xs orig_ys
 614   where
 615     go subst []     []     = return subst
 616     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
 617                                 ; go subst' xs ys }
 618     go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
 619
 620 ---------------------------------
 621 uVar :: TvSubstEnv      -- An existing substitution to extend
 622      -> TyVar           -- Type variable to be unified
 623      -> Type            -- with this type
 624      -> UM TvSubstEnv
 625
 626 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
 627 --      if swap=False   (tv1:=:ty)
 628 --      if swap=True    (ty:=:tv1)
 629
 630 uVar subst tv1 ty
 631  = -- Check to see whether tv1 is refined by the substitution
 632    case (lookupVarEnv subst tv1) of
 633      Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
 634      Nothing  -> uUnrefined subst       -- No, continue
 635                             tv1 ty ty
 636
 637 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
 638            -> TyVar               -- Type variable to be unified
 639            -> Type                -- with this type
 640            -> Type                -- (version w/ expanded synonyms)
 641            -> UM TvSubstEnv
 642
 643 -- We know that tv1 isn't refined
 644
 645 uUnrefined subst tv1 ty2 ty2'
 646   | Just ty2'' <- tcView ty2'
 647   = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
 648                 -- This is essential, in case we have
 649                 --      type Foo a = a
 650                 -- and then unify a :=: Foo a
 651
 652 uUnrefined subst tv1 ty2 (TyVarTy tv2)
 653   | tv1 == tv2          -- Same type variable
 654   = return subst
 655
 656     -- Check to see whether tv2 is refined
 657   | Just ty' <- lookupVarEnv subst tv2
 658   = uUnrefined subst tv1 ty' ty'
 659
 660   -- So both are unrefined; next, see if the kinds force the direction
 661   | eqKind k1 k2        -- Can update either; so check the bind-flags
 662   = do  { b1 <- tvBindFlag tv1
 663         ; b2 <- tvBindFlag tv2
 664         ; case (b1,b2) of
 665             (BindMe, _)          -> bind tv1 ty2
 666
 667             (AvoidMe, BindMe)    -> bind tv2 ty1
 668             (AvoidMe, _)         -> bind tv1 ty2
 669
 670             (WildCard, WildCard) -> return subst
 671             (WildCard, Skolem)   -> return subst
 672             (WildCard, _)        -> bind tv2 ty1
 673
 674             (Skolem, WildCard)   -> return subst
 675             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
 676             (Skolem, _)          -> bind tv2 ty1
 677         }
 678
 679   | k1 `isSubKind` k2 = bindTv subst tv2 ty1  -- Must update tv2
 680   | k2 `isSubKind` k1 = bindTv subst tv1 ty2  -- Must update tv1
 681
 682   | otherwise = failWith (kindMisMatch tv1 ty2)
 683   where
 684     ty1 = TyVarTy tv1
 685     k1 = tyVarKind tv1
 686     k2 = tyVarKind tv2
 687     bind tv ty = return $ extendVarEnv subst tv ty
 688
 689 uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
 690   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
 691   = failWith (occursCheck tv1 ty2)      -- Occurs check
 692   | not (k2 `isSubKind` k1)
 693   = failWith (kindMisMatch tv1 ty2)     -- Kind check
 694   | otherwise
 695   = bindTv subst tv1 ty2                -- Bind tyvar to the synonym if poss
 696   where
 697     k1 = tyVarKind tv1
 698     k2 = typeKind ty2'
 699
 700 substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
 701 -- Apply the non-idempotent substitution to a set of type variables,
 702 -- remembering that the substitution isn't necessarily idempotent
 703 substTvSet subst tvs
 704   = foldVarSet (unionVarSet . get) emptyVarSet tvs
 705   where
 706     get tv = case lookupVarEnv subst tv of
 707                Nothing -> unitVarSet tv
 708                Just ty -> substTvSet subst (tyVarsOfType ty)
 709
 710 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
 711 bindTv subst tv ty      -- ty is not a type variable
 712   = do  { b <- tvBindFlag tv
 713         ; case b of
 714             Skolem   -> failWith (misMatch (TyVarTy tv) ty)
 715             WildCard -> return subst
 716             _other   -> return $ extendVarEnv subst tv ty
 717         }
 718 \end{code}
 719
 720 %************************************************************************
 721 %*                                                                      *
 722                 Unification monad
 723 %*                                                                      *
 724 %************************************************************************
 725
 726 \begin{code}
 727 data BindFlag
 728   = BindMe      -- A regular type variable
 729   | AvoidMe     -- Like BindMe but, given the choice, avoid binding it
 730
 731   | Skolem      -- This type variable is a skolem constant
 732                 -- Don't bind it; it only matches itself
 733
 734   | WildCard    -- This type variable matches anything,
 735                 -- and does not affect the substitution
 736
 737 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 738                          -> MaybeErr Message a }
 739
 740 instance Monad UM where
 741   return a = UM (\_tvs -> Succeeded a)
 742   fail s   = UM (\_tvs -> Failed (text s))
 743   m >>= k  = UM (\tvs -> case unUM m tvs of
 744                            Failed err -> Failed err
 745                            Succeeded v  -> unUM (k v) tvs)
 746
 747 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
 748 initUM badtvs um = unUM um badtvs
 749
 750 tvBindFlag :: TyVar -> UM BindFlag
 751 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
 752
 753 failWith :: Message -> UM a
 754 failWith msg = UM (\_tv_fn -> Failed msg)
 755
 756 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
 757 maybeErrToMaybe (Succeeded a) = Just a
 758 maybeErrToMaybe (Failed _)    = Nothing
 759 \end{code}
 760
 761
 762 %************************************************************************
 763 %*                                                                      *
 764                 Error reporting
 765         We go to a lot more trouble to tidy the types
 766         in TcUnify.  Maybe we'll end up having to do that
 767         here too, but I'll leave it for now.
 768 %*                                                                      *
 769 %************************************************************************
 770
 771 \begin{code}
 772 misMatch :: Type -> Type -> SDoc
 773 misMatch t1 t2
 774   = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+>
 775     ptext SLIT("and") <+> quotes (ppr t2)
 776
 777 lengthMisMatch :: [Type] -> [Type] -> SDoc
 778 lengthMisMatch tys1 tys2
 779   = sep [ptext SLIT("Can't match unequal length lists"),
 780          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 781
 782 kindMisMatch :: TyVar -> Type -> SDoc
 783 kindMisMatch tv1 t2
 784   = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
 785             ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
 786           ptext SLIT("when matching") <+> quotes (ppr tv1) <+>
 787                 ptext SLIT("with") <+> quotes (ppr t2)]
 788
 789 occursCheck :: TyVar -> Type -> SDoc
 790 occursCheck tv ty
 791   = hang (ptext SLIT("Can't construct the infinite type"))
 792        2 (ppr tv <+> equals <+> ppr ty)
 793 \end{code}