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