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 :: [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}
-
%************************************************************************
%* *
\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