-
-%************************************************************************
-%* *
-\subsection{Matching on types}
-%* *
-%************************************************************************
-
-Matching is a {\em unidirectional} process, matching a type against a
-template (which is just a type with type variables in it). The
-matcher assumes that there are no repeated type variables in the
-template, so that it simply returns a mapping of type variables to
-types. It also fails on nested foralls.
-
-@matchTys@ matches corresponding elements of a list of templates and
-types. It and @matchTy@ both ignore usage annotations, unlike the
-main function @match@.
-
-\begin{code}
-matchTy :: TyVarSet -- Template tyvars
- -> Type -- Template
- -> Type -- Proposed instance of template
- -> Maybe TyVarSubstEnv -- Matching substitution
-
-
-matchTys :: TyVarSet -- Template tyvars
- -> [Type] -- Templates
- -> [Type] -- Proposed instance of template
- -> Maybe (TyVarSubstEnv, -- Matching substitution
- [Type]) -- Left over instance types
-
-matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
-
-matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
- (\ (senv,tys) -> Just (senv,tys))
- emptySubstEnv
-\end{code}
-
-@match@ is the main function. It takes a flag indicating whether
-usage annotations are to be respected.
-
-\begin{code}
-match :: Type -> Type -- Current match pair
- -> TyVarSet -- Template vars
- -> (TyVarSubstEnv -> Maybe result) -- Continuation
- -> TyVarSubstEnv -- Current subst
- -> Maybe result
-
--- When matching against a type variable, see if the variable
--- has already been bound. If so, check that what it's bound to
--- is the same as ty; if not, bind it and carry on.
-
-match (TyVarTy v) ty tmpls k senv
- | v `elemVarSet` tmpls
- = -- v is a template variable
- case lookupSubstEnv senv v of
- Nothing | typeKind ty `eqKind` tyVarKind v
- -- We do a kind check, just as in the uVarX above
- -- The kind check is needed to avoid bogus matches
- -- of (a b) with (c d), where the kinds don't match
- -- An occur check isn't needed when matching.
- -> k (extendSubstEnv senv v (DoneTy ty))
-
- | otherwise -> Nothing -- Fails
-
- Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
- | otherwise -> Nothing -- Fails
-
- | otherwise
- = -- v is not a template variable; ty had better match
- -- Can't use (==) because types differ
- case tcGetTyVar_maybe ty of
- Just v' | v == v' -> k senv -- Success
- other -> Nothing -- Failure
- -- This tcGetTyVar_maybe is *required* because it must strip Notes.
- -- I guess the reason the Note-stripping case is *last* rather than first
- -- is to preserve type synonyms etc., so I'm not moving it to the
- -- top; but this means that (without the deNotetype) a type
- -- variable may not match the pattern (TyVarTy v') as one would
- -- expect, due to an intervening Note. KSW 2000-06.
-
- -- Predicates
-match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
- | n1 == n2 = match t1 t2 tmpls k senv
-match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
- | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
-match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
- | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
-
- -- Functions; just check the two parts
-match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
- = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
-
-match (AppTy fun1 arg1) ty2 tmpls k senv
- = case tcSplitAppTy_maybe ty2 of
- Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
- Nothing -> Nothing -- Fail
-
-match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
- | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
-
--- Newtypes are opaque; other source types should not happen
-match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
- | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
-
- -- With type synonyms, we have to be careful for the exact
- -- same reasons as in the unifier. Please see the
- -- considerable commentary there before changing anything
- -- here! (WDP 95/05)
-match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
-match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
-
--- Catch-all fails
-match _ _ _ _ _ = Nothing
-
-match_list_exactly tys1 tys2 tmpls k senv
- = match_list tys1 tys2 tmpls k' senv
- where
- k' (senv', tys2') | null tys2' = k senv' -- Succeed
- | otherwise = Nothing -- Fail
-
-match_list [] tys2 tmpls k senv = k (senv, tys2)
-match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
-match_list (ty1:tys1) (ty2:tys2) tmpls k senv
- = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv
-\end{code}