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 tys1 tys2 = ASSERT( equalLength tys1 tys2 )
 321                            or (zipWith cant_match tys1 tys2)
 322   where
 323     cant_match :: Type -> Type -> Bool
 324     cant_match t1 t2
 325         | Just t1' <- coreView t1 = cant_match t1' t2
 326         | Just t2' <- coreView t2 = cant_match t1 t2'
 327
 328     cant_match (FunTy a1 r1) (FunTy a2 r2)
 329         = cant_match a1 a2 || cant_match r1 r2
 330
 331     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 332         | isDataTyCon tc1 && isDataTyCon tc2
 333         = tc1 /= tc2 || typesCantMatch tys1 tys2
 334
 335     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
 336     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
 337         -- tc can't be FunTyCon by invariant
 338
 339     cant_match (AppTy f1 a1) ty2
 340         | Just (f2, a2) <- repSplitAppTy_maybe ty2
 341         = cant_match f1 f2 || cant_match a1 a2
 342     cant_match ty1 (AppTy f2 a2)
 343         | Just (f1, a1) <- repSplitAppTy_maybe ty1
 344         = cant_match f1 f2 || cant_match a1 a2
 345
 346     cant_match _ _ = False      -- Safe!
 347
 348 -- Things we could add;
 349 --      foralls
 350 --      look through newtypes
 351 --      take account of tyvar bindings (EQ example above)
 352 \end{code}
 353
 354
 355 %************************************************************************
 356 %*                                                                      *
 357              Unification
 358 %*                                                                      *
 359 %************************************************************************
 360
 361 \begin{code}
 362 tcUnifyTys :: (TyVar -> BindFlag)
 363            -> [Type] -> [Type]
 364            -> Maybe TvSubst     -- A regular one-shot (idempotent) substitution
 365 -- The two types may have common type variables, and indeed do so in the
 366 -- second call to tcUnifyTys in FunDeps.checkClsFD
 367 --
 368 tcUnifyTys bind_fn tys1 tys2
 369   = maybeErrToMaybe $ initUM bind_fn $
 370     do { subst <- unifyList emptyTvSubstEnv tys1 tys2
 371
 372         -- Find the fixed point of the resulting non-idempotent substitution
 373         ; return (niFixTvSubst subst) }
 374 \end{code}
 375
 376
 377 %************************************************************************
 378 %*                                                                      *
 379                 Non-idempotent substitution
 380 %*                                                                      *
 381 %************************************************************************
 382
 383 Note [Non-idempotent substitution]
 384 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 385 During unification we use a TvSubstEnv that is
 386   (a) non-idempotent
 387   (b) loop-free; ie repeatedly applying it yields a fixed point
 388
 389 \begin{code}
 390 niFixTvSubst :: TvSubstEnv -> TvSubst
 391 -- Find the idempotent fixed point of the non-idempotent substitution
 392 -- ToDo: use laziness instead of iteration?
 393 niFixTvSubst env = f env
 394   where
 395     f e | not_fixpoint = f (mapVarEnv (substTy subst) e)
 396         | otherwise    = subst
 397         where
 398           range_tvs    = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet e
 399           subst        = mkTvSubst (mkInScopeSet range_tvs) e
 400           not_fixpoint = foldVarSet ((||) . in_domain) False range_tvs
 401           in_domain tv = tv `elemVarEnv` e
 402
 403 niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
 404 -- Apply the non-idempotent substitution to a set of type variables,
 405 -- remembering that the substitution isn't necessarily idempotent
 406 -- This is used in the occurs check, before extending the substitution
 407 niSubstTvSet subst tvs
 408   = foldVarSet (unionVarSet . get) emptyVarSet tvs
 409   where
 410     get tv = case lookupVarEnv subst tv of
 411                Nothing -> unitVarSet tv
 412                Just ty -> niSubstTvSet subst (tyVarsOfType ty)
 413 \end{code}
 414
 415 %************************************************************************
 416 %*                                                                      *
 417                 The workhorse
 418 %*                                                                      *
 419 %************************************************************************
 420
 421 \begin{code}
 422 unify :: TvSubstEnv     -- An existing substitution to extend
 423       -> Type -> Type   -- Types to be unified, and witness of their equality
 424       -> UM TvSubstEnv          -- Just the extended substitution,
 425                                 -- Nothing if unification failed
 426 -- We do not require the incoming substitution to be idempotent,
 427 -- nor guarantee that the outgoing one is.  That's fixed up by
 428 -- the wrappers.
 429
 430 -- Respects newtypes, PredTypes
 431
 432 -- in unify, any NewTcApps/Preds should be taken at face value
 433 unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
 434 unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
 435
 436 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
 437 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
 438
 439 unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
 440
 441 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
 442   | tyc1 == tyc2 = unify_tys subst tys1 tys2
 443
 444 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 445   = do  { subst' <- unify subst ty1a ty2a
 446         ; unify subst' ty1b ty2b }
 447
 448         -- Applications need a bit of care!
 449         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 450         -- NB: we've already dealt with type variables and Notes,
 451         -- so if one type is an App the other one jolly well better be too
 452 unify subst (AppTy ty1a ty1b) ty2
 453   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 454   = do  { subst' <- unify subst ty1a ty2a
 455         ; unify subst' ty1b ty2b }
 456
 457 unify subst ty1 (AppTy ty2a ty2b)
 458   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 459   = do  { subst' <- unify subst ty1a ty2a
 460         ; unify subst' ty1b ty2b }
 461
 462 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
 463         -- ForAlls??
 464
 465 ------------------------------
 466 unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
 467 unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
 468   | c1 == c2 = unify_tys subst tys1 tys2
 469 unify_pred subst (IParam n1 t1) (IParam n2 t2)
 470   | n1 == n2 = unify subst t1 t2
 471 unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 472
 473 ------------------------------
 474 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 475 unify_tys subst xs ys = unifyList subst xs ys
 476
 477 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 478 unifyList subst orig_xs orig_ys
 479   = go subst orig_xs orig_ys
 480   where
 481     go subst []     []     = return subst
 482     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
 483                                 ; go subst' xs ys }
 484     go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
 485
 486 ---------------------------------
 487 uVar :: TvSubstEnv      -- An existing substitution to extend
 488      -> TyVar           -- Type variable to be unified
 489      -> Type            -- with this type
 490      -> UM TvSubstEnv
 491
 492 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
 493 --      if swap=False   (tv1~ty)
 494 --      if swap=True    (ty~tv1)
 495
 496 uVar subst tv1 ty
 497  = -- Check to see whether tv1 is refined by the substitution
 498    case (lookupVarEnv subst tv1) of
 499      Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
 500      Nothing  -> uUnrefined subst       -- No, continue
 501                             tv1 ty ty
 502
 503 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
 504            -> TyVar               -- Type variable to be unified
 505            -> Type                -- with this type
 506            -> Type                -- (version w/ expanded synonyms)
 507            -> UM TvSubstEnv
 508
 509 -- We know that tv1 isn't refined
 510
 511 uUnrefined subst tv1 ty2 ty2'
 512   | Just ty2'' <- tcView ty2'
 513   = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
 514                 -- This is essential, in case we have
 515                 --      type Foo a = a
 516                 -- and then unify a ~ Foo a
 517
 518 uUnrefined subst tv1 ty2 (TyVarTy tv2)
 519   | tv1 == tv2          -- Same type variable
 520   = return subst
 521
 522     -- Check to see whether tv2 is refined
 523   | Just ty' <- lookupVarEnv subst tv2
 524   = uUnrefined subst tv1 ty' ty'
 525
 526   -- So both are unrefined; next, see if the kinds force the direction
 527   | eqKind k1 k2        -- Can update either; so check the bind-flags
 528   = do  { b1 <- tvBindFlag tv1
 529         ; b2 <- tvBindFlag tv2
 530         ; case (b1,b2) of
 531             (BindMe, _)          -> bind tv1 ty2
 532             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
 533             (Skolem, _)          -> bind tv2 ty1
 534         }
 535
 536   | k1 `isSubKind` k2 = bindTv subst tv2 ty1  -- Must update tv2
 537   | k2 `isSubKind` k1 = bindTv subst tv1 ty2  -- Must update tv1
 538
 539   | otherwise = failWith (kindMisMatch tv1 ty2)
 540   where
 541     ty1 = TyVarTy tv1
 542     k1 = tyVarKind tv1
 543     k2 = tyVarKind tv2
 544     bind tv ty = return $ extendVarEnv subst tv ty
 545
 546 uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
 547   | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
 548   = failWith (occursCheck tv1 ty2)      -- Occurs check
 549   | not (k2 `isSubKind` k1)
 550   = failWith (kindMisMatch tv1 ty2)     -- Kind check
 551   | otherwise
 552   = bindTv subst tv1 ty2                -- Bind tyvar to the synonym if poss
 553   where
 554     k1 = tyVarKind tv1
 555     k2 = typeKind ty2'
 556
 557 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
 558 bindTv subst tv ty      -- ty is not a type variable
 559   = do  { b <- tvBindFlag tv
 560         ; case b of
 561             Skolem -> failWith (misMatch (TyVarTy tv) ty)
 562             BindMe -> return $ extendVarEnv subst tv ty
 563         }
 564 \end{code}
 565
 566 %************************************************************************
 567 %*                                                                      *
 568                 Binding decisions
 569 %*                                                                      *
 570 %************************************************************************
 571
 572 \begin{code}
 573 data BindFlag
 574   = BindMe      -- A regular type variable
 575
 576   | Skolem      -- This type variable is a skolem constant
 577                 -- Don't bind it; it only matches itself
 578 \end{code}
 579
 580
 581 %************************************************************************
 582 %*                                                                      *
 583                 Unification monad
 584 %*                                                                      *
 585 %************************************************************************
 586
 587 \begin{code}
 588 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 589                          -> MaybeErr Message a }
 590
 591 instance Monad UM where
 592   return a = UM (\_tvs -> Succeeded a)
 593   fail s   = UM (\_tvs -> Failed (text s))
 594   m >>= k  = UM (\tvs -> case unUM m tvs of
 595                            Failed err -> Failed err
 596                            Succeeded v  -> unUM (k v) tvs)
 597
 598 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
 599 initUM badtvs um = unUM um badtvs
 600
 601 tvBindFlag :: TyVar -> UM BindFlag
 602 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
 603
 604 failWith :: Message -> UM a
 605 failWith msg = UM (\_tv_fn -> Failed msg)
 606
 607 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
 608 maybeErrToMaybe (Succeeded a) = Just a
 609 maybeErrToMaybe (Failed _)    = Nothing
 610 \end{code}
 611
 612
 613 %************************************************************************
 614 %*                                                                      *
 615                 Error reporting
 616         We go to a lot more trouble to tidy the types
 617         in TcUnify.  Maybe we'll end up having to do that
 618         here too, but I'll leave it for now.
 619 %*                                                                      *
 620 %************************************************************************
 621
 622 \begin{code}
 623 misMatch :: Type -> Type -> SDoc
 624 misMatch t1 t2
 625   = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+>
 626     ptext (sLit "and") <+> quotes (ppr t2)
 627
 628 lengthMisMatch :: [Type] -> [Type] -> SDoc
 629 lengthMisMatch tys1 tys2
 630   = sep [ptext (sLit "Can't match unequal length lists"),
 631          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 632
 633 kindMisMatch :: TyVar -> Type -> SDoc
 634 kindMisMatch tv1 t2
 635   = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
 636             ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
 637           ptext (sLit "when matching") <+> quotes (ppr tv1) <+>
 638                 ptext (sLit "with") <+> quotes (ppr t2)]
 639
 640 occursCheck :: TyVar -> Type -> SDoc
 641 occursCheck tv ty
 642   = hang (ptext (sLit "Can't construct the infinite type"))
 643        2 (ppr tv <+> equals <+> ppr ty)
 644 \end{code}