From: Manuel M T Chakravarty Date: Wed, 20 Sep 2006 18:00:37 +0000 (+0000) Subject: Refactoring in TcGadt X-Git-Tag: After_FC_branch_merge~61 X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;h=b97e1705d4bfd96d6a274d1fe593fff46edd23f6;p=ghc-hetmet.git Refactoring in TcGadt Mon Sep 18 17:11:25 EDT 2006 Manuel M T Chakravarty * Refactoring in TcGadt Sun Aug 6 20:32:20 EDT 2006 Manuel M T Chakravarty * Refactoring in TcGadt Tue Aug 1 10:28:25 EDT 2006 kevind@bu.edu --- diff --git a/compiler/typecheck/TcGadt.lhs b/compiler/typecheck/TcGadt.lhs index 75d5c54..558f97e 100644 --- a/compiler/typecheck/TcGadt.lhs +++ b/compiler/typecheck/TcGadt.lhs @@ -374,11 +374,12 @@ uVar swap subst co tv1 ty -> 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 @@ -386,65 +387,60 @@ uUnrefined :: InternalReft -- An existing substitution to extend -> UM InternalReft -- We know that tv1 isn't refined --- PRE-CONDITION: in the call (uUnrefined r co tv1 ty2 ty2'), we know that --- co :: tv1:=:ty2 +-- PRE-CONDITION: in the call (uUnrefined r co tv ty ty'), we know that +-- co :: tv:=:ty -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 -- co' :: tv2:=:ty' - = uUnrefined subst (mkTransCoercion co co') tv1 ty' 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 False tv1 ty2 + (BindMe, _) -> bind swap tv1 ty2 - (AvoidMe, BindMe) -> bind True tv2 ty1 - (AvoidMe, _) -> bind False tv1 ty2 + (AvoidMe, BindMe) -> bind (not swap) tv2 ty1 + (AvoidMe, _) -> bind swap tv1 ty2 (WildCard, WildCard) -> return subst (WildCard, Skolem) -> return subst - (WildCard, _) -> bind True tv2 ty1 + (WildCard, _) -> bind (not swap) tv2 ty1 (Skolem, WildCard) -> return subst (Skolem, Skolem) -> failWith (misMatch ty1 ty2) - (Skolem, _) -> bind True tv2 ty1 + (Skolem, _) -> bind (not swap) tv2 ty1 } - | k1 `isSubKind` k2 = bindTv subst (mkSymCoercion 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 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 + 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' @@ -459,15 +455,30 @@ substTvSet subst tvs Nothing -> unitVarSet tv Just (_,ty) -> substTvSet subst (tyVarsOfType ty) -bindTv subst co tv ty -- ty is not a type variable - = 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 +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} %************************************************************************