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