ghc/compiler/typecheck/Unify.lhs

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