ghc/compiler/types/Unify.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section{Unify}
   5
   6 This module contains a unifier and a matcher, both of which
   7 use an explicit substitution
   8
   9 \begin{code}
  10 module Unify ( unifyTysX, unifyTyListsX,
  11                match, matchTy, matchTys
  12   ) where
  13
  14 #include "HsVersions.h"
  15
  16 import TypeRep  ( Type(..) )     -- friend
  17 import Type     ( typeKind, tyVarsOfType, splitAppTy_maybe,
  18                   splitUTy, isUTy, deNoteType
  19                 )
  20
  21 import PprType  ()      -- Instances
  22                         -- This import isn't strictly necessary, but it makes sure that
  23                         -- PprType is below Unify in the hierarchy, which in turn makes
  24                         -- fewer modules boot-import PprType
  25
  26 import Var      ( tyVarKind )
  27 import VarSet
  28 import VarEnv   ( TyVarSubstEnv, emptySubstEnv, lookupSubstEnv, extendSubstEnv,
  29                   SubstResult(..)
  30                 )
  31
  32 import Outputable
  33 \end{code}
  34
  35 %************************************************************************
  36 %*                                                                      *
  37 \subsection{Unification with an explicit substitution}
  38 %*                                                                      *
  39 %************************************************************************
  40
  41 Unify types with an explicit substitution and no monad.
  42 Ignore usage annotations.
  43
  44 \begin{code}
  45 type MySubst
  46    = (TyVarSet,         -- Set of template tyvars
  47       TyVarSubstEnv)    -- Not necessarily idempotent
  48
  49 unifyTysX :: TyVarSet           -- Template tyvars
  50           -> Type
  51           -> Type
  52           -> Maybe TyVarSubstEnv
  53 unifyTysX tmpl_tyvars ty1 ty2
  54   = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
  55
  56 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
  57               -> Maybe TyVarSubstEnv
  58 unifyTyListsX tmpl_tyvars tys1 tys2
  59   = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
  60
  61
  62 uTysX :: Type
  63       -> Type
  64       -> (MySubst -> Maybe result)
  65       -> MySubst
  66       -> Maybe result
  67
  68 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
  69 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
  70
  71         -- Variables; go for uVar
  72 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
  73   | tyvar1 == tyvar2
  74   = k subst
  75 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
  76   | tyvar1 `elemVarSet` tmpls
  77   = uVarX tyvar1 ty2 k subst
  78 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
  79   | tyvar2 `elemVarSet` tmpls
  80   = uVarX tyvar2 ty1 k subst
  81
  82         -- Functions; just check the two parts
  83 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
  84   = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
  85
  86         -- Type constructors must match
  87 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
  88   | (con1 == con2 && length tys1 == length tys2)
  89   = uTyListsX tys1 tys2 k subst
  90
  91         -- Applications need a bit of care!
  92         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
  93         -- NB: we've already dealt with type variables and Notes,
  94         -- so if one type is an App the other one jolly well better be too
  95 uTysX (AppTy s1 t1) ty2 k subst
  96   = case splitAppTy_maybe ty2 of
  97       Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
  98       Nothing       -> Nothing    -- Fail
  99
 100 uTysX ty1 (AppTy s2 t2) k subst
 101   = case splitAppTy_maybe ty1 of
 102       Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
 103       Nothing       -> Nothing    -- Fail
 104
 105         -- Not expecting for-alls in unification
 106 #ifdef DEBUG
 107 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
 108 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
 109 #endif
 110
 111         -- Ignore usages
 112 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
 113 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
 114
 115         -- Anything else fails
 116 uTysX ty1 ty2 k subst = Nothing
 117
 118
 119 uTyListsX []         []         k subst = k subst
 120 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
 121 uTyListsX tys1       tys2       k subst = Nothing   -- Fail if the lists are different lengths
 122 \end{code}
 123
 124 \begin{code}
 125 -- Invariant: tv1 is a unifiable variable
 126 uVarX tv1 ty2 k subst@(tmpls, env)
 127   = case lookupSubstEnv env tv1 of
 128       Just (DoneTy ty1) ->    -- Already bound
 129                      uTysX ty1 ty2 k subst
 130
 131       Nothing        -- Not already bound
 132                |  typeKind ty2 == tyVarKind tv1
 133                && occur_check_ok ty2
 134                ->     -- No kind mismatch nor occur check
 135                   UASSERT( not (isUTy ty2) )
 136                   k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
 137
 138                | otherwise -> Nothing   -- Fail if kind mis-match or occur check
 139   where
 140     occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
 141     occur_check_ok_tv tv | tv1 == tv = False
 142                          | otherwise = case lookupSubstEnv env tv of
 143                                          Nothing           -> True
 144                                          Just (DoneTy ty)  -> occur_check_ok ty
 145 \end{code}
 146
 147
 148
 149 %************************************************************************
 150 %*                                                                      *
 151 \subsection{Matching on types}
 152 %*                                                                      *
 153 %************************************************************************
 154
 155 Matching is a {\em unidirectional} process, matching a type against a
 156 template (which is just a type with type variables in it).  The
 157 matcher assumes that there are no repeated type variables in the
 158 template, so that it simply returns a mapping of type variables to
 159 types.  It also fails on nested foralls.
 160
 161 @matchTys@ matches corresponding elements of a list of templates and
 162 types.  It and @matchTy@ both ignore usage annotations, unlike the
 163 main function @match@.
 164
 165 \begin{code}
 166 matchTy :: TyVarSet                     -- Template tyvars
 167         -> Type                         -- Template
 168         -> Type                         -- Proposed instance of template
 169         -> Maybe TyVarSubstEnv          -- Matching substitution
 170
 171
 172 matchTys :: TyVarSet                    -- Template tyvars
 173          -> [Type]                      -- Templates
 174          -> [Type]                      -- Proposed instance of template
 175          -> Maybe (TyVarSubstEnv,               -- Matching substitution
 176                    [Type])              -- Left over instance types
 177
 178 matchTy tmpls ty1 ty2 = match False ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
 179
 180 matchTys tmpls tys1 tys2 = match_list False tys1 tys2 tmpls
 181                                       (\ (senv,tys) -> Just (senv,tys))
 182                                       emptySubstEnv
 183 \end{code}
 184
 185 @match@ is the main function.  It takes a flag indicating whether
 186 usage annotations are to be respected.
 187
 188 \begin{code}
 189 match :: Bool                                   -- Respect usages?
 190       -> Type -> Type                           -- Current match pair
 191       -> TyVarSet                               -- Template vars
 192       -> (TyVarSubstEnv -> Maybe result)        -- Continuation
 193       -> TyVarSubstEnv                          -- Current subst
 194       -> Maybe result
 195
 196 -- When matching against a type variable, see if the variable
 197 -- has already been bound.  If so, check that what it's bound to
 198 -- is the same as ty; if not, bind it and carry on.
 199
 200 match uflag (TyVarTy v) ty tmpls k senv
 201   | v `elemVarSet` tmpls
 202   =     -- v is a template variable
 203     case lookupSubstEnv senv v of
 204         Nothing -> UASSERT( not (isUTy ty) )
 205                    k (extendSubstEnv senv v (DoneTy ty))
 206         Just (DoneTy ty')  | ty' == ty         -> k senv   -- Succeeds
 207                            | otherwise         -> Nothing  -- Fails
 208
 209   | otherwise
 210   =     -- v is not a template variable; ty had better match
 211         -- Can't use (==) because types differ
 212     case deNoteType ty of
 213         TyVarTy v' | v == v' -> k senv    -- Success
 214         other                -> Nothing   -- Failure
 215     -- This deNoteType is *required* and cost me much pain.  I guess
 216     -- the reason the Note-stripping case is *last* rather than first
 217     -- is to preserve type synonyms etc., so I'm not moving it to the
 218     -- top; but this means that (without the deNotetype) a type
 219     -- variable may not match the pattern (TyVarTy v') as one would
 220     -- expect, due to an intervening Note.  KSW 2000-06.
 221
 222 match uflag (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
 223   = match uflag arg1 arg2 tmpls (match uflag res1 res2 tmpls k) senv
 224
 225 match uflag (AppTy fun1 arg1) ty2 tmpls k senv
 226   = case splitAppTy_maybe ty2 of
 227         Just (fun2,arg2) -> match uflag fun1 fun2 tmpls (match uflag arg1 arg2 tmpls k) senv
 228         Nothing          -> Nothing     -- Fail
 229
 230 match uflag (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
 231   | tc1 == tc2
 232   = match_list uflag tys1 tys2 tmpls k' senv
 233   where
 234     k' (senv', tys2') | null tys2' = k senv'    -- Succeed
 235                       | otherwise  = Nothing    -- Fail
 236
 237 match False (UsageTy _ ty1) ty2 tmpls k senv = match False ty1 ty2 tmpls k senv
 238 match False ty1 (UsageTy _ ty2) tmpls k senv = match False ty1 ty2 tmpls k senv
 239
 240 match True (UsageTy u1 ty1) (UsageTy u2 ty2) tmpls k senv
 241   = match True u1 u2 tmpls (match True ty1 ty2 tmpls k) senv
 242 match True ty1@(UsageTy _ _) ty2 tmpls k senv
 243   = case splitUTy ty2 of { (u,ty2') -> match True ty1 ty2' tmpls k senv }
 244 match True ty1 ty2@(UsageTy _ _) tmpls k senv
 245   = case splitUTy ty1 of { (u,ty1') -> match True ty1' ty2 tmpls k senv }
 246
 247         -- With type synonyms, we have to be careful for the exact
 248         -- same reasons as in the unifier.  Please see the
 249         -- considerable commentary there before changing anything
 250         -- here! (WDP 95/05)
 251 match uflag (NoteTy _ ty1) ty2      tmpls k senv = match uflag ty1 ty2 tmpls k senv
 252 match uflag ty1      (NoteTy _ ty2) tmpls k senv = match uflag ty1 ty2 tmpls k senv
 253
 254 -- Catch-all fails
 255 match _ _ _ _ _ _ = Nothing
 256
 257 match_list uflag []         tys2       tmpls k senv = k (senv, tys2)
 258 match_list uflag (ty1:tys1) []         tmpls k senv = Nothing   -- Not enough arg tys => failure
 259 match_list uflag (ty1:tys1) (ty2:tys2) tmpls k senv
 260   = match uflag ty1 ty2 tmpls (match_list uflag tys1 tys2 tmpls k) senv
 261 \end{code}
 262
 263