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