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