projects
/
ghc-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Fix a long-standing infelicity in the type pretty printer
[ghc-hetmet.git]
/
compiler
/
types
/
Unify.lhs
diff --git
a/compiler/types/Unify.lhs
b/compiler/types/Unify.lhs
index
c1ef798
..
7195e5b
100644
(file)
--- a/
compiler/types/Unify.lhs
+++ b/
compiler/types/Unify.lhs
@@
-206,7
+206,7
@@
match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
-- Match the kind of the template tyvar with the kind of Type
-- Note [Matching kinds]
match_kind menv subst tv ty
-- Match the kind of the template tyvar with the kind of Type
-- Note [Matching kinds]
match_kind menv subst tv ty
- | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
+ | isCoVar tv = do { let (ty1,ty2) = coVarKind tv
(ty3,ty4) = coercionKind ty
; subst1 <- match menv subst ty1 ty3
; match menv subst1 ty2 ty4 }
(ty3,ty4) = coercionKind ty
; subst1 <- match menv subst ty1 ty3
; match menv subst1 ty2 ty4 }
@@
-384,7
+384,7
@@
dataConCannotMatch tys con
data Refinement = Reft InScopeSet InternalReft
type InternalReft = TyVarEnv (Coercion, Type)
data Refinement = Reft InScopeSet InternalReft
type InternalReft = TyVarEnv (Coercion, Type)
--- INVARIANT: a->(co,ty) then co :: (a:=:ty)
+-- INVARIANT: a->(co,ty) then co :: (a~ty)
-- Not necessarily idemopotent
instance Outputable Refinement where
-- Not necessarily idemopotent
instance Outputable Refinement where
@@
-401,7
+401,7
@@
isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
refineType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Apply the refinement to the type.
-- If (refineType r ty) = (co, ty')
refineType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Apply the refinement to the type.
-- If (refineType r ty) = (co, ty')
--- Then co :: ty:=:ty'
+-- Then co :: ty~ty'
-- Nothing => the refinement does nothing to this type
refineType (Reft in_scope env) ty
| not (isEmptyVarEnv env), -- Common case
-- Nothing => the refinement does nothing to this type
refineType (Reft in_scope env) ty
| not (isEmptyVarEnv env), -- Common case
@@
-427,7
+427,7
@@
refinePred (Reft in_scope env) pred
refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Like refineType, but returns the 'sym' coercion
-- If (refineResType r ty) = (co, ty')
refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Like refineType, but returns the 'sym' coercion
-- If (refineResType r ty) = (co, ty')
--- Then co :: ty':=:ty
+-- Then co :: ty'~ty
refineResType reft ty
= case refineType reft ty of
Just (co, ty1) -> Just (mkSymCoercion co, ty1)
refineResType reft ty
= case refineType reft ty of
Just (co, ty1) -> Just (mkSymCoercion co, ty1)
@@
-617,8
+617,8
@@
uVar :: TvSubstEnv -- An existing substitution to extend
-> UM TvSubstEnv
-- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
-> UM TvSubstEnv
-- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
--- if swap=False (tv1:=:ty)
--- if swap=True (ty:=:tv1)
+-- if swap=False (tv1~ty)
+-- if swap=True (ty~tv1)
uVar subst tv1 ty
= -- Check to see whether tv1 is refined by the substitution
uVar subst tv1 ty
= -- Check to see whether tv1 is refined by the substitution
@@
-640,7
+640,7
@@
uUnrefined subst tv1 ty2 ty2'
= uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms
-- This is essential, in case we have
-- type Foo a = a
= uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms
-- This is essential, in case we have
-- type Foo a = a
- -- and then unify a :=: Foo a
+ -- and then unify a ~ Foo a
uUnrefined subst tv1 ty2 (TyVarTy tv2)
| tv1 == tv2 -- Same type variable
uUnrefined subst tv1 ty2 (TyVarTy tv2)
| tv1 == tv2 -- Same type variable
@@
-656,15
+656,6
@@
uUnrefined subst tv1 ty2 (TyVarTy tv2)
; b2 <- tvBindFlag tv2
; case (b1,b2) of
(BindMe, _) -> bind tv1 ty2
; b2 <- tvBindFlag tv2
; case (b1,b2) of
(BindMe, _) -> bind tv1 ty2
-
- (AvoidMe, BindMe) -> bind tv2 ty1
- (AvoidMe, _) -> bind tv1 ty2
-
- (WildCard, WildCard) -> return subst
- (WildCard, Skolem) -> return subst
- (WildCard, _) -> bind tv2 ty1
-
- (Skolem, WildCard) -> return subst
(Skolem, Skolem) -> failWith (misMatch ty1 ty2)
(Skolem, _) -> bind tv2 ty1
}
(Skolem, Skolem) -> failWith (misMatch ty1 ty2)
(Skolem, _) -> bind tv2 ty1
}
@@
-704,29
+695,33
@@
bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
bindTv subst tv ty -- ty is not a type variable
= do { b <- tvBindFlag tv
; case b of
bindTv subst 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 ty
+ Skolem -> failWith (misMatch (TyVarTy tv) ty)
+ BindMe -> return $ extendVarEnv subst tv ty
}
\end{code}
%************************************************************************
%* *
}
\end{code}
%************************************************************************
%* *
- Unification monad
+ Binding decisions
%* *
%************************************************************************
\begin{code}
data BindFlag
= BindMe -- A regular type variable
%* *
%************************************************************************
\begin{code}
data BindFlag
= BindMe -- A regular type variable
- | AvoidMe -- Like BindMe but, given the choice, avoid binding it
| Skolem -- This type variable is a skolem constant
-- Don't bind it; it only matches itself
| Skolem -- This type variable is a skolem constant
-- Don't bind it; it only matches itself
+\end{code}
+
- | WildCard -- This type variable matches anything,
- -- and does not affect the substitution
+%************************************************************************
+%* *
+ Unification monad
+%* *
+%************************************************************************
+\begin{code}
newtype UM a = UM { unUM :: (TyVar -> BindFlag)
-> MaybeErr Message a }
newtype UM a = UM { unUM :: (TyVar -> BindFlag)
-> MaybeErr Message a }