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, splitAppTys, 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 ty1 (SynTy _ ty2) k subst = uTysX ty1 ty2 k subst
 384
 385         -- Variables; go for uVar
 386 uTysX (TyVarTy tyvar1) ty2 k subst = uVarX tyvar1 ty2 k subst
 387 uTysX ty1 (TyVarTy tyvar2) k subst = uVarX tyvar2 ty1 k subst
 388
 389         -- Functions; just check the two parts
 390 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
 391   = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
 392
 393         -- Type constructors must match
 394 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
 395   | (con1 == con2 && length tys1 == length tys2)
 396   = uTyListsX tys1 tys2 k subst
 397
 398         -- Applications need a bit of care!
 399         -- They can match FunTy and TyConApp
 400 uTysX (AppTy s1 t1) (AppTy s2 t2) k subst
 401   = uTysX s1 s2 (uTysX t1 t2 k) subst
 402
 403 uTysX (AppTy s1 t1) (FunTy fun2 arg2) k subst
 404   = uTysX s1 s2 (uTysX t1 t2 k) subst
 405   where
 406          -- Converts  a -> b to (->) a b
 407     s2 = TyConApp mkFunTyCon [fun2]
 408     t2 = arg2
 409
 410 uTysX (AppTy s1 t1) (TyConApp tc tys@(_:_)) k subst
 411   = case snocView tys of
 412         (ts2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
 413                   where
 414                         -- Not efficient, but simple
 415                      s2 = TyConApp tc ts2
 416
 417 uTysX s1 s2@(AppTy _ _) k subst = uTysX s2 s1 k subst
 418         -- Swap arguments if the App is in the second argument
 419
 420         -- Not expecting for-alls in unification
 421 #ifdef DEBUG
 422 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
 423 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
 424 #endif
 425
 426         -- Anything else fails
 427 uTysX ty1 ty2 k subst = Nothing
 428
 429
 430 uTyListsX []         []         k subst = k subst
 431 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
 432 uTyListsX tys1       tys2       k subst = Nothing   -- Fail if the lists are different lengths
 433 \end{code}
 434
 435 \begin{code}
 436 uVarX tv1 (TyVarTy tv2) k subst | tv1 == tv2 = k subst
 437       -- Binding a variable to itself is a no-op
 438
 439 uVarX tv1 ty2 k subst
 440   = case lookupTyVarEnv subst tv1 of
 441       Just ty1 ->    -- Already bound
 442                      uTysX ty1 ty2 k subst
 443
 444       Nothing        -- Not already bound
 445                |  typeKind ty2 `hasMoreBoxityInfo` tyVarKind tv1
 446                && occur_check_ok ty2
 447                ->     -- No kind mismatch nor occur check
 448                   k (addToTyVarEnv subst tv1 ty2)
 449
 450                | otherwise -> Nothing   -- Fail if kind mis-match or occur check
 451   where
 452     occur_check_ok ty = all occur_check_ok_tv (tyVarSetToList (tyVarsOfType ty))
 453     occur_check_ok_tv tv | tv1 == tv = False
 454                          | otherwise = case lookupTyVarEnv subst tv of
 455                                          Nothing -> True
 456                                          Just ty -> occur_check_ok ty
 457 \end{code}
 458
 459
 460 %************************************************************************
 461 %*                                                                      *
 462 \subsection[Unify-context]{Errors and contexts}
 463 %*                                                                      *
 464 %************************************************************************
 465
 466 Errors
 467 ~~~~~~
 468
 469 \begin{code}
 470 unifyCtxt ty1 ty2               -- ty1 expected, ty2 inferred
 471   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 472     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 473     returnNF_Tc (err ty1' ty2')
 474   where
 475     err ty1' ty2' = vcat [
 476                            hsep [ptext SLIT("Expected:"), ppr ty1'],
 477                            hsep [ptext SLIT("Inferred:"), ppr ty2']
 478                         ]
 479
 480 unifyMisMatch ty1 ty2
 481   = hang (ptext SLIT("Couldn't match the type"))
 482          4 (sep [quotes (ppr ty1), ptext SLIT("against"), quotes (ppr ty2)])
 483
 484 expectedFunErr ty
 485   = hang (text "Function type expected, but found the type")
 486          4 (ppr ty)
 487
 488 unifyKindErr tyvar ty
 489   = hang (ptext SLIT("Compiler bug: kind mis-match between"))
 490          4 (sep [quotes (hsep [ppr tyvar, ptext SLIT("::"), ppr (tyVarKind tyvar)]),
 491                  ptext SLIT("and"),
 492                  quotes (hsep [ppr ty, ptext SLIT("::"), ppr (typeKind ty)])])
 493
 494 unifyOccurCheck tyvar ty
 495   = hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
 496          8 (sep [ppr tyvar, char '=', ppr ty])
 497 \end{code}
 498