projects
/
ghc-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Implement TH reification of instances (Trac #1835)
[ghc-hetmet.git]
/
compiler
/
types
/
Unify.lhs
diff --git
a/compiler/types/Unify.lhs
b/compiler/types/Unify.lhs
index
3e35ac6
..
a9586b6
100644
(file)
--- a/
compiler/types/Unify.lhs
+++ b/
compiler/types/Unify.lhs
@@
-16,7
+16,7
@@
module Unify (
Refinement, emptyRefinement, isEmptyRefinement,
matchRefine, refineType, refinePred, refineResType,
Refinement, emptyRefinement, isEmptyRefinement,
matchRefine, refineType, refinePred, refineResType,
- -- side-effect free unification
+ -- Side-effect free unification
tcUnifyTys, BindFlag(..)
) where
tcUnifyTys, BindFlag(..)
) where
@@
-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