ghc/compiler/typecheck/Unify.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1995
   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 ) where
  13
  14 IMPORT_Trace            -- ToDo: rm (debugging only)
  15 import Outputable
  16 import Pretty
  17
  18 import AbsSyn
  19 import TcMonad
  20
  21 import CmdLineOpts      ( GlobalSwitch(..) )
  22 import Errors           ( unifyErr, UnifyErrInfo(..), UnifyErrContext  )
  23 import Id               ( Id, DataCon(..), Inst )
  24 import Maybes           ( Maybe(..) )
  25 import Subst            ( extendSubst, SubstResult(..), Subst )
  26 #if USE_ATTACK_PRAGMAS
  27 import Class            ( Class(..), cmpClass ) -- .. for pragmas only
  28 import TyCon            ( TyCon(..), isBoxedTyCon, isVisibleSynTyCon, cmpTyCon )
  29                         -- .. on TyCon is for pragmas only
  30 import TyVar            -- make all visible for pragmas
  31 import UniTyFuns        ( pprUniType, pprTyCon )
  32 #else
  33 import Class            ( Class )
  34 import TyVar            ( TyVar(..), TyVarTemplate )
  35 import TyCon            ( TyCon, isBoxedTyCon, isVisibleSynTyCon )
  36 #endif
  37 import UniType          ( UniType(..), TauType(..)
  38                           IF_ATTACK_PRAGMAS(COMMA cmpUniType)
  39                         )
  40 import Util
  41 \end{code}
  42
  43 %************************************************************************
  44 %*                                                                      *
  45 \subsection[Unify-spec]{Specification}
  46 %*                                                                      *
  47 %************************************************************************
  48
  49 CLAIM: the unifier works correctly even if the types to be unified are not
  50 fixed points of the substitution.
  51
  52 %************************************************************************
  53 %*                                                                      *
  54 \subsection[Unify-exported]{Exported unification functions}
  55 %*                                                                      *
  56 %************************************************************************
  57
  58 The exported functions are all defined as versions of some
  59 non-exported generic functions.
  60
  61 Unify two @TauType@s.  Dead straightforward.
  62
  63 \begin{code}
  64 unifyTauTy :: TauType -> TauType -> UnifyErrContext -> TcM ()
  65
  66 unifyTauTy ty1 ty2 err_ctxt = uTys ty1 ty1 ty2 ty2 err_ctxt
  67 \end{code}
  68
  69 @unifyTauTyLists@ unifies corresponding elements of its two list
  70 arguments.  The lists should be of equal length.
  71
  72 \begin{code}
  73 unifyTauTyLists :: [TauType] -> [TauType] -> UnifyErrContext -> TcM ()
  74
  75 unifyTauTyLists tys1 tys2 err_ctxt = uList tys1 tys2 err_ctxt
  76 \end{code}
  77
  78 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
  79 all together.  It is used, for example, when typechecking explicit
  80 lists, when all the elts should be of the same type.
  81
  82 \begin{code}
  83 unifyTauTyList :: [TauType] -> UnifyErrContext -> TcM ()
  84
  85 unifyTauTyList []   _ = returnTc ()
  86 unifyTauTyList [ty] _ = returnTc ()
  87
  88 unifyTauTyList (ty1:tys@(ty2:_)) err_ctxt
  89   = unifyTauTy ty1 ty2 err_ctxt `thenTc_`
  90     unifyTauTyList tys err_ctxt
  91 \end{code}
  92
  93 %************************************************************************
  94 %*                                                                      *
  95 \subsection[Unify-lists-of-types]{@uList@}
  96 %*                                                                      *
  97 %************************************************************************
  98
  99 @uList@ unifies corresponding elements of two lists of @TauType@s.  It
 100 uses @uTys@ to do the real work.  We charge down the list explicitly
 101 so that we can complain if their lengths differ.
 102
 103 \begin{code}
 104 uList :: [TauType] -> [TauType]
 105       -> UnifyErrContext
 106       -> TcM ()
 107
 108 uList [] [] _ = returnTc ()
 109
 110 uList (ty1:tys1) (ty2:tys2) err_ctxt
 111   = uTys ty1 ty1 ty2 ty2 err_ctxt   `thenTc_`
 112     uList tys1 tys2 err_ctxt
 113
 114 uList ty1s ty2s _ = panic "Unify.uList: mismatched type lists!"
 115 \end{code}
 116
 117 %************************************************************************
 118 %*                                                                      *
 119 \subsection[Unify-uTys]{@uTys@: getting down to business}
 120 %*                                                                      *
 121 %************************************************************************
 122
 123 @uTys@ is the heart of the unifier.  Each arg happens twice, because
 124 we want to report errors in terms of synomyms if poss.  The first of
 125 the pair is used in error messages only; it is always the same as the
 126 second, except that if the first is a synonym then the second may be a
 127 de-synonym'd version.  This way we get better error messages.
 128
 129 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 130
 131 \begin{code}
 132 uTys :: TauType -> TauType      -- Error reporting ty1 and real ty1
 133      -> TauType -> TauType      -- Error reporting ty2 and real ty2
 134      -> UnifyErrContext
 135      -> TcM ()
 136 \end{code}
 137
 138 %********************************************************
 139 %*                                                      *
 140 Sanity check: should never find a UniTyVarTemplate
 141 %*                                                      *
 142 %********************************************************
 143
 144 \begin{code}
 145 #ifdef DEBUG
 146
 147 uTys ps_ty1 ty1@(UniTyVarTemplate tv1) ps_ty2 ty2 err_ctxt
 148   = pprPanic "Unify:uTys:unifying w/ UniTyVarTemplate(1):" (ppCat [ppr PprDebug tv1, ppr PprDebug ty2])
 149
 150 uTys ps_ty1 ty1 ps_ty2 ty2@(UniTyVarTemplate tv2) err_ctxt
 151   = pprPanic "Unify:uTys:unifying w/ UniTyVarTemplate(2):" (ppCat [ppr PprDebug ty1, ppr PprDebug tv2])
 152
 153 #endif {-DEBUG-}
 154 \end{code}
 155
 156 %********************************************************
 157 %*                                                      *
 158 Both variables:
 159 %*                                                      *
 160 %********************************************************
 161
 162 \begin{code}
 163 uTys ps_ty1 (UniTyVar tyvar1) ps_ty2 ty2 err_ctxt = uVar tyvar1 ps_ty2 ty2 err_ctxt
 164 uTys ps_ty1 ty1 ps_ty2 (UniTyVar tyvar2) err_ctxt = uVar tyvar2 ps_ty1 ty1 err_ctxt
 165 \end{code}
 166
 167 %********************************************************
 168 %*                                                      *
 169 Both function constructors:
 170 %*                                                      *
 171 %********************************************************
 172
 173 \begin{code}
 174 uTys _ (UniFun fun1 arg1) _ (UniFun fun2 arg2) err_ctxt
 175   = uList [fun1, arg1] [fun2, arg2] err_ctxt
 176 \end{code}
 177
 178 %********************************************************
 179 %*                                                      *
 180 Both datatype constructors:
 181 %*                                                      *
 182 %********************************************************
 183
 184 \begin{code}
 185 uTys ps_ty1 ty1@(UniData con1 args1) ps_ty2 ty2@(UniData con2 args2) err_ctxt
 186   = if (con1 == con2) then
 187         -- Same constructors, just unify the arguments
 188         uList args1 args2 err_ctxt
 189     else
 190         -- Different constructors: disaster
 191         getSrcLocTc             `thenNF_Tc` \ src_loc ->
 192         failTc (unifyErr (UnifyMisMatch ps_ty1 ps_ty2) err_ctxt src_loc)
 193 \end{code}
 194
 195 %********************************************************
 196 %*                                                      *
 197 Type synonyms:
 198 %*                                                      *
 199 %********************************************************
 200
 201 If just one or the other is a synonym, just expand it.
 202
 203 \begin{code}
 204 uTys ps_ty1 (UniSyn con1 args1 ty1) ps_ty2 ty2 err_ctxt
 205  | isVisibleSynTyCon con1
 206  = uTys ps_ty1 ty1 ps_ty2 ty2 err_ctxt
 207
 208 uTys ps_ty1 ty1 ps_ty2 (UniSyn con2 args2 ty2) err_ctxt
 209  | isVisibleSynTyCon con2
 210  = uTys ps_ty1 ty1 ps_ty2 ty2 err_ctxt
 211 \end{code}
 212
 213 If you are tempted to make a short cut on synonyms, as in this
 214 pseudocode...
 215
 216 \begin{verbatim}
 217 uTys (UniSyn con1 args1 ty1) (UniSyn con2 args2 ty2)
 218   = if (con1 == con2) then
 219         -- Good news!  Same synonym constructors, so we can shortcut
 220         -- by unifying their arguments and ignoring their expansions.
 221         uList args1 args2
 222     else
 223         -- Never mind.  Just expand them and try again
 224         uTys ty1 ty2
 225 \end{verbatim}
 226
 227 then THINK AGAIN.  Here is the whole story, as detected and reported
 228 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
 229 \begin{quotation}
 230 Here's a test program that should detect the problem:
 231
 232 \begin{verbatim}
 233         type Bogus a = Int
 234         x = (1 :: Bogus Char) :: Bogus Bool
 235 \end{verbatim}
 236
 237 The problem with [the attempted shortcut code] is that
 238 \begin{verbatim}
 239         con1 == con2
 240 \end{verbatim}
 241 is not a sufficient condition to be able to use the shortcut!
 242 You also need to know that the type synonym actually USES all
 243 its arguments.  For example, consider the following type synonym
 244 which does not use all its arguments.
 245 \begin{verbatim}
 246         type Bogus a = Int
 247 \end{verbatim}
 248
 249 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
 250 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
 251 would fail, even though the expanded forms (both \tr{Int}) should
 252 match.
 253
 254 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 255 unnecessarily bind \tr{t} to \tr{Char}.
 256
 257 ... You could explicitly test for the problem synonyms and mark them
 258 somehow as needing expansion, perhaps also issuing a warning to the
 259 user.
 260 \end{quotation}
 261
 262 Still, if the synonym is abstract, we can only just go ahead and try!
 263
 264 \begin{code}
 265 uTys ps_ty1 (UniSyn con1 args1 ty1) ps_ty2 (UniSyn con2 args2 ty2) err_ctxt
 266   -- Both must be abstract (i.e., non "visible" -- not done yet)
 267   = if (con1 == con2) then
 268         -- Good news!  Same synonym constructors, so we can shortcut
 269         -- by unifying their arguments and ignoring their expansions.
 270         uList args1 args2 err_ctxt
 271     else
 272         -- Bad news; mis-matched type constructors
 273         getSrcLocTc             `thenNF_Tc` \ src_loc ->
 274         failTc (unifyErr (UnifyMisMatch ps_ty1 ps_ty2) err_ctxt src_loc)
 275 \end{code}
 276
 277 %********************************************************
 278 %*                                                      *
 279 Catch-all case---just fails:
 280 %*                                                      *
 281 %********************************************************
 282
 283 Anything else fails. For example, matching a @UniFun@ against
 284 a @UniData@.
 285 \begin{code}
 286 uTys ps_ty1 ty1 ps_ty2 ty2 err_ctxt
 287   = getSrcLocTc         `thenNF_Tc` \ src_loc ->
 288     failTc (unifyErr (UnifyMisMatch ps_ty1 ps_ty2) err_ctxt src_loc)
 289 \end{code}
 290
 291 %************************************************************************
 292 %*                                                                      *
 293 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 294 %*                                                                      *
 295 %************************************************************************
 296
 297 @uVar@ is called when at least one of the types being unified is a
 298 variable.  It does {\em not} assume that the variable is a fixed point
 299 of the substitution; rather, notice that @bindTo@ (defined below) nips
 300 back into @uTys@ if it turns out that the variable is already bound.
 301
 302 There is a slight worry that one might try to @bindTo@ a (say) Poly
 303 tyvar (as tv1) with an Open tyvar (as ty2) which is already unified to
 304 an unboxed type.  In fact this can't happen, because the Open ones are
 305 always the ones which are unified away.
 306
 307 \begin{code}
 308 uVar :: TyVar
 309      -> UniType -> UniType      -- printing and real versions
 310      -> UnifyErrContext
 311      -> TcM ()
 312
 313 uVar tv1 ps_ty2 ty2 err_ctxt
 314   = do tv1 ty2
 315   where
 316         -- Expand synonyms
 317     do _ (UniSyn _ _ ty2) = do tv1 ty2
 318
 319         -- Commit any open type variable
 320     do (OpenSysTyVar _) ty2                                 = tv1 `bindTo` ps_ty2
 321     do _                ty2@(UniTyVar tv2@(OpenSysTyVar _)) = tv2 `bindTo` ty1
 322
 323         -- Eliminate Poly in favour of User
 324     do (PolySysTyVar _) ty2@(UniTyVar (UserTyVar _ _))      = tv1 `bindTo` ps_ty2
 325     do (PolySysTyVar _) ty2@(UniTyVar (PolySysTyVar _))     = tv1 `bindTo` ps_ty2
 326     do (UserTyVar _ _)  ty2@(UniTyVar tv2@(PolySysTyVar _)) = tv2 `bindTo` ty1
 327     do (UserTyVar _ _)  ty2@(UniTyVar (UserTyVar _ _))      = tv1 `bindTo` ps_ty2
 328
 329         -- Matching for boxed data types
 330     do (PolySysTyVar _) ty2@(UniData con _) | isBoxedTyCon con  = tv1 `bindTo` ps_ty2
 331     do (UserTyVar _ _)  ty2@(UniData con _) | isBoxedTyCon con  = tv1 `bindTo` ps_ty2
 332
 333         -- Matching for unboxed data types:
 334         --   requires specialisation w.r.t. the unboxed type
 335     do (PolySysTyVar _) ty2@(UniData con _)  = tv1 `bindToUnboxed` ps_ty2
 336     do (UserTyVar _ _)  ty2@(UniData con _)  = tv1 `bindToUnboxed` ps_ty2
 337
 338         -- Matching for function types
 339     do (PolySysTyVar _) ty2@(UniFun _ _)     = tv1 `bindTo` ps_ty2
 340     do (UserTyVar _ _)  ty2@(UniFun _ _)     = tv1 `bindTo` ps_ty2
 341
 342         -- Default
 343     do _ _ = getSrcLocTc `thenNF_Tc` \ src_loc ->
 344              failTc (unifyErr (UnifyMisMatch ty1 ps_ty2) err_ctxt src_loc)
 345
 346         ----------- END OF CASES ---------------
 347
 348     ty1 = UniTyVar tv1
 349
 350     tyvar1 `bindTo` ty2
 351         = extendSubstTc tyvar1 ty2 err_ctxt
 352
 353     tyvar1 `bindToUnboxed` ty2
 354         = getSwitchCheckerTc    `thenNF_Tc` \ sw_chkr ->
 355           if sw_chkr SpecialiseUnboxed then
 356               extendSubstTc tyvar1 ty2 err_ctxt
 357           else
 358               getSrcLocTc       `thenNF_Tc` \ src_loc ->
 359               failTc (unifyErr (UnifyMisMatch ty1 ps_ty2) err_ctxt src_loc)
 360 \end{code}