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