%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
tcUnifyTys, BindFlag(..)
) where
-import HsSyn ( HsWrapper(..), idHsWrapper, isIdHsWrapper )
-import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion,
- mkLeftCoercion, mkRightCoercion, mkCoKind, coercionKindPredTy,
- splitCoercionKind, decomposeCo, coercionKind )
-import TcType ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst,
- substTyVar, zipTopTvSubst, typeKind,
- eqKind, isSubKind, repSplitAppTy_maybe,
- tcView, tcGetTyVar_maybe
- )
-import Type ( Type, tyVarsOfType, tyVarsOfTypes, tcEqType, mkTyVarTy )
-import TypeRep ( Type(..), PredType(..) )
-import DataCon ( DataCon, dataConUnivTyVars, dataConEqSpec )
-import Var ( CoVar, TyVar, tyVarKind, varUnique )
+#include "HsVersions.h"
+
+import HsSyn
+import Coercion
+import TypeRep
+import DataCon
+import Var
import VarEnv
import VarSet
-import ErrUtils ( Message )
-import Maybes ( MaybeErr(..), isJust )
-import Control.Monad ( foldM )
+import ErrUtils
+import Maybes
+import Control.Monad
import Outputable
-import Unique ( Unique )
-import UniqFM ( ufmToList )
+import TcType
-#include "HsVersions.h"
+#ifdef DEBUG
+import Unique
+import UniqFM
+#endif
\end{code}
\begin{code}
data Refinement = Reft InScopeSet InternalReft
+
+type InternalReft = TyVarEnv (Coercion, Type)
-- INVARIANT: a->(co,ty) then co :: (a:=:ty)
-- Not necessarily idemopotent
emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
-refineType :: Refinement -> Type -> (HsWrapper, Type)
+refineType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Apply the refinement to the type.
-- If (refineType r ty) = (co, ty')
-- Then co :: ty:=:ty'
+-- Nothing => the refinement does nothing to this type
refineType (Reft in_scope env) ty
| not (isEmptyVarEnv env), -- Common case
any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
- = (WpCo (substTy co_subst ty), substTy tv_subst ty)
+ = Just (substTy co_subst ty, substTy tv_subst ty)
| otherwise
- = (idHsWrapper, ty) -- The type doesn't mention any refined type variables
+ = Nothing -- The type doesn't mention any refined type variables
where
tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
co_subst = mkTvSubst in_scope (mapVarEnv fst env)
-- Like refineType, but returns the 'sym' coercion
-- If (refineResType r ty) = (co, ty')
-- Then co :: ty':=:ty
+-- It's convenient to return a HsWrapper here
refineResType reft ty
= case refineType reft ty of
- (WpCo co, ty1) -> (WpCo (mkSymCoercion co), ty1)
- (id_co, ty1) -> ASSERT( isIdHsWrapper id_co )
- (idHsWrapper, ty1)
+ Just (co, ty1) -> (WpCo (mkSymCoercion co), ty1)
+ Nothing -> (idHsWrapper, ty)
\end{code}
ex_tvs co_vars
-- Precondition: fvs( co_vars ) # env1
-- That is, the kinds of the co_vars are a
--- fixed point of the incoming refinement
+-- fixed point of the incoming refinement
= ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars),
ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) )
where
tv_set = mkVarSet ex_tvs
in_scope' = foldr extend in_scope co_vars
+
+ -- For each co_var, add it *and* the tyvars it mentions, to in_scope
extend co_var in_scope
- = extendInScopeSetSet (extendInScopeSet in_scope co_var)
- (tyVarsOfType (tyVarKind co_var))
+ = extendInScopeSetSet in_scope $
+ extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
where
where
fixpt = mapVarEnv step env
- step (co, ty) = (co1, ty')
+ step (co, ty) = case refineType (Reft in_scope fixpt) ty of
+ Nothing -> (co, ty)
+ Just (co', ty') -> (mkTransCoercion co co', ty')
-- Apply fixpt one step:
-- Use refineType to get a substituted type, ty', and a coercion, co_fn,
-- which justifies the substitution. If the coercion is not the identity
-- then use transitivity with the original coercion
- where
- (co_fn, ty') = refineType (Reft in_scope fixpt) ty
- co1 | WpCo co'' <- co_fn = mkTransCoercion co co''
- | otherwise = ASSERT( isIdHsWrapper co_fn ) co
-----------------------------
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
%************************************************************************
\begin{code}
-type InternalReft = TyVarEnv (Coercion, Type)
-
--- INVARIANT: a->(co,ty) then co :: (a:=:ty)
--- Not necessarily idemopotent
-
+#ifdef DEBUG
badReftElts :: InternalReft -> [(Unique, (Coercion,Type))]
-- Return the BAD elements of the refinement
-- Should be empty; used in asserions only
| otherwise = False
where
(ty1,ty2) = coercionKind co
+#endif
emptyInternalReft :: InternalReft
emptyInternalReft = emptyVarEnv
occursCheck tv ty
= hang (ptext SLIT("Can't construct the infinite type"))
2 (ppr tv <+> equals <+> ppr ty)
-\end{code}
\ No newline at end of file
+\end{code}