From 67ee8a93fc96a38c3f73468cb86d8421a11d2911 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Wed, 20 Sep 2006 17:58:30 +0000 Subject: [PATCH] Fix GADT refinement fix-pointing, add ASSERTs and a WARN, make type equality functions work for PredTy Eqtype ... Mon Sep 18 17:07:38 EDT 2006 Manuel M T Chakravarty * 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 * 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 --- compiler/typecheck/TcGadt.lhs | 23 ++++++++++++++++------- compiler/types/Coercion.lhs | 7 +++++-- compiler/types/Type.lhs | 1 + 3 files changed, 22 insertions(+), 9 deletions(-) diff --git a/compiler/typecheck/TcGadt.lhs b/compiler/typecheck/TcGadt.lhs index deac1eb..6c63593 100644 --- a/compiler/typecheck/TcGadt.lhs +++ b/compiler/typecheck/TcGadt.lhs @@ -18,14 +18,14 @@ module TcGadt ( 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 ) -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 ) @@ -201,14 +201,16 @@ fixTvCoEnv in_scope 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 - 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 ----------------------------- @@ -237,6 +239,8 @@ dataConCanMatch con tys tryToBind :: TyVarSet -> TyVar -> BindFlag tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe | otherwise = AvoidMe + + \end{code} @@ -409,9 +413,12 @@ uUnrefined subst co tv1 ty2 (TyVarTy 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)) where - 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') @@ -435,7 +442,9 @@ substTvSet subst tvs 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 diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 54061ed..c9de505 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -36,7 +36,8 @@ module Coercion ( 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, @@ -309,7 +310,9 @@ symCoercionTyCon = 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 diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index 5799147..2aa31eb 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -1029,6 +1029,7 @@ cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTy 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, -- 1.7.10.4