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) = coVarKind 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 :: [TyVar] -> [Coercion] -> 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 in_scope_tvs cos
 466   = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos))
 467   where
 468     in_scope = mkInScopeSet (mkVarSet in_scope_tvs)
 469         -- NB: in_scope_tvs include both coercion variables
 470         --     *and* the tyvars in their kinds
 471
 472     refineOne co = refine co ty1 ty2
 473       where
 474         (ty1, ty2) = coercionKind co
 475
 476     refine co (TyVarTy tv) ty                     = unitVarEnv tv (co, ty)
 477     refine co (TyConApp _ tys) (TyConApp _ tys')  = refineArgs co tys tys'
 478     refine _  (PredTy _) (PredTy _)               =
 479       error "Unify.matchRefine: PredTy"
 480     refine co (FunTy arg res) (FunTy arg' res')   =
 481       refine (mkRightCoercion (mkLeftCoercion co)) arg arg'
 482       `plusVarEnv`
 483       refine (mkRightCoercion co) res res'
 484     refine co (AppTy fun arg) (AppTy fun' arg')   =
 485       refine (mkLeftCoercion co) fun fun'
 486       `plusVarEnv`
 487       refine (mkRightCoercion co) arg arg'
 488     refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
 489       refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
 490     refine _ _ _ = error "RcGadt.matchRefine: mismatch"
 491
 492     refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
 493     refineArgs co tys tys' =
 494       fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
 495       where
 496         refineArg (ty, ty') (reft, coWrapper)
 497           = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
 498              mkLeftCoercion . coWrapper)
 499 \end{code}
 500
 501
 502 %************************************************************************
 503 %*                                                                      *
 504                 Unification
 505 %*                                                                      *
 506 %************************************************************************
 507
 508 \begin{code}
 509 tcUnifyTys :: (TyVar -> BindFlag)
 510            -> [Type] -> [Type]
 511            -> Maybe TvSubst     -- A regular one-shot substitution
 512 -- The two types may have common type variables, and indeed do so in the
 513 -- second call to tcUnifyTys in FunDeps.checkClsFD
 514 --
 515 tcUnifyTys bind_fn tys1 tys2
 516   = maybeErrToMaybe $ initUM bind_fn $
 517     do { subst <- unifyList emptyTvSubstEnv tys1 tys2
 518
 519         -- Find the fixed point of the resulting non-idempotent substitution
 520         ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
 521               tv_env   = fixTvSubstEnv in_scope subst
 522
 523         ; return (mkTvSubst in_scope tv_env) }
 524   where
 525     tvs1 = tyVarsOfTypes tys1
 526     tvs2 = tyVarsOfTypes tys2
 527
 528 ----------------------------
 529 -- XXX Can we do this more nicely, by exploiting laziness?
 530 -- Or avoid needing it in the first place?
 531 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
 532 fixTvSubstEnv in_scope env = f env
 533   where
 534     f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
 535           in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
 536              then e
 537              else f e'
 538
 539 \end{code}
 540
 541
 542 %************************************************************************
 543 %*                                                                      *
 544                 The workhorse
 545 %*                                                                      *
 546 %************************************************************************
 547
 548 \begin{code}
 549 unify :: TvSubstEnv     -- An existing substitution to extend
 550       -> Type -> Type   -- Types to be unified, and witness of their equality
 551       -> UM TvSubstEnv          -- Just the extended substitution,
 552                                 -- Nothing if unification failed
 553 -- We do not require the incoming substitution to be idempotent,
 554 -- nor guarantee that the outgoing one is.  That's fixed up by
 555 -- the wrappers.
 556
 557 -- Respects newtypes, PredTypes
 558
 559 -- in unify, any NewTcApps/Preds should be taken at face value
 560 unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
 561 unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
 562
 563 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
 564 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
 565
 566 unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
 567
 568 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
 569   | tyc1 == tyc2 = unify_tys subst tys1 tys2
 570
 571 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 572   = do  { subst' <- unify subst ty1a ty2a
 573         ; unify subst' ty1b ty2b }
 574
 575         -- Applications need a bit of care!
 576         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 577         -- NB: we've already dealt with type variables and Notes,
 578         -- so if one type is an App the other one jolly well better be too
 579 unify subst (AppTy ty1a ty1b) ty2
 580   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 581   = do  { subst' <- unify subst ty1a ty2a
 582         ; unify subst' ty1b ty2b }
 583
 584 unify subst ty1 (AppTy ty2a ty2b)
 585   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 586   = do  { subst' <- unify subst ty1a ty2a
 587         ; unify subst' ty1b ty2b }
 588
 589 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
 590         -- ForAlls??
 591
 592 ------------------------------
 593 unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
 594 unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
 595   | c1 == c2 = unify_tys subst tys1 tys2
 596 unify_pred subst (IParam n1 t1) (IParam n2 t2)
 597   | n1 == n2 = unify subst t1 t2
 598 unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 599
 600 ------------------------------
 601 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 602 unify_tys subst xs ys = unifyList subst xs ys
 603
 604 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 605 unifyList subst orig_xs orig_ys
 606   = go subst orig_xs orig_ys
 607   where
 608     go subst []     []     = return subst
 609     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
 610                                 ; go subst' xs ys }
 611     go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
 612
 613 ---------------------------------
 614 uVar :: TvSubstEnv      -- An existing substitution to extend
 615      -> TyVar           -- Type variable to be unified
 616      -> Type            -- with this type
 617      -> UM TvSubstEnv
 618
 619 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
 620 --      if swap=False   (tv1~ty)
 621 --      if swap=True    (ty~tv1)
 622
 623 uVar subst tv1 ty
 624  = -- Check to see whether tv1 is refined by the substitution
 625    case (lookupVarEnv subst tv1) of
 626      Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
 627      Nothing  -> uUnrefined subst       -- No, continue
 628                             tv1 ty ty
 629
 630 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
 631            -> TyVar               -- Type variable to be unified
 632            -> Type                -- with this type
 633            -> Type                -- (version w/ expanded synonyms)
 634            -> UM TvSubstEnv
 635
 636 -- We know that tv1 isn't refined
 637
 638 uUnrefined subst tv1 ty2 ty2'
 639   | Just ty2'' <- tcView ty2'
 640   = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
 641                 -- This is essential, in case we have
 642                 --      type Foo a = a
 643                 -- and then unify a ~ Foo a
 644
 645 uUnrefined subst tv1 ty2 (TyVarTy tv2)
 646   | tv1 == tv2          -- Same type variable
 647   = return subst
 648
 649     -- Check to see whether tv2 is refined
 650   | Just ty' <- lookupVarEnv subst tv2
 651   = uUnrefined subst tv1 ty' ty'
 652
 653   -- So both are unrefined; next, see if the kinds force the direction
 654   | eqKind k1 k2        -- Can update either; so check the bind-flags
 655   = do  { b1 <- tvBindFlag tv1
 656         ; b2 <- tvBindFlag tv2
 657         ; case (b1,b2) of
 658             (BindMe, _)          -> bind tv1 ty2
 659             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
 660             (Skolem, _)          -> bind tv2 ty1
 661         }
 662
 663   | k1 `isSubKind` k2 = bindTv subst tv2 ty1  -- Must update tv2
 664   | k2 `isSubKind` k1 = bindTv subst tv1 ty2  -- Must update tv1
 665
 666   | otherwise = failWith (kindMisMatch tv1 ty2)
 667   where
 668     ty1 = TyVarTy tv1
 669     k1 = tyVarKind tv1
 670     k2 = tyVarKind tv2
 671     bind tv ty = return $ extendVarEnv subst tv ty
 672
 673 uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
 674   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
 675   = failWith (occursCheck tv1 ty2)      -- Occurs check
 676   | not (k2 `isSubKind` k1)
 677   = failWith (kindMisMatch tv1 ty2)     -- Kind check
 678   | otherwise
 679   = bindTv subst tv1 ty2                -- Bind tyvar to the synonym if poss
 680   where
 681     k1 = tyVarKind tv1
 682     k2 = typeKind ty2'
 683
 684 substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
 685 -- Apply the non-idempotent substitution to a set of type variables,
 686 -- remembering that the substitution isn't necessarily idempotent
 687 substTvSet subst tvs
 688   = foldVarSet (unionVarSet . get) emptyVarSet tvs
 689   where
 690     get tv = case lookupVarEnv subst tv of
 691                Nothing -> unitVarSet tv
 692                Just ty -> substTvSet subst (tyVarsOfType ty)
 693
 694 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
 695 bindTv subst tv ty      -- ty is not a type variable
 696   = do  { b <- tvBindFlag tv
 697         ; case b of
 698             Skolem -> failWith (misMatch (TyVarTy tv) ty)
 699             BindMe -> return $ extendVarEnv subst tv ty
 700         }
 701 \end{code}
 702
 703 %************************************************************************
 704 %*                                                                      *
 705                 Binding decisions
 706 %*                                                                      *
 707 %************************************************************************
 708
 709 \begin{code}
 710 data BindFlag
 711   = BindMe      -- A regular type variable
 712
 713   | Skolem      -- This type variable is a skolem constant
 714                 -- Don't bind it; it only matches itself
 715 \end{code}
 716
 717
 718 %************************************************************************
 719 %*                                                                      *
 720                 Unification monad
 721 %*                                                                      *
 722 %************************************************************************
 723
 724 \begin{code}
 725 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 726                          -> MaybeErr Message a }
 727
 728 instance Monad UM where
 729   return a = UM (\_tvs -> Succeeded a)
 730   fail s   = UM (\_tvs -> Failed (text s))
 731   m >>= k  = UM (\tvs -> case unUM m tvs of
 732                            Failed err -> Failed err
 733                            Succeeded v  -> unUM (k v) tvs)
 734
 735 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
 736 initUM badtvs um = unUM um badtvs
 737
 738 tvBindFlag :: TyVar -> UM BindFlag
 739 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
 740
 741 failWith :: Message -> UM a
 742 failWith msg = UM (\_tv_fn -> Failed msg)
 743
 744 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
 745 maybeErrToMaybe (Succeeded a) = Just a
 746 maybeErrToMaybe (Failed _)    = Nothing
 747 \end{code}
 748
 749
 750 %************************************************************************
 751 %*                                                                      *
 752                 Error reporting
 753         We go to a lot more trouble to tidy the types
 754         in TcUnify.  Maybe we'll end up having to do that
 755         here too, but I'll leave it for now.
 756 %*                                                                      *
 757 %************************************************************************
 758
 759 \begin{code}
 760 misMatch :: Type -> Type -> SDoc
 761 misMatch t1 t2
 762   = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+>
 763     ptext (sLit "and") <+> quotes (ppr t2)
 764
 765 lengthMisMatch :: [Type] -> [Type] -> SDoc
 766 lengthMisMatch tys1 tys2
 767   = sep [ptext (sLit "Can't match unequal length lists"),
 768          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 769
 770 kindMisMatch :: TyVar -> Type -> SDoc
 771 kindMisMatch tv1 t2
 772   = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
 773             ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
 774           ptext (sLit "when matching") <+> quotes (ppr tv1) <+>
 775                 ptext (sLit "with") <+> quotes (ppr t2)]
 776
 777 occursCheck :: TyVar -> Type -> SDoc
 778 occursCheck tv ty
 779   = hang (ptext (sLit "Can't construct the infinite type"))
 780        2 (ppr tv <+> equals <+> ppr ty)
 781 \end{code}