%
% (c) The University of Glasgow 2006
%
\begin{code}
module Unify (
tcMatchTy, tcMatchTys, tcMatchTyX,
ruleMatchTyX, tcMatchPreds, MatchEnv(..),
dataConCannotMatch,
tcUnifyTys, BindFlag(..)
) where
#include "HsVersions.h"
import Var
import VarEnv
import VarSet
import Type
import Coercion
import TyCon
import DataCon
import TypeRep
import Outputable
import ErrUtils
import Util
import Maybes
import UniqFM
import FastString
\end{code}
%************************************************************************
%* *
Matching
%* *
%************************************************************************
Matching is much tricker than you might think.
1. The substitution we generate binds the *template type variables*
which are given to us explicitly.
2. We want to match in the presence of foralls;
e.g (forall a. t1) ~ (forall b. t2)
That is what the RnEnv2 is for; it does the alpharenaming
that makes it as if a and b were the same variable.
Initialising the RnEnv2, so that it can generate a fresh
binder when necessary, entails knowing the free variables of
both types.
3. We must be careful not to bind a template type variable to a
locally bound variable. E.g.
(forall a. x) ~ (forall b. b)
where x is the template type variable. Then we do not want to
bind x to a/b! This is a kind of occurs check.
The necessary locals accumulate in the RnEnv2.
\begin{code}
data MatchEnv
= ME { me_tmpls :: VarSet
, me_env :: RnEnv2
}
tcMatchTy :: TyVarSet
-> Type
-> Type
-> Maybe TvSubst
tcMatchTy tmpls ty1 ty2
= case match menv emptyTvSubstEnv ty1 ty2 of
Just subst_env -> Just (TvSubst in_scope subst_env)
Nothing -> Nothing
where
menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
tcMatchTys :: TyVarSet
-> [Type]
-> [Type]
-> Maybe TvSubst
tcMatchTys tmpls tys1 tys2
= case match_tys menv emptyTvSubstEnv tys1 tys2 of
Just subst_env -> Just (TvSubst in_scope subst_env)
Nothing -> Nothing
where
menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
tcMatchTyX :: TyVarSet
-> TvSubst
-> Type
-> Type
-> Maybe TvSubst
tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
= case match menv subst_env ty1 ty2 of
Just subst_env -> Just (TvSubst in_scope subst_env)
Nothing -> Nothing
where
menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
tcMatchPreds
:: [TyVar]
-> [PredType] -> [PredType]
-> Maybe TvSubstEnv
tcMatchPreds tmpls ps1 ps2
= match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
where
menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
ruleMatchTyX :: MatchEnv
-> TvSubstEnv
-> Type
-> Type
-> Maybe TvSubstEnv
ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2
\end{code}
Now the internals of matching
\begin{code}
match :: MatchEnv
-> TvSubstEnv
-> Type -> Type
-> Maybe TvSubstEnv
match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
| Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
match menv subst (TyVarTy tv1) ty2
| Just ty1' <- lookupVarEnv subst tv1'
= if tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
then Just subst
else Nothing
| tv1' `elemVarSet` me_tmpls menv
= if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
then Nothing
else do { subst1 <- match_kind menv subst tv1 ty2
; return (extendVarEnv subst1 tv1' ty2) }
| otherwise
= case ty2 of
TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
_ -> Nothing
where
rn_env = me_env menv
tv1' = rnOccL rn_env tv1
match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
= match menv' subst ty1 ty2
where
menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
match menv subst (PredTy p1) (PredTy p2)
= match_pred menv subst p1 p2
match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2 = match_tys menv subst tys1 tys2
match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
= do { subst' <- match menv subst ty1a ty2a
; match menv subst' ty1b ty2b }
match menv subst (AppTy ty1a ty1b) ty2
| Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
= do { subst' <- match menv subst ty1a ty2a
; match menv subst' ty1b ty2b }
match _ _ _ _
= Nothing
match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
match_kind menv subst tv ty
| isCoVar tv = do { let (ty1,ty2) = coVarKind tv
(ty3,ty4) = coercionKind ty
; subst1 <- match menv subst ty1 ty3
; match menv subst1 ty2 ty4 }
| otherwise = if typeKind ty `isSubKind` tyVarKind tv
then Just subst
else Nothing
match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
-> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
match_list _ subst [] [] = Just subst
match_list fn subst (ty1:tys1) (ty2:tys2) = do { subst' <- fn subst ty1 ty2
; match_list fn subst' tys1 tys2 }
match_list _ _ _ _ = Nothing
match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
| c1 == c2 = match_tys menv subst tys1 tys2
match_pred menv subst (IParam n1 t1) (IParam n2 t2)
| n1 == n2 = match menv subst t1 t2
match_pred _ _ _ _ = Nothing
\end{code}
%************************************************************************
%* *
GADTs
%* *
%************************************************************************
Note [Pruning dead case alternatives]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider data T a where
T1 :: T Int
T2 :: T a
newtype X = MkX Int
newtype Y = MkY Char
type family F a
type instance F Bool = Int
Now consider case x of { T1 -> e1; T2 -> e2 }
The question before the house is this: if I know something about the type
of x, can I prune away the T1 alternative?
Suppose x::T Char. It's impossible to construct a (T Char) using T1,
Answer = YES (clearly)
Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated
to 'Bool', in which case x::T Int, so
ANSWER = NO (clearly)
Suppose x::T X. Then *in Haskell* it's impossible to construct a (nonbottom)
value of type (T X) using T1. But *in FC* it's quite possible. The newtype
gives a coercion
CoX :: X ~ Int
So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a nonbottom value
of type (T X) constructed with T1. Hence
ANSWER = NO (surprisingly)
Furthermore, this can even happen; see Trac #1251. GHC's newtypederiving
mechanism uses a cast, just as above, to move from one dictionary to another,
in effect giving the programmer access to CoX.
Finally, suppose x::T Y. Then *even in FC* we can't construct a
nonbottom value of type (T Y) using T1. That's because we can get
from Y to Char, but not to Int.
Here's a related question. data Eq a b where EQ :: Eq a a
Consider
case x of { EQ -> ... }
Suppose x::Eq Int Char. Is the alternative dead? Clearly yes.
What about x::Eq Int a, in a context where we have evidence that a~Char.
Then again the alternative is dead.
Summary
We are really doing a test for unsatisfiability of the type
constraints implied by the match. And that is clearly, in general, a
hard thing to do.
However, since we are simply dropping dead code, a conservative test
suffices. There is a continuum of tests, ranging from easy to hard, that
drop more and more dead code.
For now we implement a very simple test: type variables match
anything, type functions (incl newtypes) match anything, and only
distinct data types fail to match. We can elaborate later.
\begin{code}
dataConCannotMatch :: [Type] -> DataCon -> Bool
dataConCannotMatch tys con
| null eq_spec = False
| all isTyVarTy tys = False
| otherwise
= cant_match_s (map (substTyVar subst . fst) eq_spec)
(map snd eq_spec)
where
dc_tvs = dataConUnivTyVars con
eq_spec = dataConEqSpec con
subst = zipTopTvSubst dc_tvs tys
cant_match_s :: [Type] -> [Type] -> Bool
cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
or (zipWith cant_match tys1 tys2)
cant_match :: Type -> Type -> Bool
cant_match t1 t2
| Just t1' <- coreView t1 = cant_match t1' t2
| Just t2' <- coreView t2 = cant_match t1 t2'
cant_match (FunTy a1 r1) (FunTy a2 r2)
= cant_match a1 a2 || cant_match r1 r2
cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| isDataTyCon tc1 && isDataTyCon tc2
= tc1 /= tc2 || cant_match_s tys1 tys2
cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
cant_match (AppTy f1 a1) ty2
| Just (f2, a2) <- repSplitAppTy_maybe ty2
= cant_match f1 f2 || cant_match a1 a2
cant_match ty1 (AppTy f2 a2)
| Just (f1, a1) <- repSplitAppTy_maybe ty1
= cant_match f1 f2 || cant_match a1 a2
cant_match _ _ = False
\end{code}
%************************************************************************
%* *
Unification
%* *
%************************************************************************
\begin{code}
tcUnifyTys :: (TyVar -> BindFlag)
-> [Type] -> [Type]
-> Maybe TvSubst
tcUnifyTys bind_fn tys1 tys2
= maybeErrToMaybe $ initUM bind_fn $
do { subst <- unifyList emptyTvSubstEnv tys1 tys2
; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
tv_env = fixTvSubstEnv in_scope subst
; return (mkTvSubst in_scope tv_env) }
where
tvs1 = tyVarsOfTypes tys1
tvs2 = tyVarsOfTypes tys2
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
fixTvSubstEnv in_scope env = f env
where
f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
then e
else f e'
\end{code}
%************************************************************************
%* *
The workhorse
%* *
%************************************************************************
\begin{code}
unify :: TvSubstEnv
-> Type -> Type
-> UM TvSubstEnv
unify subst (TyVarTy tv1) ty2 = uVar subst tv1 ty2
unify subst ty1 (TyVarTy tv2) = uVar subst tv2 ty1
unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
| tyc1 == tyc2 = unify_tys subst tys1 tys2
unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
= do { subst' <- unify subst ty1a ty2a
; unify subst' ty1b ty2b }
unify subst (AppTy ty1a ty1b) ty2
| Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
= do { subst' <- unify subst ty1a ty2a
; unify subst' ty1b ty2b }
unify subst ty1 (AppTy ty2a ty2b)
| Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
= do { subst' <- unify subst ty1a ty2a
; unify subst' ty1b ty2b }
unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
| c1 == c2 = unify_tys subst tys1 tys2
unify_pred subst (IParam n1 t1) (IParam n2 t2)
| n1 == n2 = unify subst t1 t2
unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
unify_tys subst xs ys = unifyList subst xs ys
unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
unifyList subst orig_xs orig_ys
= go subst orig_xs orig_ys
where
go subst [] [] = return subst
go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
; go subst' xs ys }
go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
uVar :: TvSubstEnv
-> TyVar
-> Type
-> UM TvSubstEnv
uVar subst tv1 ty
=
case (lookupVarEnv subst tv1) of
Just ty' -> unify subst ty' ty
Nothing -> uUnrefined subst
tv1 ty ty
uUnrefined :: TvSubstEnv
-> TyVar
-> Type
-> Type
-> UM TvSubstEnv
uUnrefined subst tv1 ty2 ty2'
| Just ty2'' <- tcView ty2'
= uUnrefined subst tv1 ty2 ty2''
uUnrefined subst tv1 ty2 (TyVarTy tv2)
| tv1 == tv2
= return subst
| Just ty' <- lookupVarEnv subst tv2
= uUnrefined subst tv1 ty' ty'
| eqKind k1 k2
= do { b1 <- tvBindFlag tv1
; b2 <- tvBindFlag tv2
; case (b1,b2) of
(BindMe, _) -> bind tv1 ty2
(Skolem, Skolem) -> failWith (misMatch ty1 ty2)
(Skolem, _) -> bind tv2 ty1
}
| k1 `isSubKind` k2 = bindTv subst tv2 ty1
| k2 `isSubKind` k1 = bindTv subst tv1 ty2
| otherwise = failWith (kindMisMatch tv1 ty2)
where
ty1 = TyVarTy tv1
k1 = tyVarKind tv1
k2 = tyVarKind tv2
bind tv ty = return $ extendVarEnv subst tv ty
uUnrefined subst tv1 ty2 ty2'
| tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
= failWith (occursCheck tv1 ty2)
| not (k2 `isSubKind` k1)
= failWith (kindMisMatch tv1 ty2)
| otherwise
= bindTv subst tv1 ty2
where
k1 = tyVarKind tv1
k2 = typeKind ty2'
substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
substTvSet subst tvs
= foldVarSet (unionVarSet . get) emptyVarSet tvs
where
get tv = case lookupVarEnv subst tv of
Nothing -> unitVarSet tv
Just ty -> substTvSet subst (tyVarsOfType ty)
bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
bindTv subst tv ty
= do { b <- tvBindFlag tv
; case b of
Skolem -> failWith (misMatch (TyVarTy tv) ty)
BindMe -> return $ extendVarEnv subst tv ty
}
\end{code}
%************************************************************************
%* *
Binding decisions
%* *
%************************************************************************
\begin{code}
data BindFlag
= BindMe
| Skolem
\end{code}
%************************************************************************
%* *
Unification monad
%* *
%************************************************************************
\begin{code}
newtype UM a = UM { unUM :: (TyVar -> BindFlag)
-> MaybeErr Message a }
instance Monad UM where
return a = UM (\_tvs -> Succeeded a)
fail s = UM (\_tvs -> Failed (text s))
m >>= k = UM (\tvs -> case unUM m tvs of
Failed err -> Failed err
Succeeded v -> unUM (k v) tvs)
initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
initUM badtvs um = unUM um badtvs
tvBindFlag :: TyVar -> UM BindFlag
tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
failWith :: Message -> UM a
failWith msg = UM (\_tv_fn -> Failed msg)
maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
maybeErrToMaybe (Succeeded a) = Just a
maybeErrToMaybe (Failed _) = Nothing
\end{code}
%************************************************************************
%* *
Error reporting
We go to a lot more trouble to tidy the types
in TcUnify. Maybe we'll end up having to do that
here too, but I'll leave it for now.
%* *
%************************************************************************
\begin{code}
misMatch :: Type -> Type -> SDoc
misMatch t1 t2
= ptext (sLit "Can't match types") <+> quotes (ppr t1) <+>
ptext (sLit "and") <+> quotes (ppr t2)
lengthMisMatch :: [Type] -> [Type] -> SDoc
lengthMisMatch tys1 tys2
= sep [ptext (sLit "Can't match unequal length lists"),
nest 2 (ppr tys1), nest 2 (ppr tys2) ]
kindMisMatch :: TyVar -> Type -> SDoc
kindMisMatch tv1 t2
= vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
ptext (sLit "when matching") <+> quotes (ppr tv1) <+>
ptext (sLit "with") <+> quotes (ppr t2)]
occursCheck :: TyVar -> Type -> SDoc
occursCheck tv ty
= hang (ptext (sLit "Can't construct the infinite type"))
2 (ppr tv <+> equals <+> ppr ty)
\end{code}