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