%************************************************************************
\begin{code}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
module TcGadt (
- Refinement, emptyRefinement, gadtRefine,
- refineType, refineResType,
- dataConCanMatch,
+ Refinement, emptyRefinement, isEmptyRefinement,
+ gadtRefine,
+ refineType, refinePred, refineResType,
tcUnifyTys, BindFlag(..)
) where
import HsSyn
import Coercion
+import Type
+
import TypeRep
-import DataCon
import Var
import VarEnv
import VarSet
import Maybes
import Control.Monad
import Outputable
-
-#ifdef DEBUG
+import TcType
import Unique
import UniqFM
-import TcType
-#endif
+import FastString
\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 :: Refinement
emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
+isEmptyRefinement :: Refinement -> Bool
+isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
refineType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Apply the refinement to the type.
tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
co_subst = mkTvSubst in_scope (mapVarEnv fst env)
+refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
+refinePred (Reft in_scope env) pred
+ | not (isEmptyVarEnv env), -- Common case
+ any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
+ = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
+ | otherwise
+ = 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)
+
refineResType :: Refinement -> Type -> (HsWrapper, Type)
-- Like refineType, but returns the 'sym' coercion
-- If (refineResType r ty) = (co, ty')
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
(ty1,ty2) = splitCoercionKind (tyVarKind co_var)
-\end{code}
+\end{code}
%************************************************************************
%* *
-- then use transitivity with the original coercion
-----------------------------
+-- XXX Can we do this more nicely, by exploiting laziness?
+-- Or avoid needing it in the first place?
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
-fixTvSubstEnv in_scope env
- = fixpt
- where
- fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env
-
-----------------------------
-dataConCanMatch :: DataCon -> [Type] -> Bool
--- Returns True iff the data con can match a scrutinee of type (T tys)
--- where T is the type constructor for the data con
---
--- Instantiate the equations and try to unify them
-dataConCanMatch con tys
- = isJust (tcUnifyTys (\tv -> BindMe)
- (map (substTyVar subst . fst) eq_spec)
- (map snd eq_spec))
+fixTvSubstEnv in_scope env = f env
where
- dc_tvs = dataConUnivTyVars con
- eq_spec = dataConEqSpec con
- subst = zipTopTvSubst dc_tvs tys
+ 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'
----------------------------
tryToBind :: TyVarSet -> TyVar -> BindFlag
tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
| otherwise = AvoidMe
-
\end{code}
%************************************************************************
\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