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