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