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