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,
  12
  13         MatchEnv(..), matchList,
  14
  15         typesCantMatch,
  16
  17         -- Side-effect free unification
  18         tcUnifyTys, BindFlag(..),
  19         niFixTvSubst, niSubstTvSet
  20
  21    ) where
  22
  23 #include "HsVersions.h"
  24
  25 import Var
  26 import VarEnv
  27 import VarSet
  28 import Kind
  29 import Type
  30 import TyCon
  31 import TypeRep
  32 import Outputable
  33 import ErrUtils
  34 import Util
  35 import Maybes
  36 import FastString
  37
  38 import Control.Monad (guard)
  39 \end{code}
  40
  41
  42 %************************************************************************
  43 %*                                                                      *
  44                 Matching
  45 %*                                                                      *
  46 %************************************************************************
  47
  48
  49 Matching is much tricker than you might think.
  50
  51 1. The substitution we generate binds the *template type variables*
  52    which are given to us explicitly.
  53
  54 2. We want to match in the presence of foralls;
  55         e.g     (forall a. t1) ~ (forall b. t2)
  56
  57    That is what the RnEnv2 is for; it does the alpha-renaming
  58    that makes it as if a and b were the same variable.
  59    Initialising the RnEnv2, so that it can generate a fresh
  60    binder when necessary, entails knowing the free variables of
  61    both types.
  62
  63 3. We must be careful not to bind a template type variable to a
  64    locally bound variable.  E.g.
  65         (forall a. x) ~ (forall b. b)
  66    where x is the template type variable.  Then we do not want to
  67    bind x to a/b!  This is a kind of occurs check.
  68    The necessary locals accumulate in the RnEnv2.
  69
  70
  71 \begin{code}
  72 data MatchEnv
  73   = ME  { me_tmpls :: VarSet    -- Template variables
  74         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
  75         }                       --   In-scope set includes template variables
  76     -- Nota Bene: MatchEnv isn't specific to Types.  It is used
  77     --            for matching terms and coercions as well as types
  78
  79 tcMatchTy :: TyVarSet           -- Template tyvars
  80           -> Type               -- Template
  81           -> Type               -- Target
  82           -> Maybe TvSubst      -- One-shot; in principle the template
  83                                 -- variables could be free in the target
  84
  85 tcMatchTy tmpls ty1 ty2
  86   = case match menv emptyTvSubstEnv ty1 ty2 of
  87         Just subst_env -> Just (TvSubst in_scope subst_env)
  88         Nothing        -> Nothing
  89   where
  90     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
  91     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
  92         -- We're assuming that all the interesting
  93         -- tyvars in tys1 are in tmpls
  94
  95 tcMatchTys :: TyVarSet          -- Template tyvars
  96            -> [Type]            -- Template
  97            -> [Type]            -- Target
  98            -> Maybe TvSubst     -- One-shot; in principle the template
  99                                 -- variables could be free in the target
 100
 101 tcMatchTys tmpls tys1 tys2
 102   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
 103         Just subst_env -> Just (TvSubst in_scope subst_env)
 104         Nothing        -> Nothing
 105   where
 106     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
 107     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
 108         -- We're assuming that all the interesting
 109         -- tyvars in tys1 are in tmpls
 110
 111 -- This is similar, but extends a substitution
 112 tcMatchTyX :: TyVarSet          -- Template tyvars
 113            -> TvSubst           -- Substitution to extend
 114            -> Type              -- Template
 115            -> Type              -- Target
 116            -> Maybe TvSubst
 117 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
 118   = case match menv subst_env ty1 ty2 of
 119         Just subst_env -> Just (TvSubst in_scope subst_env)
 120         Nothing        -> Nothing
 121   where
 122     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
 123
 124 tcMatchPreds
 125         :: [TyVar]                      -- Bind these
 126         -> [PredType] -> [PredType]
 127         -> Maybe TvSubstEnv
 128 tcMatchPreds tmpls ps1 ps2
 129   = matchList (match_pred menv) emptyTvSubstEnv ps1 ps2
 130   where
 131     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
 132     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
 133
 134 -- This one is called from the expression matcher, which already has a MatchEnv in hand
 135 ruleMatchTyX :: MatchEnv
 136          -> TvSubstEnv          -- Substitution to extend
 137          -> Type                -- Template
 138          -> Type                -- Target
 139          -> Maybe TvSubstEnv
 140
 141 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
 142 \end{code}
 143
 144 Now the internals of matching
 145
 146 \begin{code}
 147 match :: MatchEnv       -- For the most part this is pushed downwards
 148       -> TvSubstEnv     -- Substitution so far:
 149                         --   Domain is subset of template tyvars
 150                         --   Free vars of range is subset of
 151                         --      in-scope set of the RnEnv2
 152       -> Type -> Type   -- Template and target respectively
 153       -> Maybe TvSubstEnv
 154 -- This matcher works on core types; that is, it ignores PredTypes
 155 -- Watch out if newtypes become transparent agin!
 156 --      this matcher must respect newtypes
 157
 158 match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
 159                          | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
 160
 161 match menv subst (TyVarTy tv1) ty2
 162   | Just ty1' <- lookupVarEnv subst tv1'        -- tv1' is already bound
 163   = if eqTypeX (nukeRnEnvL rn_env) ty1' ty2
 164         -- ty1 has no locally-bound variables, hence nukeRnEnvL
 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 _ subst tv ty
 209   = guard (typeKind ty `isSubKind` tyVarKind tv) >> return subst
 210
 211 -- Note [Matching kinds]
 212 -- ~~~~~~~~~~~~~~~~~~~~~
 213 -- For ordinary type variables, we don't want (m a) to match (n b)
 214 -- if say (a::*) and (b::*->*).  This is just a yes/no issue.
 215 --
 216 -- For coercion kinds matters are more complicated.  If we have a
 217 -- coercion template variable co::a~[b], where a,b are presumably also
 218 -- template type variables, then we must match co's kind against the
 219 -- kind of the actual argument, so as to give bindings to a,b.
 220 --
 221 -- In fact I have no example in mind that *requires* this kind-matching
 222 -- to instantiate template type variables, but it seems like the right
 223 -- thing to do.  C.f. Note [Matching variable types] in Rules.lhs
 224
 225 --------------
 226 match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
 227 match_tys menv subst tys1 tys2 = matchList (match menv) subst tys1 tys2
 228
 229 --------------
 230 matchList :: (env -> a -> b -> Maybe env)
 231            -> env -> [a] -> [b] -> Maybe env
 232 matchList _  subst []     []     = Just subst
 233 matchList fn subst (a:as) (b:bs) = do { subst' <- fn subst a b
 234                                       ; matchList fn subst' as bs }
 235 matchList _  _     _      _      = Nothing
 236
 237 --------------
 238 match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
 239 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
 240   | c1 == c2 = match_tys menv subst tys1 tys2
 241 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
 242   | n1 == n2 = match menv subst t1 t2
 243 match_pred _    _     _ _ = Nothing
 244 \end{code}
 245
 246
 247 %************************************************************************
 248 %*                                                                      *
 249                 GADTs
 250 %*                                                                      *
 251 %************************************************************************
 252
 253 Note [Pruning dead case alternatives]
 254 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 255 Consider        data T a where
 256                    T1 :: T Int
 257                    T2 :: T a
 258
 259                 newtype X = MkX Int
 260                 newtype Y = MkY Char
 261
 262                 type family F a
 263                 type instance F Bool = Int
 264
 265 Now consider    case x of { T1 -> e1; T2 -> e2 }
 266
 267 The question before the house is this: if I know something about the type
 268 of x, can I prune away the T1 alternative?
 269
 270 Suppose x::T Char.  It's impossible to construct a (T Char) using T1,
 271         Answer = YES (clearly)
 272
 273 Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
 274 to 'Bool', in which case x::T Int, so
 275         ANSWER = NO (clearly)
 276
 277 Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom)
 278 value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
 279 gives a coercion
 280         CoX :: X ~ Int
 281 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
 282 of type (T X) constructed with T1.  Hence
 283         ANSWER = NO (surprisingly)
 284
 285 Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
 286 mechanism uses a cast, just as above, to move from one dictionary to another,
 287 in effect giving the programmer access to CoX.
 288
 289 Finally, suppose x::T Y.  Then *even in FC* we can't construct a
 290 non-bottom value of type (T Y) using T1.  That's because we can get
 291 from Y to Char, but not to Int.
 292
 293
 294 Here's a related question.      data Eq a b where EQ :: Eq a a
 295 Consider
 296         case x of { EQ -> ... }
 297
 298 Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
 299
 300 What about x::Eq Int a, in a context where we have evidence that a~Char.
 301 Then again the alternative is dead.
 302
 303
 304                         Summary
 305
 306 We are really doing a test for unsatisfiability of the type
 307 constraints implied by the match. And that is clearly, in general, a
 308 hard thing to do.
 309
 310 However, since we are simply dropping dead code, a conservative test
 311 suffices.  There is a continuum of tests, ranging from easy to hard, that
 312 drop more and more dead code.
 313
 314 For now we implement a very simple test: type variables match
 315 anything, type functions (incl newtypes) match anything, and only
 316 distinct data types fail to match.  We can elaborate later.
 317
 318 \begin{code}
 319 typesCantMatch :: [(Type,Type)] -> Bool
 320 typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
 321   where
 322     cant_match :: Type -> Type -> Bool
 323     cant_match t1 t2
 324         | Just t1' <- coreView t1 = cant_match t1' t2
 325         | Just t2' <- coreView t2 = cant_match t1 t2'
 326
 327     cant_match (FunTy a1 r1) (FunTy a2 r2)
 328         = cant_match a1 a2 || cant_match r1 r2
 329
 330     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 331         | isDataTyCon tc1 && isDataTyCon tc2
 332         = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2)
 333
 334     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
 335     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
 336         -- tc can't be FunTyCon by invariant
 337
 338     cant_match (AppTy f1 a1) ty2
 339         | Just (f2, a2) <- repSplitAppTy_maybe ty2
 340         = cant_match f1 f2 || cant_match a1 a2
 341     cant_match ty1 (AppTy f2 a2)
 342         | Just (f1, a1) <- repSplitAppTy_maybe ty1
 343         = cant_match f1 f2 || cant_match a1 a2
 344
 345     cant_match _ _ = False      -- Safe!
 346
 347 -- Things we could add;
 348 --      foralls
 349 --      look through newtypes
 350 --      take account of tyvar bindings (EQ example above)
 351 \end{code}
 352
 353
 354 %************************************************************************
 355 %*                                                                      *
 356              Unification
 357 %*                                                                      *
 358 %************************************************************************
 359
 360 \begin{code}
 361 tcUnifyTys :: (TyVar -> BindFlag)
 362            -> [Type] -> [Type]
 363            -> Maybe TvSubst     -- A regular one-shot (idempotent) substitution
 364 -- The two types may have common type variables, and indeed do so in the
 365 -- second call to tcUnifyTys in FunDeps.checkClsFD
 366 --
 367 tcUnifyTys bind_fn tys1 tys2
 368   = maybeErrToMaybe $ initUM bind_fn $
 369     do { subst <- unifyList emptyTvSubstEnv tys1 tys2
 370
 371         -- Find the fixed point of the resulting non-idempotent substitution
 372         ; return (niFixTvSubst subst) }
 373 \end{code}
 374
 375
 376 %************************************************************************
 377 %*                                                                      *
 378                 Non-idempotent substitution
 379 %*                                                                      *
 380 %************************************************************************
 381
 382 Note [Non-idempotent substitution]
 383 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 384 During unification we use a TvSubstEnv that is
 385   (a) non-idempotent
 386   (b) loop-free; ie repeatedly applying it yields a fixed point
 387
 388 \begin{code}
 389 niFixTvSubst :: TvSubstEnv -> TvSubst
 390 -- Find the idempotent fixed point of the non-idempotent substitution
 391 -- ToDo: use laziness instead of iteration?
 392 niFixTvSubst env = f env
 393   where
 394     f e | not_fixpoint = f (mapVarEnv (substTy subst) e)
 395         | otherwise    = subst
 396         where
 397           range_tvs    = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet e
 398           subst        = mkTvSubst (mkInScopeSet range_tvs) e
 399           not_fixpoint = foldVarSet ((||) . in_domain) False range_tvs
 400           in_domain tv = tv `elemVarEnv` e
 401
 402 niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
 403 -- Apply the non-idempotent substitution to a set of type variables,
 404 -- remembering that the substitution isn't necessarily idempotent
 405 -- This is used in the occurs check, before extending the substitution
 406 niSubstTvSet subst tvs
 407   = foldVarSet (unionVarSet . get) emptyVarSet tvs
 408   where
 409     get tv = case lookupVarEnv subst tv of
 410                Nothing -> unitVarSet tv
 411                Just ty -> niSubstTvSet subst (tyVarsOfType ty)
 412 \end{code}
 413
 414 %************************************************************************
 415 %*                                                                      *
 416                 The workhorse
 417 %*                                                                      *
 418 %************************************************************************
 419
 420 \begin{code}
 421 unify :: TvSubstEnv     -- An existing substitution to extend
 422       -> Type -> Type   -- Types to be unified, and witness of their equality
 423       -> UM TvSubstEnv          -- Just the extended substitution,
 424                                 -- Nothing if unification failed
 425 -- We do not require the incoming substitution to be idempotent,
 426 -- nor guarantee that the outgoing one is.  That's fixed up by
 427 -- the wrappers.
 428
 429 -- Respects newtypes, PredTypes
 430
 431 -- in unify, any NewTcApps/Preds should be taken at face value
 432 unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
 433 unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
 434
 435 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
 436 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
 437
 438 unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
 439
 440 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
 441   | tyc1 == tyc2 = unify_tys subst tys1 tys2
 442
 443 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 444   = do  { subst' <- unify subst ty1a ty2a
 445         ; unify subst' ty1b ty2b }
 446
 447         -- Applications need a bit of care!
 448         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 449         -- NB: we've already dealt with type variables and Notes,
 450         -- so if one type is an App the other one jolly well better be too
 451 unify subst (AppTy ty1a ty1b) ty2
 452   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 453   = do  { subst' <- unify subst ty1a ty2a
 454         ; unify subst' ty1b ty2b }
 455
 456 unify subst ty1 (AppTy ty2a ty2b)
 457   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 458   = do  { subst' <- unify subst ty1a ty2a
 459         ; unify subst' ty1b ty2b }
 460
 461 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
 462         -- ForAlls??
 463
 464 ------------------------------
 465 unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
 466 unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
 467   | c1 == c2 = unify_tys subst tys1 tys2
 468 unify_pred subst (IParam n1 t1) (IParam n2 t2)
 469   | n1 == n2 = unify subst t1 t2
 470 unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 471
 472 ------------------------------
 473 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 474 unify_tys subst xs ys = unifyList subst xs ys
 475
 476 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 477 unifyList subst orig_xs orig_ys
 478   = go subst orig_xs orig_ys
 479   where
 480     go subst []     []     = return subst
 481     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
 482                                 ; go subst' xs ys }
 483     go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
 484
 485 ---------------------------------
 486 uVar :: TvSubstEnv      -- An existing substitution to extend
 487      -> TyVar           -- Type variable to be unified
 488      -> Type            -- with this type
 489      -> UM TvSubstEnv
 490
 491 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
 492 --      if swap=False   (tv1~ty)
 493 --      if swap=True    (ty~tv1)
 494
 495 uVar subst tv1 ty
 496  = -- Check to see whether tv1 is refined by the substitution
 497    case (lookupVarEnv subst tv1) of
 498      Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
 499      Nothing  -> uUnrefined subst       -- No, continue
 500                             tv1 ty ty
 501
 502 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
 503            -> TyVar               -- Type variable to be unified
 504            -> Type                -- with this type
 505            -> Type                -- (version w/ expanded synonyms)
 506            -> UM TvSubstEnv
 507
 508 -- We know that tv1 isn't refined
 509
 510 uUnrefined subst tv1 ty2 ty2'
 511   | Just ty2'' <- tcView ty2'
 512   = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
 513                 -- This is essential, in case we have
 514                 --      type Foo a = a
 515                 -- and then unify a ~ Foo a
 516
 517 uUnrefined subst tv1 ty2 (TyVarTy tv2)
 518   | tv1 == tv2          -- Same type variable
 519   = return subst
 520
 521     -- Check to see whether tv2 is refined
 522   | Just ty' <- lookupVarEnv subst tv2
 523   = uUnrefined subst tv1 ty' ty'
 524
 525   -- So both are unrefined; next, see if the kinds force the direction
 526   | eqKind k1 k2        -- Can update either; so check the bind-flags
 527   = do  { b1 <- tvBindFlag tv1
 528         ; b2 <- tvBindFlag tv2
 529         ; case (b1,b2) of
 530             (BindMe, _)          -> bind tv1 ty2
 531             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
 532             (Skolem, _)          -> bind tv2 ty1
 533         }
 534
 535   | k1 `isSubKind` k2 = bindTv subst tv2 ty1  -- Must update tv2
 536   | k2 `isSubKind` k1 = bindTv subst tv1 ty2  -- Must update tv1
 537
 538   | otherwise = failWith (kindMisMatch tv1 ty2)
 539   where
 540     ty1 = TyVarTy tv1
 541     k1 = tyVarKind tv1
 542     k2 = tyVarKind tv2
 543     bind tv ty = return $ extendVarEnv subst tv ty
 544
 545 uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
 546   | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
 547   = failWith (occursCheck tv1 ty2)      -- Occurs check
 548   | not (k2 `isSubKind` k1)
 549   = failWith (kindMisMatch tv1 ty2)     -- Kind check
 550   | otherwise
 551   = bindTv subst tv1 ty2                -- Bind tyvar to the synonym if poss
 552   where
 553     k1 = tyVarKind tv1
 554     k2 = typeKind ty2'
 555
 556 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
 557 bindTv subst tv ty      -- ty is not a type variable
 558   = do  { b <- tvBindFlag tv
 559         ; case b of
 560             Skolem -> failWith (misMatch (TyVarTy tv) ty)
 561             BindMe -> return $ extendVarEnv subst tv ty
 562         }
 563 \end{code}
 564
 565 %************************************************************************
 566 %*                                                                      *
 567                 Binding decisions
 568 %*                                                                      *
 569 %************************************************************************
 570
 571 \begin{code}
 572 data BindFlag
 573   = BindMe      -- A regular type variable
 574
 575   | Skolem      -- This type variable is a skolem constant
 576                 -- Don't bind it; it only matches itself
 577 \end{code}
 578
 579
 580 %************************************************************************
 581 %*                                                                      *
 582                 Unification monad
 583 %*                                                                      *
 584 %************************************************************************
 585
 586 \begin{code}
 587 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 588                          -> MaybeErr Message a }
 589
 590 instance Monad UM where
 591   return a = UM (\_tvs -> Succeeded a)
 592   fail s   = UM (\_tvs -> Failed (text s))
 593   m >>= k  = UM (\tvs -> case unUM m tvs of
 594                            Failed err -> Failed err
 595                            Succeeded v  -> unUM (k v) tvs)
 596
 597 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
 598 initUM badtvs um = unUM um badtvs
 599
 600 tvBindFlag :: TyVar -> UM BindFlag
 601 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
 602
 603 failWith :: Message -> UM a
 604 failWith msg = UM (\_tv_fn -> Failed msg)
 605
 606 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
 607 maybeErrToMaybe (Succeeded a) = Just a
 608 maybeErrToMaybe (Failed _)    = Nothing
 609 \end{code}
 610
 611
 612 %************************************************************************
 613 %*                                                                      *
 614                 Error reporting
 615         We go to a lot more trouble to tidy the types
 616         in TcUnify.  Maybe we'll end up having to do that
 617         here too, but I'll leave it for now.
 618 %*                                                                      *
 619 %************************************************************************
 620
 621 \begin{code}
 622 misMatch :: Type -> Type -> SDoc
 623 misMatch t1 t2
 624   = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+>
 625     ptext (sLit "and") <+> quotes (ppr t2)
 626
 627 lengthMisMatch :: [Type] -> [Type] -> SDoc
 628 lengthMisMatch tys1 tys2
 629   = sep [ptext (sLit "Can't match unequal length lists"),
 630          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 631
 632 kindMisMatch :: TyVar -> Type -> SDoc
 633 kindMisMatch tv1 t2
 634   = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
 635             ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
 636           ptext (sLit "when matching") <+> quotes (ppr tv1) <+>
 637                 ptext (sLit "with") <+> quotes (ppr t2)]
 638
 639 occursCheck :: TyVar -> Type -> SDoc
 640 occursCheck tv ty
 641   = hang (ptext (sLit "Can't construct the infinite type"))
 642        2 (ppr tv <+> equals <+> ppr ty)
 643 \end{code}