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