import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion )
import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion,
- mkLeftCoercion, mkRightCoercion,
- splitCoercionKind, decomposeCo )
+ mkLeftCoercion, mkRightCoercion, mkCoKind, coercionKindPredTy,
+ splitCoercionKind, decomposeCo, coercionKind )
import TcType ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst,
substTyVar, zipTopTvSubst, typeKind,
eqKind, isSubKind, repSplitAppTy_maybe,
- tcView
+ tcView, tcGetTyVar_maybe
)
-import Type ( Type, tyVarsOfType, tyVarsOfTypes )
+import Type ( Type, tyVarsOfType, tyVarsOfTypes, tcEqType, mkTyVarTy )
import TypeRep ( Type(..), PredType(..) )
import DataCon ( DataCon, dataConUnivTyVars, dataConEqSpec )
-import Var ( CoVar, TyVar, tyVarKind )
+import Var ( CoVar, TyVar, tyVarKind, varUnique )
import VarEnv
import VarSet
import ErrUtils ( Message )
import Maybes ( MaybeErr(..), isJust )
import Control.Monad ( foldM )
import Outputable
+import Unique ( Unique )
+import UniqFM ( ufmToList )
#include "HsVersions.h"
\end{code}
emptyRefinement :: Refinement
emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
+
refineType :: Refinement -> Type -> (ExprCoFn, Type)
-- Apply the refinement to the type.
-- If (refineType r ty) = (co, ty')
-- That is, the kinds of the co_vars are a
-- fixed point of the incoming refinement
- = initUM (tryToBind tv_set) $
+ = ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars),
+ ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) )
+ initUM (tryToBind tv_set) $
do { -- Run the unifier, starting with an empty env
; env2 <- foldM do_one emptyInternalReft co_vars
-- non-idempotent substitution
; let tmp_env = env1 `plusVarEnv` env2
out_env = fixTvCoEnv in_scope' tmp_env
- ; return (Reft in_scope' out_env) }
+ ; WARN( not (null (badReftElts tmp_env)), ppr (badReftElts tmp_env) $$ ppr tmp_env )
+ WARN( not (null (badReftElts out_env)), ppr (badReftElts out_env) $$ ppr out_env )
+ return (Reft in_scope' out_env) }
where
tv_set = mkVarSet ex_tvs
in_scope' = foldr extend in_scope co_vars
where
fixpt = mapVarEnv step env
- step (co, ty) = (co', ty')
+ step (co, ty) = (co1, 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
- co' | ExprCoFn co'' <- co_fn = mkTransCoercion co co''
+ co1 | ExprCoFn co'' <- co_fn = mkTransCoercion co co''
| otherwise = ASSERT( isIdCoercion co_fn ) co
-----------------------------
tryToBind :: TyVarSet -> TyVar -> BindFlag
tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
| otherwise = AvoidMe
+
+
\end{code}
-- INVARIANT: a->(co,ty) then co :: (a:=:ty)
-- Not necessarily idemopotent
+badReftElts :: InternalReft -> [(Unique, (Coercion,Type))]
+-- Return the BAD elements of the refinement
+-- Should be empty; used in asserions only
+badReftElts env
+ = filter (not . ok) (ufmToList env)
+ where
+ ok :: (Unique, (Coercion, Type)) -> Bool
+ ok (u, (co, ty)) | Just tv <- tcGetTyVar_maybe ty1
+ = varUnique tv == u && ty `tcEqType` ty2
+ | otherwise = False
+ where
+ (ty1,ty2) = coercionKind co
+
emptyInternalReft :: InternalReft
emptyInternalReft = emptyVarEnv
-> 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 r co tv1 ty2 ty2'), we know that
+-- co :: tv1:=:ty2
uUnrefined subst co tv1 ty2 ty2'
| Just ty2'' <- tcView ty2'
= return subst
-- Check to see whether tv2 is refined
- | Just (co',ty') <- lookupVarEnv subst tv2
+ | Just (co',ty') <- lookupVarEnv subst tv2 -- co' :: tv2:=:ty'
= uUnrefined subst (mkTransCoercion co co') tv1 ty' ty'
-- So both are unrefined; next, see if the kinds force the direction
= do { b1 <- tvBindFlag tv1
; b2 <- tvBindFlag tv2
; case (b1,b2) of
- (BindMe, _) -> bind tv1 ty2
+ (BindMe, _) -> bind False tv1 ty2
- (AvoidMe, BindMe) -> bind tv2 ty1
- (AvoidMe, _) -> bind tv1 ty2
+ (AvoidMe, BindMe) -> bind True tv2 ty1
+ (AvoidMe, _) -> bind False tv1 ty2
(WildCard, WildCard) -> return subst
(WildCard, Skolem) -> return subst
- (WildCard, _) -> bind tv2 ty1
+ (WildCard, _) -> bind True tv2 ty1
(Skolem, WildCard) -> return subst
(Skolem, Skolem) -> failWith (misMatch ty1 ty2)
- (Skolem, _) -> bind tv2 ty1
+ (Skolem, _) -> bind True tv2 ty1
}
- | k1 `isSubKind` k2 = bindTv subst co tv2 ty1 -- Must update tv2
+ | k1 `isSubKind` k2 = bindTv subst (mkSymCoercion co) tv2 ty1 -- Must update tv2
| k2 `isSubKind` k1 = bindTv subst co tv1 ty2 -- Must update tv1
| otherwise = failWith (kindMisMatch tv1 ty2)
ty1 = TyVarTy tv1
k1 = tyVarKind tv1
k2 = tyVarKind tv2
- bind tv ty = return (extendVarEnv subst tv (co,ty))
+ bind swap tv ty =
+ ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty)
+ , (text "Refinement invariant failure: co = " <+> ppr co <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)))
+ return (extendVarEnv subst tv (co1,ty))
+ where
+ co1 = if swap then mkSymCoercion co else co
uUnrefined subst co tv1 ty2 ty2' -- ty2 is not a type variable
| tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
Just (_,ty) -> substTvSet subst (tyVarsOfType ty)
bindTv subst co tv ty -- ty is not a type variable
- = do { b <- tvBindFlag tv
+ = ASSERT2( (coercionKindPredTy co `tcEqType` mkCoKind (mkTyVarTy tv) ty),
+ (text "Refinement invariant failure: co = " <+> ppr co <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) )
+ do { b <- tvBindFlag tv
; case b of
Skolem -> failWith (misMatch (TyVarTy tv) ty)
WildCard -> return subst