Commit 67ee8a93 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.
Browse files

Fix GADT refinement fix-pointing, add ASSERTs and a WARN, make type equality...

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 <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
parent a97f155c
......@@ -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
......
......@@ -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
......
......@@ -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,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment