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   | Just ty1' <- lookupVarEnv subst tv1'        -- tv1' is already bound
 162   = if tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
 163         -- ty1 has no locally-bound variables, hence nukeRnEnvL
 164         -- Note tcEqType...we are doing source-type matching here
 165     then Just subst
 166     else Nothing        -- ty2 doesn't match
 167
 168   | tv1' `elemVarSet` me_tmpls menv
 169   = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
 170     then Nothing        -- Occurs check
 171     else do { subst1 <- match_kind menv subst tv1 ty2
 172                         -- Note [Matching kinds]
 173             ; return (extendVarEnv subst1 tv1' ty2) }
 174
 175    | otherwise  -- tv1 is not a template tyvar
 176    = case ty2 of
 177         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
 178         _                                       -> 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 _ _ _ _
 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 :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
 233 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
 234
 235 --------------
 236 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
 237            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
 238 match_list _  subst []         []         = Just subst
 239 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
 240                                                 ; match_list fn subst' tys1 tys2 }
 241 match_list _  _     _          _          = Nothing
 242
 243 --------------
 244 match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
 245 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
 246   | c1 == c2 = match_tys menv subst tys1 tys2
 247 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
 248   | n1 == n2 = match menv subst t1 t2
 249 match_pred _    _     _ _ = Nothing
 250 \end{code}
 251
 252
 253 %************************************************************************
 254 %*                                                                      *
 255                 GADTs
 256 %*                                                                      *
 257 %************************************************************************
 258
 259 Note [Pruning dead case alternatives]
 260 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 261 Consider        data T a where
 262                    T1 :: T Int
 263                    T2 :: T a
 264
 265                 newtype X = MkX Int
 266                 newtype Y = MkY Char
 267
 268                 type family F a
 269                 type instance F Bool = Int
 270
 271 Now consider    case x of { T1 -> e1; T2 -> e2 }
 272
 273 The question before the house is this: if I know something about the type
 274 of x, can I prune away the T1 alternative?
 275
 276 Suppose x::T Char.  It's impossible to construct a (T Char) using T1,
 277         Answer = YES (clearly)
 278
 279 Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
 280 to 'Bool', in which case x::T Int, so
 281         ANSWER = NO (clearly)
 282
 283 Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom)
 284 value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
 285 gives a coercion
 286         CoX :: X ~ Int
 287 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
 288 of type (T X) constructed with T1.  Hence
 289         ANSWER = NO (surprisingly)
 290
 291 Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
 292 mechanism uses a cast, just as above, to move from one dictionary to another,
 293 in effect giving the programmer access to CoX.
 294
 295 Finally, suppose x::T Y.  Then *even in FC* we can't construct a
 296 non-bottom value of type (T Y) using T1.  That's because we can get
 297 from Y to Char, but not to Int.
 298
 299
 300 Here's a related question.      data Eq a b where EQ :: Eq a a
 301 Consider
 302         case x of { EQ -> ... }
 303
 304 Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
 305
 306 What about x::Eq Int a, in a context where we have evidence that a~Char.
 307 Then again the alternative is dead.
 308
 309
 310                         Summary
 311
 312 We are really doing a test for unsatisfiability of the type
 313 constraints implied by the match. And that is clearly, in general, a
 314 hard thing to do.
 315
 316 However, since we are simply dropping dead code, a conservative test
 317 suffices.  There is a continuum of tests, ranging from easy to hard, that
 318 drop more and more dead code.
 319
 320 For now we implement a very simple test: type variables match
 321 anything, type functions (incl newtypes) match anything, and only
 322 distinct data types fail to match.  We can elaborate later.
 323
 324 \begin{code}
 325 dataConCannotMatch :: [Type] -> DataCon -> Bool
 326 -- Returns True iff the data con *definitely cannot* match a
 327 --                  scrutinee of type (T tys)
 328 --                  where T is the type constructor for the data con
 329 --
 330 dataConCannotMatch tys con
 331   | null eq_spec      = False   -- Common
 332   | all isTyVarTy tys = False   -- Also common
 333   | otherwise
 334   = cant_match_s (map (substTyVar subst . fst) eq_spec)
 335                  (map snd eq_spec)
 336   where
 337     dc_tvs  = dataConUnivTyVars con
 338     eq_spec = dataConEqSpec con
 339     subst   = zipTopTvSubst dc_tvs tys
 340
 341     cant_match_s :: [Type] -> [Type] -> Bool
 342     cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
 343                              or (zipWith cant_match tys1 tys2)
 344
 345     cant_match :: Type -> Type -> Bool
 346     cant_match t1 t2
 347         | Just t1' <- coreView t1 = cant_match t1' t2
 348         | Just t2' <- coreView t2 = cant_match t1 t2'
 349
 350     cant_match (FunTy a1 r1) (FunTy a2 r2)
 351         = cant_match a1 a2 || cant_match r1 r2
 352
 353     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 354         | isDataTyCon tc1 && isDataTyCon tc2
 355         = tc1 /= tc2 || cant_match_s tys1 tys2
 356
 357     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
 358     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
 359         -- tc can't be FunTyCon by invariant
 360
 361     cant_match (AppTy f1 a1) ty2
 362         | Just (f2, a2) <- repSplitAppTy_maybe ty2
 363         = cant_match f1 f2 || cant_match a1 a2
 364     cant_match ty1 (AppTy f2 a2)
 365         | Just (f1, a1) <- repSplitAppTy_maybe ty1
 366         = cant_match f1 f2 || cant_match a1 a2
 367
 368     cant_match _ _ = False      -- Safe!
 369
 370 -- Things we could add;
 371 --      foralls
 372 --      look through newtypes
 373 --      take account of tyvar bindings (EQ example above)
 374 \end{code}
 375
 376
 377 %************************************************************************
 378 %*                                                                      *
 379                 What a refinement is
 380 %*                                                                      *
 381 %************************************************************************
 382
 383 \begin{code}
 384 data Refinement = Reft InScopeSet InternalReft
 385
 386 type InternalReft = TyVarEnv (Coercion, Type)
 387 -- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
 388 -- Not necessarily idemopotent
 389
 390 instance Outputable Refinement where
 391   ppr (Reft _in_scope env)
 392     = ptext (sLit "Refinement") <+>
 393         braces (ppr env)
 394
 395 emptyRefinement :: Refinement
 396 emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
 397
 398 isEmptyRefinement :: Refinement -> Bool
 399 isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
 400
 401 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
 402 -- Apply the refinement to the type.
 403 -- If (refineType r ty) = (co, ty')
 404 -- Then co :: ty:=:ty'
 405 -- Nothing => the refinement does nothing to this type
 406 refineType (Reft in_scope env) ty
 407   | not (isEmptyVarEnv env),            -- Common case
 408     any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
 409   = Just (substTy co_subst ty, substTy tv_subst ty)
 410   | otherwise
 411   = Nothing     -- The type doesn't mention any refined type variables
 412   where
 413     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
 414     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
 415
 416 refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
 417 refinePred (Reft in_scope env) pred
 418   | not (isEmptyVarEnv env),            -- Common case
 419     any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
 420   = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
 421   | otherwise
 422   = Nothing     -- The type doesn't mention any refined type variables
 423   where
 424     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
 425     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
 426
 427 refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
 428 -- Like refineType, but returns the 'sym' coercion
 429 -- If (refineResType r ty) = (co, ty')
 430 -- Then co :: ty':=:ty
 431 refineResType reft ty
 432   = case refineType reft ty of
 433       Just (co, ty1) -> Just (mkSymCoercion co, ty1)
 434       Nothing        -> Nothing
 435 \end{code}
 436
 437
 438 %************************************************************************
 439 %*                                                                      *
 440                 Simple generation of a type refinement
 441 %*                                                                      *
 442 %************************************************************************
 443
 444 \begin{code}
 445 matchRefine :: [CoVar] -> Refinement
 446 \end{code}
 447
 448 Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
 449 is a specialisation of ty1, produce a type refinement that maps the variables
 450 of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
 451
 452   matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
 453     = { right (left (right co)) :: a ~ c
 454       , right (right co)        :: b ~ Maybe d
 455       }
 456
 457 Precondition: The rhs types must indeed be a specialisation of the lhs types;
 458   i.e., some free variables of the lhs are replaced with either distinct free
 459   variables or proper type terms to obtain the rhs.  (We don't perform full
 460   unification or type matching here!)
 461
 462 NB: matchRefine does *not* expand the type synonyms.
 463
 464 \begin{code}
 465 matchRefine co_vars
 466   = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
 467   where
 468     in_scope = foldr extend emptyInScopeSet co_vars
 469
 470         -- For each co_var, add it *and* the tyvars it mentions, to in_scope
 471     extend co_var in_scope
 472       = extendInScopeSetSet in_scope $
 473           extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
 474
 475     refineOne co_var = refine (TyVarTy co_var) ty1 ty2
 476       where
 477         (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
 478
 479     refine co (TyVarTy tv) ty                     = unitVarEnv tv (co, ty)
 480     refine co (TyConApp _ tys) (TyConApp _ tys')  = refineArgs co tys tys'
 481     refine _  (PredTy _) (PredTy _)               =
 482       error "Unify.matchRefine: PredTy"
 483     refine co (FunTy arg res) (FunTy arg' res')   =
 484       refine (mkRightCoercion (mkLeftCoercion co)) arg arg'
 485       `plusVarEnv`
 486       refine (mkRightCoercion co) res res'
 487     refine co (AppTy fun arg) (AppTy fun' arg')   =
 488       refine (mkLeftCoercion co) fun fun'
 489       `plusVarEnv`
 490       refine (mkRightCoercion co) arg arg'
 491     refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
 492       refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
 493     refine _ _ _ = error "RcGadt.matchRefine: mismatch"
 494
 495     refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
 496     refineArgs co tys tys' =
 497       fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
 498       where
 499         refineArg (ty, ty') (reft, coWrapper)
 500           = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
 501              mkLeftCoercion . coWrapper)
 502 \end{code}
 503
 504
 505 %************************************************************************
 506 %*                                                                      *
 507                 Unification
 508 %*                                                                      *
 509 %************************************************************************
 510
 511 \begin{code}
 512 tcUnifyTys :: (TyVar -> BindFlag)
 513            -> [Type] -> [Type]
 514            -> Maybe TvSubst     -- A regular one-shot substitution
 515 -- The two types may have common type variables, and indeed do so in the
 516 -- second call to tcUnifyTys in FunDeps.checkClsFD
 517 --
 518 tcUnifyTys bind_fn tys1 tys2
 519   = maybeErrToMaybe $ initUM bind_fn $
 520     do { subst <- unifyList emptyTvSubstEnv tys1 tys2
 521
 522         -- Find the fixed point of the resulting non-idempotent substitution
 523         ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
 524               tv_env   = fixTvSubstEnv in_scope subst
 525
 526         ; return (mkTvSubst in_scope tv_env) }
 527   where
 528     tvs1 = tyVarsOfTypes tys1
 529     tvs2 = tyVarsOfTypes tys2
 530
 531 ----------------------------
 532 -- XXX Can we do this more nicely, by exploiting laziness?
 533 -- Or avoid needing it in the first place?
 534 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
 535 fixTvSubstEnv in_scope env = f env
 536   where
 537     f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
 538           in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
 539              then e
 540              else f e'
 541
 542 \end{code}
 543
 544
 545 %************************************************************************
 546 %*                                                                      *
 547                 The workhorse
 548 %*                                                                      *
 549 %************************************************************************
 550
 551 \begin{code}
 552 unify :: TvSubstEnv     -- An existing substitution to extend
 553       -> Type -> Type   -- Types to be unified, and witness of their equality
 554       -> UM TvSubstEnv          -- Just the extended substitution,
 555                                 -- Nothing if unification failed
 556 -- We do not require the incoming substitution to be idempotent,
 557 -- nor guarantee that the outgoing one is.  That's fixed up by
 558 -- the wrappers.
 559
 560 -- Respects newtypes, PredTypes
 561
 562 -- in unify, any NewTcApps/Preds should be taken at face value
 563 unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
 564 unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
 565
 566 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
 567 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
 568
 569 unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
 570
 571 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
 572   | tyc1 == tyc2 = unify_tys subst tys1 tys2
 573
 574 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 575   = do  { subst' <- unify subst ty1a ty2a
 576         ; unify subst' ty1b ty2b }
 577
 578         -- Applications need a bit of care!
 579         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 580         -- NB: we've already dealt with type variables and Notes,
 581         -- so if one type is an App the other one jolly well better be too
 582 unify subst (AppTy ty1a ty1b) ty2
 583   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 584   = do  { subst' <- unify subst ty1a ty2a
 585         ; unify subst' ty1b ty2b }
 586
 587 unify subst ty1 (AppTy ty2a ty2b)
 588   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 589   = do  { subst' <- unify subst ty1a ty2a
 590         ; unify subst' ty1b ty2b }
 591
 592 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
 593         -- ForAlls??
 594
 595 ------------------------------
 596 unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
 597 unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
 598   | c1 == c2 = unify_tys subst tys1 tys2
 599 unify_pred subst (IParam n1 t1) (IParam n2 t2)
 600   | n1 == n2 = unify subst t1 t2
 601 unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 602
 603 ------------------------------
 604 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 605 unify_tys subst xs ys = unifyList subst xs ys
 606
 607 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 608 unifyList subst orig_xs orig_ys
 609   = go subst orig_xs orig_ys
 610   where
 611     go subst []     []     = return subst
 612     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
 613                                 ; go subst' xs ys }
 614     go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
 615
 616 ---------------------------------
 617 uVar :: TvSubstEnv      -- An existing substitution to extend
 618      -> TyVar           -- Type variable to be unified
 619      -> Type            -- with this type
 620      -> UM TvSubstEnv
 621
 622 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
 623 --      if swap=False   (tv1:=:ty)
 624 --      if swap=True    (ty:=:tv1)
 625
 626 uVar subst tv1 ty
 627  = -- Check to see whether tv1 is refined by the substitution
 628    case (lookupVarEnv subst tv1) of
 629      Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
 630      Nothing  -> uUnrefined subst       -- No, continue
 631                             tv1 ty ty
 632
 633 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
 634            -> TyVar               -- Type variable to be unified
 635            -> Type                -- with this type
 636            -> Type                -- (version w/ expanded synonyms)
 637            -> UM TvSubstEnv
 638
 639 -- We know that tv1 isn't refined
 640
 641 uUnrefined subst tv1 ty2 ty2'
 642   | Just ty2'' <- tcView ty2'
 643   = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
 644                 -- This is essential, in case we have
 645                 --      type Foo a = a
 646                 -- and then unify a :=: Foo a
 647
 648 uUnrefined subst tv1 ty2 (TyVarTy tv2)
 649   | tv1 == tv2          -- Same type variable
 650   = return subst
 651
 652     -- Check to see whether tv2 is refined
 653   | Just ty' <- lookupVarEnv subst tv2
 654   = uUnrefined subst tv1 ty' ty'
 655
 656   -- So both are unrefined; next, see if the kinds force the direction
 657   | eqKind k1 k2        -- Can update either; so check the bind-flags
 658   = do  { b1 <- tvBindFlag tv1
 659         ; b2 <- tvBindFlag tv2
 660         ; case (b1,b2) of
 661             (BindMe, _)          -> bind tv1 ty2
 662
 663             (AvoidMe, BindMe)    -> bind tv2 ty1
 664             (AvoidMe, _)         -> bind tv1 ty2
 665
 666             (WildCard, WildCard) -> return subst
 667             (WildCard, Skolem)   -> return subst
 668             (WildCard, _)        -> bind tv2 ty1
 669
 670             (Skolem, WildCard)   -> return subst
 671             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
 672             (Skolem, _)          -> bind tv2 ty1
 673         }
 674
 675   | k1 `isSubKind` k2 = bindTv subst tv2 ty1  -- Must update tv2
 676   | k2 `isSubKind` k1 = bindTv subst tv1 ty2  -- Must update tv1
 677
 678   | otherwise = failWith (kindMisMatch tv1 ty2)
 679   where
 680     ty1 = TyVarTy tv1
 681     k1 = tyVarKind tv1
 682     k2 = tyVarKind tv2
 683     bind tv ty = return $ extendVarEnv subst tv ty
 684
 685 uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
 686   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
 687   = failWith (occursCheck tv1 ty2)      -- Occurs check
 688   | not (k2 `isSubKind` k1)
 689   = failWith (kindMisMatch tv1 ty2)     -- Kind check
 690   | otherwise
 691   = bindTv subst tv1 ty2                -- Bind tyvar to the synonym if poss
 692   where
 693     k1 = tyVarKind tv1
 694     k2 = typeKind ty2'
 695
 696 substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
 697 -- Apply the non-idempotent substitution to a set of type variables,
 698 -- remembering that the substitution isn't necessarily idempotent
 699 substTvSet subst tvs
 700   = foldVarSet (unionVarSet . get) emptyVarSet tvs
 701   where
 702     get tv = case lookupVarEnv subst tv of
 703                Nothing -> unitVarSet tv
 704                Just ty -> substTvSet subst (tyVarsOfType ty)
 705
 706 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
 707 bindTv subst tv ty      -- ty is not a type variable
 708   = do  { b <- tvBindFlag tv
 709         ; case b of
 710             Skolem   -> failWith (misMatch (TyVarTy tv) ty)
 711             WildCard -> return subst
 712             _other   -> return $ extendVarEnv subst tv ty
 713         }
 714 \end{code}
 715
 716 %************************************************************************
 717 %*                                                                      *
 718                 Unification monad
 719 %*                                                                      *
 720 %************************************************************************
 721
 722 \begin{code}
 723 data BindFlag
 724   = BindMe      -- A regular type variable
 725   | AvoidMe     -- Like BindMe but, given the choice, avoid binding it
 726
 727   | Skolem      -- This type variable is a skolem constant
 728                 -- Don't bind it; it only matches itself
 729
 730   | WildCard    -- This type variable matches anything,
 731                 -- and does not affect the substitution
 732
 733 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 734                          -> MaybeErr Message a }
 735
 736 instance Monad UM where
 737   return a = UM (\_tvs -> Succeeded a)
 738   fail s   = UM (\_tvs -> Failed (text s))
 739   m >>= k  = UM (\tvs -> case unUM m tvs of
 740                            Failed err -> Failed err
 741                            Succeeded v  -> unUM (k v) tvs)
 742
 743 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
 744 initUM badtvs um = unUM um badtvs
 745
 746 tvBindFlag :: TyVar -> UM BindFlag
 747 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
 748
 749 failWith :: Message -> UM a
 750 failWith msg = UM (\_tv_fn -> Failed msg)
 751
 752 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
 753 maybeErrToMaybe (Succeeded a) = Just a
 754 maybeErrToMaybe (Failed _)    = Nothing
 755 \end{code}
 756
 757
 758 %************************************************************************
 759 %*                                                                      *
 760                 Error reporting
 761         We go to a lot more trouble to tidy the types
 762         in TcUnify.  Maybe we'll end up having to do that
 763         here too, but I'll leave it for now.
 764 %*                                                                      *
 765 %************************************************************************
 766
 767 \begin{code}
 768 misMatch :: Type -> Type -> SDoc
 769 misMatch t1 t2
 770   = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+>
 771     ptext (sLit "and") <+> quotes (ppr t2)
 772
 773 lengthMisMatch :: [Type] -> [Type] -> SDoc
 774 lengthMisMatch tys1 tys2
 775   = sep [ptext (sLit "Can't match unequal length lists"),
 776          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 777
 778 kindMisMatch :: TyVar -> Type -> SDoc
 779 kindMisMatch tv1 t2
 780   = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
 781             ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
 782           ptext (sLit "when matching") <+> quotes (ppr tv1) <+>
 783                 ptext (sLit "with") <+> quotes (ppr t2)]
 784
 785 occursCheck :: TyVar -> Type -> SDoc
 786 occursCheck tv ty
 787   = hang (ptext (sLit "Can't construct the infinite type"))
 788        2 (ppr tv <+> equals <+> ppr ty)
 789 \end{code}