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