Mon Sep 18 17:07:38 EDT 2006 Manuel M T Chakravarty <chak@cse.unsw.edu.au>
* Fix GADT refinement fix-pointing, add ASSERTs and a WARN, make type equality functions work for PredTy Eqtype ...
Sun Aug 6 20:28:50 EDT 2006 Manuel M T Chakravarty <chak@cse.unsw.edu.au>
* Fix GADT refinement fix-pointing, add ASSERTs and a WARN, make type equality functions work for PredTy Eqtype ...
Tue Aug 1 06:14:43 EDT 2006 kevind@bu.edu
import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion )
import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion,
import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion )
import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion,
- mkLeftCoercion, mkRightCoercion,
+ mkLeftCoercion, mkRightCoercion, mkCoKind, coercionKindPredTy,
splitCoercionKind, decomposeCo )
import TcType ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst,
substTyVar, zipTopTvSubst, typeKind,
eqKind, isSubKind, repSplitAppTy_maybe,
tcView
)
splitCoercionKind, decomposeCo )
import TcType ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst,
substTyVar, zipTopTvSubst, typeKind,
eqKind, isSubKind, repSplitAppTy_maybe,
tcView
)
-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 TypeRep ( Type(..), PredType(..) )
import DataCon ( DataCon, dataConUnivTyVars, dataConEqSpec )
import Var ( CoVar, TyVar, tyVarKind )
where
fixpt = mapVarEnv step env
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
-- 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
+ -- This trans looks backwards, but it
+ -- works somehow
| otherwise = ASSERT( isIdCoercion co_fn ) co
-----------------------------
| otherwise = ASSERT( isIdCoercion co_fn ) co
-----------------------------
tryToBind :: TyVarSet -> TyVar -> BindFlag
tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
| otherwise = AvoidMe
tryToBind :: TyVarSet -> TyVar -> BindFlag
tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
| otherwise = AvoidMe
ty1 = TyVarTy tv1
k1 = tyVarKind tv1
k2 = tyVarKind tv2
ty1 = TyVarTy tv1
k1 = tyVarKind tv1
k2 = tyVarKind tv2
- bind swap 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))
- co' = if swap then mkSymCoercion co else co
+ 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')
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
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
; case b of
Skolem -> failWith (misMatch (TyVarTy tv) ty)
WildCard -> return subst
import TypeRep
import Type ( Type, Kind, PredType, substTyWith, mkAppTy, mkForAllTy,
mkFunTy, splitAppTy_maybe, splitForAllTy_maybe, coreView,
import TypeRep
import Type ( Type, Kind, PredType, substTyWith, mkAppTy, mkForAllTy,
mkFunTy, splitAppTy_maybe, splitForAllTy_maybe, coreView,
- kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys
+ kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys,
+ coreEqType
)
import TyCon ( TyCon, tyConArity, mkCoercionTyCon, isNewTyCon,
newTyConRhs, newTyConCo,
)
import TyCon ( TyCon, tyConArity, mkCoercionTyCon, isNewTyCon,
newTyConRhs, newTyConCo,
transCoercionTyCon =
mkCoercionTyCon transCoercionTyConName 2 (mkKindingFun composeCoercionKindsOf)
where
transCoercionTyCon =
mkCoercionTyCon transCoercionTyConName 2 (mkKindingFun composeCoercionKindsOf)
where
- composeCoercionKindsOf (co1:co2:rest) = (a1, r2, rest)
+ composeCoercionKindsOf (co1:co2:rest) =
+ WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")
+ (a1, r2, rest)
where
(a1, r1) = coercionKind co1
(a2, r2) = coercionKind co2
where
(a1, r1) = coercionKind co1
(a2, r2) = coercionKind co2
cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
cmpPredX env (IParam _ _) (ClassP _ _) = LT
cmpPredX env (ClassP _ _) (IParam _ _) = GT
cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
cmpPredX env (IParam _ _) (ClassP _ _) = LT
cmpPredX env (ClassP _ _) (IParam _ _) = GT
+cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
\end{code}
PredTypes are used as a FM key in TcSimplify,
\end{code}
PredTypes are used as a FM key in TcSimplify,