ghc/compiler/typecheck/TcUnify.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[Unify]{Unifier}
   5
   6 The unifier is now squarely in the typechecker monad (because of the
   7 updatable substitution).
   8
   9 \begin{code}
  10 module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
  11                  unifyFunTy, unifyListTy, unifyTupleTy,
  12                  unifyKind, unifyKinds, unifyTypeKind
  13  ) where
  14
  15 #include "HsVersions.h"
  16
  17 -- friends:
  18 import TcMonad
  19 import TypeRep  ( Type(..), funTyCon,
  20                   Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind,
  21                 )  -- friend
  22 import Type     ( tyVarsOfType,
  23                   mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
  24                   isNotUsgTy,
  25                   splitAppTy_maybe,
  26                   tidyOpenType, tidyOpenTypes, tidyTyVar
  27                 )
  28 import TyCon    ( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
  29 import Name     ( hasBetterProv )
  30 import Var      ( TyVar, tyVarKind, varName, isSigTyVar )
  31 import VarEnv
  32 import VarSet   ( varSetElems )
  33 import TcType   ( TcType, TcTauType, TcTyVar, TcKind,
  34                   newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind,
  35                   tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind
  36                 )
  37 -- others:
  38 import BasicTypes ( Arity, Boxity, isBoxed )
  39 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
  40 import PprType  ()              -- Instances
  41 import Util
  42 import Outputable
  43 \end{code}
  44
  45
  46 %************************************************************************
  47 %*                                                                      *
  48 \subsection{The Kind variants}
  49 %*                                                                      *
  50 %************************************************************************
  51
  52 \begin{code}
  53 unifyKind :: TcKind                 -- Expected
  54           -> TcKind                 -- Actual
  55           -> TcM s ()
  56 unifyKind k1 k2
  57   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
  58     uTys k1 k1 k2 k2
  59
  60 unifyKinds :: [TcKind] -> [TcKind] -> TcM s ()
  61 unifyKinds []       []       = returnTc ()
  62 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenTc_`
  63                                unifyKinds ks1 ks2
  64 unifyKinds _ _ = panic "unifyKinds: length mis-match"
  65 \end{code}
  66
  67
  68 %************************************************************************
  69 %*                                                                      *
  70 \subsection[Unify-exported]{Exported unification functions}
  71 %*                                                                      *
  72 %************************************************************************
  73
  74 The exported functions are all defined as versions of some
  75 non-exported generic functions.
  76
  77 Unify two @TauType@s.  Dead straightforward.
  78
  79 \begin{code}
  80 unifyTauTy :: TcTauType -> TcTauType -> TcM s ()
  81 unifyTauTy ty1 ty2      -- ty1 expected, ty2 inferred
  82   = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
  83     uTys ty1 ty1 ty2 ty2
  84 \end{code}
  85
  86 @unifyTauTyList@ unifies corresponding elements of two lists of
  87 @TauType@s.  It uses @uTys@ to do the real work.  The lists should be
  88 of equal length.  We charge down the list explicitly so that we can
  89 complain if their lengths differ.
  90
  91 \begin{code}
  92 unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM s ()
  93 unifyTauTyLists []           []         = returnTc ()
  94 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2   `thenTc_`
  95                                         unifyTauTyLists tys1 tys2
  96 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
  97 \end{code}
  98
  99 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
 100 all together.  It is used, for example, when typechecking explicit
 101 lists, when all the elts should be of the same type.
 102
 103 \begin{code}
 104 unifyTauTyList :: [TcTauType] -> TcM s ()
 105 unifyTauTyList []                = returnTc ()
 106 unifyTauTyList [ty]              = returnTc ()
 107 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2   `thenTc_`
 108                                    unifyTauTyList tys
 109 \end{code}
 110
 111 %************************************************************************
 112 %*                                                                      *
 113 \subsection[Unify-uTys]{@uTys@: getting down to business}
 114 %*                                                                      *
 115 %************************************************************************
 116
 117 @uTys@ is the heart of the unifier.  Each arg happens twice, because
 118 we want to report errors in terms of synomyms if poss.  The first of
 119 the pair is used in error messages only; it is always the same as the
 120 second, except that if the first is a synonym then the second may be a
 121 de-synonym'd version.  This way we get better error messages.
 122
 123 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 124
 125 \begin{code}
 126 uTys :: TcTauType -> TcTauType  -- Error reporting ty1 and real ty1
 127      -> TcTauType -> TcTauType  -- Error reporting ty2 and real ty2
 128      -> TcM s ()
 129
 130         -- Always expand synonyms (see notes at end)
 131         -- (this also throws away FTVs and usage annots)
 132 uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 133 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 134
 135         -- Variables; go for uVar
 136 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
 137 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
 138                                         -- "True" means args swapped
 139
 140         -- Functions; just check the two parts
 141 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
 142   = uTys fun1 fun1 fun2 fun2    `thenTc_`    uTys arg1 arg1 arg2 arg2
 143
 144         -- Type constructors must match
 145 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
 146   = checkTcM (cons_match && length tys1 == length tys2)
 147              (unifyMisMatch ps_ty1 ps_ty2)                      `thenTc_`
 148     unifyTauTyLists tys1 tys2
 149   where
 150         -- The AnyBox wild card matches anything
 151     cons_match =  con1 == con2
 152                || con1 == anyBoxCon
 153                || con2 == anyBoxCon
 154
 155         -- Applications need a bit of care!
 156         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 157         -- NB: we've already dealt with type variables and Notes,
 158         -- so if one type is an App the other one jolly well better be too
 159 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
 160   = case splitAppTy_maybe ty2 of
 161         Just (s2,t2) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 162         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 163
 164         -- Now the same, but the other way round
 165         -- Don't swap the types, because the error messages get worse
 166 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
 167   = case splitAppTy_maybe ty1 of
 168         Just (s1,t1) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 169         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 170
 171         -- Not expecting for-alls in unification
 172         -- ... but the error message from the unifyMisMatch more informative
 173         -- than a panic message!
 174
 175         -- Anything else fails
 176 uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
 177 \end{code}
 178
 179 Notes on synonyms
 180 ~~~~~~~~~~~~~~~~~
 181 If you are tempted to make a short cut on synonyms, as in this
 182 pseudocode...
 183
 184 \begin{verbatim}
 185 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
 186   = if (con1 == con2) then
 187         -- Good news!  Same synonym constructors, so we can shortcut
 188         -- by unifying their arguments and ignoring their expansions.
 189         unifyTauTypeLists args1 args2
 190     else
 191         -- Never mind.  Just expand them and try again
 192         uTys ty1 ty2
 193 \end{verbatim}
 194
 195 then THINK AGAIN.  Here is the whole story, as detected and reported
 196 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
 197 \begin{quotation}
 198 Here's a test program that should detect the problem:
 199
 200 \begin{verbatim}
 201         type Bogus a = Int
 202         x = (1 :: Bogus Char) :: Bogus Bool
 203 \end{verbatim}
 204
 205 The problem with [the attempted shortcut code] is that
 206 \begin{verbatim}
 207         con1 == con2
 208 \end{verbatim}
 209 is not a sufficient condition to be able to use the shortcut!
 210 You also need to know that the type synonym actually USES all
 211 its arguments.  For example, consider the following type synonym
 212 which does not use all its arguments.
 213 \begin{verbatim}
 214         type Bogus a = Int
 215 \end{verbatim}
 216
 217 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
 218 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
 219 would fail, even though the expanded forms (both \tr{Int}) should
 220 match.
 221
 222 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 223 unnecessarily bind \tr{t} to \tr{Char}.
 224
 225 ... You could explicitly test for the problem synonyms and mark them
 226 somehow as needing expansion, perhaps also issuing a warning to the
 227 user.
 228 \end{quotation}
 229
 230
 231 %************************************************************************
 232 %*                                                                      *
 233 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 234 %*                                                                      *
 235 %************************************************************************
 236
 237 @uVar@ is called when at least one of the types being unified is a
 238 variable.  It does {\em not} assume that the variable is a fixed point
 239 of the substitution; rather, notice that @uVar@ (defined below) nips
 240 back into @uTys@ if it turns out that the variable is already bound.
 241
 242 \begin{code}
 243 uVar :: Bool            -- False => tyvar is the "expected"
 244                         -- True  => ty    is the "expected" thing
 245      -> TcTyVar
 246      -> TcTauType -> TcTauType  -- printing and real versions
 247      -> TcM s ()
 248
 249 uVar swapped tv1 ps_ty2 ty2
 250   = tcGetTyVar tv1      `thenNF_Tc` \ maybe_ty1 ->
 251     case maybe_ty1 of
 252         Just ty1 | swapped   -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
 253                  | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
 254         other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 255
 256         -- Expand synonyms; ignore FTVs; ignore usage annots
 257 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
 258   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 259
 260
 261         -- The both-type-variable case
 262 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 263
 264         -- Same type variable => no-op
 265   | tv1 == tv2
 266   = returnTc ()
 267
 268         -- Distinct type variables
 269         -- ASSERT maybe_ty1 /= Just
 270   | otherwise
 271   = tcGetTyVar tv2      `thenNF_Tc` \ maybe_ty2 ->
 272     case maybe_ty2 of
 273         Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 274
 275         Nothing -> checkKinds swapped tv1 ty2                   `thenTc_`
 276
 277                    if tv1 `dominates` tv2 then
 278                         tcPutTyVar tv2 (TyVarTy tv1)            `thenNF_Tc_`
 279                         returnTc ()
 280                    else
 281                         ASSERT( isNotUsgTy ps_ty2 )
 282                         tcPutTyVar tv1 ps_ty2                   `thenNF_Tc_`
 283                         returnTc ()
 284   where
 285     tv1 `dominates` tv2 =  isSigTyVar tv1
 286                                 -- Don't unify a signature type variable if poss
 287                         || varName tv1 `hasBetterProv` varName tv2
 288                                 -- Try to update sys-y type variables in preference to sig-y ones
 289
 290         -- Second one isn't a type variable
 291 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
 292   | non_var_ty2 == anyBoxKind
 293         -- If the
 294   = returnTc ()
 295
 296   | otherwise
 297   = checkKinds swapped tv1 non_var_ty2                  `thenTc_`
 298     occur_check non_var_ty2                             `thenTc_`
 299     ASSERT( isNotUsgTy ps_ty2 )
 300     checkTcM (not (isSigTyVar tv1))
 301              (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
 302
 303     tcPutTyVar tv1 non_var_ty2                          `thenNF_Tc_`
 304         -- This used to say "ps_ty2" instead of "non_var_ty2"
 305
 306         -- But that led to an infinite loop in the type checker!
 307         -- Consider
 308         --      type A a = ()
 309         --
 310         --      f :: (A a -> a -> ()) -> ()
 311         --      f = \ _ -> ()
 312         --
 313         --      x :: ()
 314         --      x = f (\ x p -> p x)
 315         --
 316         -- Here, we try to match "t" with "A t", and succeed
 317         -- because the unifier looks through synonyms.  The occurs
 318         -- check doesn't kick in because we are "really" binding "t" to "()",
 319         -- but we *actually* bind "t" to "A t" if we store ps_ty2.
 320         -- That leads the typechecker into an infinite loop later.
 321
 322     returnTc ()
 323   where
 324     occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty))       `thenTc_`
 325                      returnTc ()
 326
 327     occur_check_tv tv2
 328        | tv1 == tv2             -- Same tyvar; fail
 329        = zonkTcType ps_ty2      `thenNF_Tc` \ zonked_ty2 ->
 330          failWithTcM (unifyOccurCheck tv1 zonked_ty2)
 331
 332        | otherwise              -- A different tyvar
 333        = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
 334          case maybe_ty2 of
 335                 Just ty2' -> occur_check ty2'
 336                 other     -> returnTc ()
 337
 338 checkKinds swapped tv1 ty2
 339   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)       $
 340
 341         -- We have to use tcTypeKind not just typeKind to get the
 342         -- kind of ty2, because there might be mutable kind variables
 343         -- in the way.  For example, suppose that ty2 :: (a b), and
 344         -- the kind of 'a' is a kind variable 'k' that has (presumably)
 345         -- been unified with 'k1 -> k2'.
 346     tcTypeKind ty2              `thenNF_Tc` \ k2 ->
 347
 348     if swapped then
 349         unifyKind k2 (tyVarKind tv1)
 350     else
 351         unifyKind (tyVarKind tv1) k2
 352 \end{code}
 353
 354 %************************************************************************
 355 %*                                                                      *
 356 \subsection[Unify-fun]{@unifyFunTy@}
 357 %*                                                                      *
 358 %************************************************************************
 359
 360 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
 361
 362 \begin{code}
 363 unifyFunTy :: TcType                            -- Fail if ty isn't a function type
 364            -> TcM s (TcType, TcType)    -- otherwise return arg and result types
 365
 366 unifyFunTy ty@(TyVarTy tyvar)
 367   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 368     case maybe_ty of
 369         Just ty' -> unifyFunTy ty'
 370         other       -> unify_fun_ty_help ty
 371
 372 unifyFunTy ty
 373   = case splitFunTy_maybe ty of
 374         Just arg_and_res -> returnTc arg_and_res
 375         Nothing          -> unify_fun_ty_help ty
 376
 377 unify_fun_ty_help ty    -- Special cases failed, so revert to ordinary unification
 378   = newTyVarTy_OpenKind         `thenNF_Tc` \ arg ->
 379     newTyVarTy_OpenKind         `thenNF_Tc` \ res ->
 380     unifyTauTy ty (mkFunTy arg res)     `thenTc_`
 381     returnTc (arg,res)
 382 \end{code}
 383
 384 \begin{code}
 385 unifyListTy :: TcType              -- expected list type
 386             -> TcM s TcType      -- list element type
 387
 388 unifyListTy ty@(TyVarTy tyvar)
 389   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 390     case maybe_ty of
 391         Just ty' -> unifyListTy ty'
 392         other       -> unify_list_ty_help ty
 393
 394 unifyListTy ty
 395   = case splitTyConApp_maybe ty of
 396         Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
 397         other                                       -> unify_list_ty_help ty
 398
 399 unify_list_ty_help ty   -- Revert to ordinary unification
 400   = newTyVarTy boxedTypeKind            `thenNF_Tc` \ elt_ty ->
 401     unifyTauTy ty (mkListTy elt_ty)     `thenTc_`
 402     returnTc elt_ty
 403 \end{code}
 404
 405 \begin{code}
 406 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM s [TcType]
 407 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
 408   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 409     case maybe_ty of
 410         Just ty' -> unifyTupleTy boxity arity ty'
 411         other    -> unify_tuple_ty_help boxity arity ty
 412
 413 unifyTupleTy boxity arity ty
 414   = case splitTyConApp_maybe ty of
 415         Just (tycon, arg_tys)
 416                 |  isTupleTyCon tycon
 417                 && tyConArity tycon == arity
 418                 && tupleTyConBoxity tycon == boxity
 419                 -> returnTc arg_tys
 420         other -> unify_tuple_ty_help boxity arity ty
 421
 422 unify_tuple_ty_help boxity arity ty
 423   = mapNF_Tc new_tyvar [1..arity]                       `thenNF_Tc` \ arg_tys ->
 424     unifyTauTy ty (mkTupleTy boxity arity arg_tys)      `thenTc_`
 425     returnTc arg_tys
 426   where
 427     new_tyvar _ | isBoxed boxity = newTyVarTy boxedTypeKind
 428                 | otherwise      = newTyVarTy_OpenKind
 429 \end{code}
 430
 431 Make sure a kind is of the form (Type b) for some boxity b.
 432
 433 \begin{code}
 434 unifyTypeKind  :: TcKind -> TcM s ()
 435 unifyTypeKind kind@(TyVarTy kv)
 436   = tcGetTyVar kv       `thenNF_Tc` \ maybe_kind ->
 437     case maybe_kind of
 438         Just kind' -> unifyTypeKind kind'
 439         Nothing    -> unify_type_kind_help kind
 440
 441 unifyTypeKind kind
 442   = case splitTyConApp_maybe kind of
 443         Just (tycon, [_]) | tycon == typeCon -> returnTc ()
 444         other                                -> unify_type_kind_help kind
 445
 446 unify_type_kind_help kind
 447   = newOpenTypeKind     `thenNF_Tc` \ expected_kind ->
 448     unifyKind expected_kind kind
 449 \end{code}
 450
 451
 452 %************************************************************************
 453 %*                                                                      *
 454 \subsection[Unify-context]{Errors and contexts}
 455 %*                                                                      *
 456 %************************************************************************
 457
 458 Errors
 459 ~~~~~~
 460
 461 \begin{code}
 462 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
 463   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 464     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 465     returnNF_Tc (err ty1' ty2')
 466   where
 467     err ty1 ty2 = (env1,
 468                    nest 4
 469                         (vcat [
 470                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
 471                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
 472                         ]))
 473                   where
 474                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
 475
 476 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
 477   = returnNF_Tc (env2, ptext SLIT("When matching types") <+>
 478                        sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
 479   where
 480     (pp_expected, pp_actual) | swapped   = (pp2, pp1)
 481                              | otherwise = (pp1, pp2)
 482     (env1, tv1') = tidyTyVar tidy_env tv1
 483     (env2, ty2') = tidyOpenType  env1     ty2
 484     pp1 = ppr tv1'
 485     pp2 = ppr ty2'
 486
 487 unifyMisMatch ty1 ty2
 488   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 489     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 490     let
 491         (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
 492         msg = hang (ptext SLIT("Couldn't match"))
 493                    4 (sep [quotes (ppr tidy_ty1),
 494                            ptext SLIT("against"),
 495                            quotes (ppr tidy_ty2)])
 496     in
 497     failWithTcM (env, msg)
 498
 499 unifyWithSigErr tyvar ty
 500   = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
 501               4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
 502   where
 503     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
 504     (env2, tidy_ty)    = tidyOpenType  env1     ty
 505
 506 unifyOccurCheck tyvar ty
 507   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
 508               4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
 509   where
 510     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
 511     (env2, tidy_ty)    = tidyOpenType  env1     ty
 512 \end{code}
 513