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
  13  ) where
  14
  15 #include "HsVersions.h"
  16
  17 -- friends:
  18 import TcMonad
  19 import TcEnv    ( tidyType, tidyTypes, tidyTyVar )
  20 import Type     ( GenType(..), Type, tyVarsOfType, funTyCon,
  21                   typeKind, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
  22                   Kind, hasMoreBoxityInfo, openTypeKind, boxedTypeKind, superKind,
  23                   splitAppTy_maybe
  24                 )
  25 import TyCon    ( TyCon, isTupleTyCon, isUnboxedTupleTyCon,
  26                   tyConArity, matchesTyCon )
  27 import Name     ( isSysLocalName )
  28 import Var      ( TyVar, tyVarKind, varName )
  29 import VarEnv
  30 import VarSet   ( varSetElems )
  31 import TcType   ( TcType, TcMaybe(..), TcTauType, TcTyVar,
  32                   TcKind,
  33                   newTyVarTy, tcReadTyVar, tcWriteTyVar, zonkTcType
  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 s               -- Expected
  52           -> TcKind s               -- Actual
  53           -> TcM s ()
  54 unifyKind k1 k2
  55   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
  56     uTys k1 k1 k2 k2
  57
  58 unifyKinds :: [TcKind s] -> [TcKind s] -> 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 s -> TcTauType s -> 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 s] -> [TcTauType s] ->  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 s] -> 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 s -> TcTauType s      -- Error reporting ty1 and real ty1
 125      -> TcTauType s -> TcTauType s      -- 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 (con1 `matchesTyCon` con2 && length tys1 == length tys2)
 144              (failWithTcM (unifyMisMatch ps_ty1 ps_ty2))                `thenTc_`
 145     unifyTauTyLists tys1 tys2
 146
 147         -- Applications need a bit of care!
 148         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 149         -- NB: we've already dealt with type variables and Notes,
 150         -- so if one type is an App the other one jolly well better be too
 151 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
 152   = case splitAppTy_maybe ty2 of
 153         Just (s2,t2) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 154         Nothing      -> failWithTcM (unifyMisMatch ps_ty1 ps_ty2)
 155
 156         -- Now the same, but the other way round
 157         -- ** DON'T ** swap the types, because when unifying kinds
 158         -- we need to check that the expected type has less boxity info
 159         -- than the inferred one; so we need to keep them the right way round
 160 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
 161   = case splitAppTy_maybe ty1 of
 162         Just (s1,t1) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 163         Nothing      -> failWithTcM (unifyMisMatch ps_ty1 ps_ty2)
 164
 165         -- Not expecting for-alls in unification
 166         -- ... but the error message from the unifyMisMatch more informative
 167         -- than a panic message!
 168
 169         -- Anything else fails
 170 uTys ps_ty1 ty1 ps_ty2 ty2  = failWithTcM (unifyMisMatch ps_ty1 ps_ty2)
 171 \end{code}
 172
 173 Notes on synonyms
 174 ~~~~~~~~~~~~~~~~~
 175 If you are tempted to make a short cut on synonyms, as in this
 176 pseudocode...
 177
 178 \begin{verbatim}
 179 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
 180   = if (con1 == con2) then
 181         -- Good news!  Same synonym constructors, so we can shortcut
 182         -- by unifying their arguments and ignoring their expansions.
 183         unifyTauTypeLists args1 args2
 184     else
 185         -- Never mind.  Just expand them and try again
 186         uTys ty1 ty2
 187 \end{verbatim}
 188
 189 then THINK AGAIN.  Here is the whole story, as detected and reported
 190 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
 191 \begin{quotation}
 192 Here's a test program that should detect the problem:
 193
 194 \begin{verbatim}
 195         type Bogus a = Int
 196         x = (1 :: Bogus Char) :: Bogus Bool
 197 \end{verbatim}
 198
 199 The problem with [the attempted shortcut code] is that
 200 \begin{verbatim}
 201         con1 == con2
 202 \end{verbatim}
 203 is not a sufficient condition to be able to use the shortcut!
 204 You also need to know that the type synonym actually USES all
 205 its arguments.  For example, consider the following type synonym
 206 which does not use all its arguments.
 207 \begin{verbatim}
 208         type Bogus a = Int
 209 \end{verbatim}
 210
 211 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
 212 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
 213 would fail, even though the expanded forms (both \tr{Int}) should
 214 match.
 215
 216 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 217 unnecessarily bind \tr{t} to \tr{Char}.
 218
 219 ... You could explicitly test for the problem synonyms and mark them
 220 somehow as needing expansion, perhaps also issuing a warning to the
 221 user.
 222 \end{quotation}
 223
 224
 225 %************************************************************************
 226 %*                                                                      *
 227 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 228 %*                                                                      *
 229 %************************************************************************
 230
 231 @uVar@ is called when at least one of the types being unified is a
 232 variable.  It does {\em not} assume that the variable is a fixed point
 233 of the substitution; rather, notice that @uVar@ (defined below) nips
 234 back into @uTys@ if it turns out that the variable is already bound.
 235
 236 \begin{code}
 237 uVar :: Bool            -- False => tyvar is the "expected"
 238                         -- True  => ty    is the "expected" thing
 239      -> TcTyVar s
 240      -> TcTauType s -> TcTauType s      -- printing and real versions
 241      -> TcM s ()
 242
 243 uVar swapped tv1 ps_ty2 ty2
 244   = tcReadTyVar tv1     `thenNF_Tc` \ maybe_ty1 ->
 245     case maybe_ty1 of
 246         BoundTo ty1 | swapped   -> uTys ps_ty2 ty2 ty1 ty1      -- Swap back
 247                     | otherwise -> uTys ty1 ty1 ps_ty2 ty2      -- Same order
 248         other       -> uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
 249
 250         -- Expand synonyms
 251 uUnboundVar tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
 252   = uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
 253
 254
 255         -- The both-type-variable case
 256 uUnboundVar tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 257
 258         -- Same type variable => no-op
 259   | tv1 == tv2
 260   = returnTc ()
 261
 262         -- Distinct type variables
 263         -- ASSERT maybe_ty1 /= BoundTo
 264   | otherwise
 265   = tcReadTyVar tv2     `thenNF_Tc` \ maybe_ty2 ->
 266     case maybe_ty2 of
 267         BoundTo ty2' -> uUnboundVar tv1 maybe_ty1 ty2' ty2'
 268
 269         -- Try to update sys-y type variables in preference to sig-y ones
 270         -- (the latter respond False to isSysLocalName)
 271         UnBound |  can_update_tv2
 272                 && (tv2_is_sys_y || not can_update_tv1)
 273                 -> tcWriteTyVar tv2 (TyVarTy tv1)       `thenNF_Tc_` returnTc ()
 274
 275                 |  can_update_tv1
 276                 -> tcWriteTyVar tv1 ps_ty2              `thenNF_Tc_` returnTc ()
 277
 278         other   -> failWithTc (unifyKindErr tv1 ps_ty2)
 279   where
 280     kind1 = tyVarKind tv1
 281     kind2 = tyVarKind tv2
 282
 283     can_update_tv1 = kind2 `hasMoreBoxityInfo` kind1
 284     can_update_tv2 = kind1 `hasMoreBoxityInfo` kind2
 285
 286         -- Try to overwrite sys-y things with sig-y things
 287     tv2_is_sys_y = isSysLocalName (varName tv2)
 288
 289
 290         -- Second one isn't a type variable
 291 uUnboundVar tv1 maybe_ty1 ps_ty2 non_var_ty2
 292   | non_var_ty2 == openTypeKind
 293   =     -- We never bind a kind variable to openTypeKind;
 294         -- instead we refine it to boxedTypeKind
 295         -- This is a rather dark corner, I have to admit.  SLPJ May 98
 296      tcWriteTyVar tv1 boxedTypeKind             `thenNF_Tc_`
 297      returnTc ()
 298
 299   |  tyvar_kind == superKind
 300   || typeKind non_var_ty2 `hasMoreBoxityInfo` tyvar_kind
 301         -- OK to bind if we're at the kind level, or
 302         -- (at the type level) the variable has less boxity info than the type
 303   =  occur_check non_var_ty2                    `thenTc_`
 304      tcWriteTyVar tv1 ps_ty2                    `thenNF_Tc_`
 305      returnTc ()
 306
 307   | otherwise
 308   = failWithTc (unifyKindErr tv1 ps_ty2)
 309
 310   where
 311     tyvar_kind = tyVarKind tv1
 312
 313     occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty))       `thenTc_`
 314                      returnTc ()
 315
 316     occur_check_tv tv2
 317        | tv1 == tv2             -- Same tyvar; fail
 318        = zonkTcType ps_ty2      `thenNF_Tc` \ zonked_ty2 ->
 319          failWithTcM (unifyOccurCheck tv1 zonked_ty2)
 320
 321        | otherwise              -- A different tyvar
 322        = tcReadTyVar tv2        `thenNF_Tc` \ maybe_ty2 ->
 323          case maybe_ty2 of
 324                 BoundTo ty2' -> occur_check ty2'
 325                 other        -> returnTc ()
 326 \end{code}
 327
 328 %************************************************************************
 329 %*                                                                      *
 330 \subsection[Unify-fun]{@unifyFunTy@}
 331 %*                                                                      *
 332 %************************************************************************
 333
 334 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
 335
 336 \begin{code}
 337 unifyFunTy :: TcType s                          -- Fail if ty isn't a function type
 338            -> TcM s (TcType s, TcType s)        -- otherwise return arg and result types
 339
 340 unifyFunTy ty@(TyVarTy tyvar)
 341   = tcReadTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 342     case maybe_ty of
 343         BoundTo ty' -> unifyFunTy ty'
 344         other       -> unify_fun_ty_help ty
 345
 346 unifyFunTy ty
 347   = case splitFunTy_maybe ty of
 348         Just arg_and_res -> returnTc arg_and_res
 349         Nothing          -> unify_fun_ty_help ty
 350
 351 unify_fun_ty_help ty    -- Special cases failed, so revert to ordinary unification
 352   = newTyVarTy openTypeKind             `thenNF_Tc` \ arg ->
 353     newTyVarTy openTypeKind             `thenNF_Tc` \ res ->
 354     unifyTauTy ty (mkFunTy arg res)     `thenTc_`
 355     returnTc (arg,res)
 356 \end{code}
 357
 358 \begin{code}
 359 unifyListTy :: TcType s              -- expected list type
 360             -> TcM s (TcType s)      -- list element type
 361
 362 unifyListTy ty@(TyVarTy tyvar)
 363   = tcReadTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 364     case maybe_ty of
 365         BoundTo ty' -> unifyListTy ty'
 366         other       -> unify_list_ty_help ty
 367
 368 unifyListTy ty
 369   = case splitTyConApp_maybe ty of
 370         Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
 371         other                                       -> unify_list_ty_help ty
 372
 373 unify_list_ty_help ty   -- Revert to ordinary unification
 374   = newTyVarTy boxedTypeKind            `thenNF_Tc` \ elt_ty ->
 375     unifyTauTy ty (mkListTy elt_ty)     `thenTc_`
 376     returnTc elt_ty
 377 \end{code}
 378
 379 \begin{code}
 380 unifyTupleTy :: Arity -> TcType s -> TcM s [TcType s]
 381 unifyTupleTy arity ty@(TyVarTy tyvar)
 382   = tcReadTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 383     case maybe_ty of
 384         BoundTo ty' -> unifyTupleTy arity ty'
 385         other       -> unify_tuple_ty_help arity ty
 386
 387 unifyTupleTy arity ty
 388   = case splitTyConApp_maybe ty of
 389         Just (tycon, arg_tys) |  isTupleTyCon tycon
 390                          && tyConArity tycon == arity
 391                          -> returnTc arg_tys
 392         other -> unify_tuple_ty_help arity ty
 393
 394 unify_tuple_ty_help arity ty
 395   = mapNF_Tc (\ _ -> newTyVarTy boxedTypeKind) [1..arity]       `thenNF_Tc` \ arg_tys ->
 396     unifyTauTy ty (mkTupleTy arity arg_tys)                     `thenTc_`
 397     returnTc arg_tys
 398 \end{code}
 399
 400 \begin{code}
 401 unifyUnboxedTupleTy :: Arity -> TcType s -> TcM s [TcType s]
 402 unifyUnboxedTupleTy arity ty@(TyVarTy tyvar)
 403   = tcReadTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 404     case maybe_ty of
 405         BoundTo ty' -> unifyUnboxedTupleTy arity ty'
 406         other       -> unify_unboxed_tuple_ty_help arity ty
 407
 408 unifyUnboxedTupleTy arity ty
 409   = case splitTyConApp_maybe ty of
 410         Just (tycon, arg_tys) |  isUnboxedTupleTyCon tycon
 411                          && tyConArity tycon == arity
 412                          -> returnTc arg_tys
 413         other -> unify_tuple_ty_help arity ty
 414
 415 unify_unboxed_tuple_ty_help arity ty
 416   = mapNF_Tc (\ _ -> newTyVarTy openTypeKind) [1..arity]`thenNF_Tc` \ arg_tys ->
 417     unifyTauTy ty (mkUnboxedTupleTy arity arg_tys)      `thenTc_`
 418     returnTc arg_tys
 419 \end{code}
 420
 421 %************************************************************************
 422 %*                                                                      *
 423 \subsection[Unify-context]{Errors and contexts}
 424 %*                                                                      *
 425 %************************************************************************
 426
 427 Errors
 428 ~~~~~~
 429
 430 \begin{code}
 431 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
 432   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 433     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 434     returnNF_Tc (err ty1' ty2')
 435   where
 436     err ty1 ty2 = (env1,
 437                    nest 4
 438                         (vcat [
 439                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
 440                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
 441                         ]))
 442                   where
 443                     (env1, [tidy_ty1,tidy_ty2]) = tidyTypes tidy_env [ty1,ty2]
 444
 445 unifyMisMatch ty1 ty2
 446   = (env2, hang (ptext SLIT("Couldn't match"))
 447               4 (sep [quotes (ppr tidy_ty1), ptext SLIT("against"), quotes (ppr tidy_ty2)]))
 448   where
 449     (env1, tidy_ty1) = tidyType emptyTidyEnv ty1
 450     (env2, tidy_ty2) = tidyType env1         ty2
 451
 452 unifyKindErr tyvar ty
 453   = hang (ptext SLIT("Kind mis-match between"))
 454          4 (sep [quotes (hsep [ppr tyvar, ptext SLIT("::"), ppr (tyVarKind tyvar)]),
 455                  ptext SLIT("and"),
 456                  quotes (hsep [ppr ty, ptext SLIT("::"), ppr (typeKind ty)])])
 457
 458 unifyOccurCheck tyvar ty
 459   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
 460               4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
 461   where
 462     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
 463     (env2, tidy_ty)    = tidyType  env1         ty
 464 \end{code}
 465