dataConCannotMatch,
- -- GADT type refinement
- Refinement, emptyRefinement, isEmptyRefinement,
- matchRefine, refineType, refinePred, refineResType,
-
-- Side-effect free unification
tcUnifyTys, BindFlag(..)
\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 :: [TyVar] -> [Coercion] -> 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 in_scope_tvs cos
- = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos))
- where
- in_scope = mkInScopeSet (mkVarSet in_scope_tvs)
- -- NB: in_scope_tvs include both coercion variables
- -- *and* the tyvars in their kinds
-
- refineOne co = refine co ty1 ty2
- where
- (ty1, ty2) = coercionKind co
-
- 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}
-
%************************************************************************
%* *