%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\begin{code}
module TcGadt (
- Refinement, emptyRefinement, gadtRefine,
- refineType, refineResType,
- dataConCanMatch,
+ Refinement, emptyRefinement, isEmptyRefinement,
+ matchRefine,
+ refineType, refinePred, refineResType,
tcUnifyTys, BindFlag(..)
) where
-import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion )
-import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion,
- mkLeftCoercion, mkRightCoercion,
- splitCoercionKind, decomposeCo )
-import TcType ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst,
- substTyVar, zipTopTvSubst, typeKind,
- eqKind, isSubKind, repSplitAppTy_maybe,
- tcView
- )
-import Type ( Type, tyVarsOfType, tyVarsOfTypes )
-import TypeRep ( Type(..), PredType(..) )
-import DataCon ( DataCon, dataConUnivTyVars, dataConEqSpec )
-import Var ( CoVar, TyVar, tyVarKind )
+#include "HsVersions.h"
+
+import HsSyn
+import Coercion
+import Type
+
+import TypeRep
+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
-
-#include "HsVersions.h"
+import TcType
+import UniqFM
+import FastString
\end{code}
%************************************************************************
\begin{code}
-data Refinement = Reft InScopeSet TvSubstEnv CoSubstEnv
-type CoSubstEnv = TvSubstEnv -- Maps type variables to *coercions*
--- INVARIANT: in the refinement (tsub, csub)
--- forall a. (csub(a) :: a:=:tsub(a))
+data Refinement = Reft InScopeSet InternalReft
+
+type InternalReft = TyVarEnv (Coercion, Type)
+-- INVARIANT: a->(co,ty) then co :: (a:=:ty)
+-- Not necessarily idemopotent
instance Outputable Refinement where
- ppr (Reft in_scope tv_env co_env)
- = ptext SLIT("Refinment") <+>
- braces (ppr tv_env $$ ppr co_env)
+ ppr (Reft _in_scope env)
+ = ptext SLIT("Refinement") <+>
+ braces (ppr env)
emptyRefinement :: Refinement
-emptyRefinement = Reft emptyInScopeSet emptyVarEnv emptyVarEnv
+emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
-refineType :: Refinement -> Type -> (ExprCoFn, Type)
+isEmptyRefinement :: Refinement -> Bool
+isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
+
+refineType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Apply the refinement to the type.
-- If (refineType r ty) = (co, ty')
-- Then co :: ty:=:ty'
-refineType (Reft in_scope tv_env co_env) ty
- | not (isEmptyVarEnv tv_env), -- Common case
- any (`elemVarEnv` tv_env) (varSetElems (tyVarsOfType ty))
- = (ExprCoFn (substTy co_subst ty), substTy tv_subst 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))
+ = Just (substTy co_subst ty, substTy tv_subst ty)
| otherwise
- = (idCoercion, 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 tv_env
- co_subst = mkTvSubst in_scope co_env
+ tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
+ co_subst = mkTvSubst in_scope (mapVarEnv fst env)
-refineResType :: Refinement -> Type -> (ExprCoFn, Type)
+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')
-- Then co :: ty':=:ty
+-- It's convenient to return a HsWrapper here
refineResType reft ty
= case refineType reft ty of
- (ExprCoFn co, ty1) -> (ExprCoFn (mkSymCoercion co), ty1)
- (id_co, ty1) -> ASSERT( isIdCoercion id_co )
- (idCoercion, ty1)
+ Just (co, ty1) -> (WpCo (mkSymCoercion co), ty1)
+ Nothing -> (idHsWrapper, ty)
\end{code}
%************************************************************************
%* *
- Generating a type refinement
+ Simple generation of a type refinement
%* *
%************************************************************************
\begin{code}
-gadtRefine :: Refinement
- -> [TyVar] -- Bind these by preference
- -> [CoVar]
- -> MaybeErr Message Refinement
+matchRefine :: [CoVar] -> Refinement
\end{code}
-(gadtRefine cvs) takes a list of coercion variables, and returns a
-list of coercions, obtained by unifying the types equated by the
-incoming coercions. The returned coercions all have kinds of form
-(a:=:ty), where a is a rigid type variable.
-
-Example:
- gadtRefine [c :: (a,Int):=:(Bool,b)]
- = [ right (left c) :: a:=:Bool,
- sym (right c) :: b:=:Int ]
-
-That is, given evidence 'c' that (a,Int)=(Bool,b), it returns derived
-evidence in easy-to-use form. In particular, given any e::ty, we know
-that:
- e `cast` ty[right (left c)/a, sym (right c)/b]
- :: ty [Bool/a, Int/b]
-
-Two refinements:
-
-- It can fail, if the coercion is unsatisfiable.
-
-- It's biased, by being given a set of type variables to bind
- when there is a choice. Example:
- MkT :: forall a. a -> T [a]
- f :: forall b. T [b] -> b
- f x = let v = case x of { MkT y -> y }
- in ...
- Here we want to bind [a->b], not the other way round, because
- in this example the return type is wobbly, and we want the
- program to typecheck
-
-
--- E.g. (a, Bool, right (left c))
--- INVARIANT: in the triple (tv, ty, co), we have (co :: tv:=:ty)
--- The result is idempotent: the
+Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
+is a specialisation of ty1, produce a type refinement that maps the variables
+of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
+
+ matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
+ = { right (left (right co)) :: a ~ c
+ , right (right co) :: b ~ Maybe d
+ }
+
+Precondition: The rhs types must indeed be a specialisation of the lhs types;
+ i.e., some free variables of the lhs are replaced with either distinct free
+ variables or proper type terms to obtain the rhs. (We don't perform full
+ unification or type matching here!)
+
+NB: matchRefine does *not* expand the type synonyms.
\begin{code}
-gadtRefine (Reft in_scope tv_env1 co_env1)
- ex_tvs co_vars
--- Precondition: fvs( co_vars ) # tv_env1
--- That is, the kinds of the co_vars are a
--- fixed point of the incoming refinement
-
- = initUM (tryToBind tv_set) $
- do { -- Run the unifier, starting with an empty env
- ; env2 <- foldM do_one emptyInternalReft co_vars
-
- -- Find the fixed point of the resulting
- -- non-idempotent substitution
- ; let tv_env2 = tv_env1 `plusVarEnv` mapVarEnv snd env2
- co_env2 = co_env1 `plusVarEnv` mapVarEnv fst env2
-
- ; return (Reft in_scope' (fixTvSubstEnv in_scope' tv_env2)
- (fixTvSubstEnv in_scope' co_env2)) }
+matchRefine co_vars
+ = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
where
- tv_set = mkVarSet ex_tvs
- in_scope' = foldr extend in_scope co_vars
+ in_scope = foldr extend emptyInScopeSet 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))
-
- do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
- where
- (ty1,ty2) = splitCoercionKind (tyVarKind co_var)
-\end{code}
+ = extendInScopeSetSet in_scope $
+ extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
+
+ refineOne co_var = refine (TyVarTy co_var) ty1 ty2
+ where
+ (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
+
+ refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty)
+ refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys'
+ refine co (NoteTy _ ty) ty' = refine co ty ty'
+ refine co ty (NoteTy _ ty') = refine co ty ty'
+ refine _ (PredTy _) (PredTy _) =
+ error "TcGadt.matchRefine: PredTy"
+ refine co (FunTy arg res) (FunTy arg' res') =
+ refine (mkRightCoercion (mkLeftCoercion co)) arg arg'
+ `plusVarEnv`
+ refine (mkRightCoercion co) res res'
+ refine co (AppTy fun arg) (AppTy fun' arg') =
+ refine (mkLeftCoercion co) fun fun'
+ `plusVarEnv`
+ refine (mkRightCoercion co) arg arg'
+ refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
+ refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
+ refine _ _ _ = error "RcGadt.matchRefine: mismatch"
+
+ refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
+ refineArgs co tys tys' =
+ fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
+ where
+ refineArg (ty, ty') (reft, coWrapper)
+ = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
+ mkLeftCoercion . coWrapper)
+\end{code}
+
%************************************************************************
%* *
----------------------------
+-- XXX Can we do this more nicely, by exploiting laziness?
+-- Or avoid needing it in the first place?
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
- -- Find the fixed point of a TvSubstEnv
- -- (assuming it has no loops!)
-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
-
emptyInternalReft :: InternalReft
emptyInternalReft = emptyVarEnv
-> unify subst (mkTransCoercion (mkSymCoercion co') co) ty' ty
-- No, continue
- Nothing -> uUnrefined subst (if swap then mkSymCoercion co else co)
+ Nothing -> uUnrefined swap subst co
tv1 ty ty
-uUnrefined :: InternalReft -- An existing substitution to extend
+uUnrefined :: Bool -- Whether the input is swapped
+ -> InternalReft -- An existing substitution to extend
-> Coercion
-> TyVar -- Type variable to be unified
-> Type -- with this type
-> UM InternalReft
-- We know that tv1 isn't refined
--- PRE-CONDITION: in the call (uUnrefined r co tv ty ty'), we know that
--- co :: tv:=:ty
+-- PRE-CONDITION: in the call (uUnrefined False r co tv1 ty2 ty2'), we know that
+-- co :: tv1:=:ty2
+-- and if the first argument is True instead, we know
+-- co :: ty2:=:tv1
-uUnrefined subst co tv1 ty2 ty2'
+uUnrefined swap subst co tv1 ty2 ty2'
| Just ty2'' <- tcView ty2'
- = uUnrefined subst co tv1 ty2 ty2'' -- Unwrap synonyms
+ = uUnrefined swap subst co tv1 ty2 ty2'' -- Unwrap synonyms
-- This is essential, in case we have
-- type Foo a = a
-- and then unify a :=: Foo a
-uUnrefined subst co tv1 ty2 (TyVarTy tv2)
+uUnrefined swap subst co tv1 ty2 (TyVarTy tv2)
| tv1 == tv2 -- Same type variable
= return subst
-- Check to see whether tv2 is refined
- | Just (co',ty') <- lookupVarEnv subst tv2
- = uUnrefined subst (mkTransCoercion co co') tv1 ty' ty'
+ | Just (co',ty') <- lookupVarEnv subst tv2 -- co' :: tv2:=:ty'
+ = uUnrefined False subst (mkTransCoercion (doSwap swap co) co') tv1 ty' ty'
-- So both are unrefined; next, see if the kinds force the direction
| eqKind k1 k2 -- Can update either; so check the bind-flags
= do { b1 <- tvBindFlag tv1
; b2 <- tvBindFlag tv2
; case (b1,b2) of
- (BindMe, _) -> bind tv1 ty2
+ (BindMe, _) -> bind swap tv1 ty2
- (AvoidMe, BindMe) -> bind tv2 ty1
- (AvoidMe, _) -> bind tv1 ty2
+ (AvoidMe, BindMe) -> bind (not swap) tv2 ty1
+ (AvoidMe, _) -> bind swap tv1 ty2
(WildCard, WildCard) -> return subst
(WildCard, Skolem) -> return subst
- (WildCard, _) -> bind tv2 ty1
+ (WildCard, _) -> bind (not swap) tv2 ty1
(Skolem, WildCard) -> return subst
(Skolem, Skolem) -> failWith (misMatch ty1 ty2)
- (Skolem, _) -> bind tv2 ty1
+ (Skolem, _) -> bind (not swap) tv2 ty1
}
- | k1 `isSubKind` k2 = bindTv subst co tv2 ty1 -- Must update tv2
- | k2 `isSubKind` k1 = bindTv subst co tv1 ty2 -- Must update tv1
+ | k1 `isSubKind` k2 = bindTv (not swap) subst co tv2 ty1 -- Must update tv2
+ | k2 `isSubKind` k1 = bindTv swap subst co tv1 ty2 -- Must update tv1
| otherwise = failWith (kindMisMatch tv1 ty2)
where
ty1 = TyVarTy tv1
k1 = tyVarKind tv1
k2 = tyVarKind tv2
- bind tv ty = return (extendVarEnv subst tv (co,ty))
+ bind swap tv ty = extendReft swap subst tv co ty
-uUnrefined subst co tv1 ty2 ty2' -- ty2 is not a type variable
+uUnrefined swap subst co tv1 ty2 ty2' -- ty2 is not a type variable
| tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
= failWith (occursCheck tv1 ty2) -- Occurs check
| not (k2 `isSubKind` k1)
= failWith (kindMisMatch tv1 ty2) -- Kind check
| otherwise
- = bindTv subst co tv1 ty2 -- Bind tyvar to the synonym if poss
+ = bindTv swap subst co tv1 ty2 -- Bind tyvar to the synonym if poss
where
k1 = tyVarKind tv1
k2 = typeKind ty2'
Nothing -> unitVarSet tv
Just (_,ty) -> substTvSet subst (tyVarsOfType ty)
-bindTv subst co tv ty -- ty is not a type variable
- = do { b <- tvBindFlag tv
+bindTv swap subst co tv ty -- ty is not a type variable
+ = do { b <- tvBindFlag tv
; case b of
Skolem -> failWith (misMatch (TyVarTy tv) ty)
WildCard -> return subst
- other -> return (extendVarEnv subst tv (co,ty))
+ other -> extendReft swap subst tv co ty
}
+
+doSwap :: Bool -> Coercion -> Coercion
+doSwap swap co = if swap then mkSymCoercion co else co
+
+extendReft :: Bool
+ -> InternalReft
+ -> TyVar
+ -> Coercion
+ -> Type
+ -> UM InternalReft
+extendReft swap subst tv co ty
+ = ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty),
+ (text "Refinement invariant failure: co = " <+> ppr co1 <+> ppr (coercionKindPredTy co1) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) )
+ return (extendVarEnv subst tv (co1, ty))
+ where
+ co1 = doSwap swap co
+
\end{code}
%************************************************************************
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}