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