dataConCannotMatch,
- -- GADT type refinement
- Refinement, emptyRefinement, isEmptyRefinement,
- matchRefine, refineType, refinePred, refineResType,
-
- -- side-effect free unification
+ -- Side-effect free unification
tcUnifyTys, BindFlag(..)
) where
-- 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 }
\end{code}
-%************************************************************************
-%* *
- What a refinement is
-%* *
-%************************************************************************
-
-\begin{code}
-data Refinement = Reft InScopeSet InternalReft
-
-type InternalReft = TyVarEnv (Coercion, Type)
--- INVARIANT: a->(co,ty) then co :: (a:=:ty)
--- Not necessarily idemopotent
-
-instance Outputable Refinement where
- ppr (Reft _in_scope env)
- = ptext SLIT("Refinement") <+>
- braces (ppr env)
-
-emptyRefinement :: Refinement
-emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
-
-isEmptyRefinement :: Refinement -> Bool
-isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
-
-refineType :: Refinement -> Type -> Maybe (Coercion, Type)
--- Apply the refinement to the type.
--- If (refineType r ty) = (co, ty')
--- Then co :: ty:=:ty'
--- Nothing => the refinement does nothing to this type
-refineType (Reft in_scope env) ty
- | not (isEmptyVarEnv env), -- Common case
- any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
- = Just (substTy co_subst ty, substTy tv_subst ty)
- | otherwise
- = Nothing -- The type doesn't mention any refined type variables
- where
- tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
- co_subst = mkTvSubst in_scope (mapVarEnv fst env)
-
-refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
-refinePred (Reft in_scope env) pred
- | not (isEmptyVarEnv env), -- Common case
- any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
- = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
- | otherwise
- = Nothing -- The type doesn't mention any refined type variables
- where
- tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
- co_subst = mkTvSubst in_scope (mapVarEnv fst env)
-
-refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
--- Like refineType, but returns the 'sym' coercion
--- If (refineResType r ty) = (co, ty')
--- Then co :: ty':=:ty
-refineResType reft ty
- = case refineType reft ty of
- Just (co, ty1) -> Just (mkSymCoercion co, ty1)
- Nothing -> Nothing
-\end{code}
-
-
-%************************************************************************
-%* *
- Simple generation of a type refinement
-%* *
-%************************************************************************
-
-\begin{code}
-matchRefine :: [CoVar] -> Refinement
-\end{code}
-
-Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
-is a specialisation of ty1, produce a type refinement that maps the variables
-of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
-
- matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
- = { right (left (right co)) :: a ~ c
- , right (right co) :: b ~ Maybe d
- }
-
-Precondition: The rhs types must indeed be a specialisation of the lhs types;
- i.e., some free variables of the lhs are replaced with either distinct free
- variables or proper type terms to obtain the rhs. (We don't perform full
- unification or type matching here!)
-
-NB: matchRefine does *not* expand the type synonyms.
-
-\begin{code}
-matchRefine co_vars
- = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
- where
- in_scope = foldr extend emptyInScopeSet co_vars
-
- -- For each co_var, add it *and* the tyvars it mentions, to in_scope
- extend co_var in_scope
- = extendInScopeSetSet in_scope $
- extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
-
- refineOne co_var = refine (TyVarTy co_var) ty1 ty2
- where
- (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
-
- refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty)
- refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys'
- refine _ (PredTy _) (PredTy _) =
- error "Unify.matchRefine: PredTy"
- refine co (FunTy arg res) (FunTy arg' res') =
- refine (mkRightCoercion (mkLeftCoercion co)) arg arg'
- `plusVarEnv`
- refine (mkRightCoercion co) res res'
- refine co (AppTy fun arg) (AppTy fun' arg') =
- refine (mkLeftCoercion co) fun fun'
- `plusVarEnv`
- refine (mkRightCoercion co) arg arg'
- refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
- refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
- refine _ _ _ = error "RcGadt.matchRefine: mismatch"
-
- refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
- refineArgs co tys tys' =
- fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
- where
- refineArg (ty, ty') (reft, coWrapper)
- = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
- mkLeftCoercion . coWrapper)
-\end{code}
-
%************************************************************************
%* *
\begin{code}
tcUnifyTys :: (TyVar -> BindFlag)
-> [Type] -> [Type]
- -> Maybe TvSubst -- A regular one-shot substitution
+ -> Maybe TvSubst -- A regular one-shot (idempotent) substitution
-- The two types may have common type variables, and indeed do so in the
-- second call to tcUnifyTys in FunDeps.checkClsFD
--
-> 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
= 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
; 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
}
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}
%************************************************************************
%* *
- Unification monad
+ Binding decisions
%* *
%************************************************************************
\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
+\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 }
\begin{code}
misMatch :: Type -> Type -> SDoc
misMatch t1 t2
- = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+>
- ptext SLIT("and") <+> quotes (ppr t2)
+ = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+>
+ ptext (sLit "and") <+> quotes (ppr t2)
lengthMisMatch :: [Type] -> [Type] -> SDoc
lengthMisMatch tys1 tys2
- = sep [ptext SLIT("Can't match unequal length lists"),
+ = sep [ptext (sLit "Can't match unequal length lists"),
nest 2 (ppr tys1), nest 2 (ppr tys2) ]
kindMisMatch :: TyVar -> Type -> SDoc
kindMisMatch tv1 t2
- = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
- ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
- ptext SLIT("when matching") <+> quotes (ppr tv1) <+>
- ptext SLIT("with") <+> quotes (ppr t2)]
+ = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
+ ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
+ ptext (sLit "when matching") <+> quotes (ppr tv1) <+>
+ ptext (sLit "with") <+> quotes (ppr t2)]
occursCheck :: TyVar -> Type -> SDoc
occursCheck tv ty
- = hang (ptext SLIT("Can't construct the infinite type"))
+ = hang (ptext (sLit "Can't construct the infinite type"))
2 (ppr tv <+> equals <+> ppr ty)
\end{code}
projects / ghc-hetmet.git / blobdiff