--------------------------------
-- TyVarDetails
- TyVarDetails(..), isUserTyVar, isSkolemTyVar,
+ TyVarDetails(..), isUserTyVar, isSkolemTyVar, isExistentialTyVar,
tyVarBindingInfo,
--------------------------------
| PatSigTv -- Scoped type variable, introduced by a pattern
-- type signature \ x::a -> e
+ | ExistTv -- An existential type variable bound by a pattern for
+ -- a data constructor with an existential type. E.g.
+ -- data T = forall a. Eq a => MkT a
+ -- f (MkT x) = ...
+ -- The pattern MkT x will allocate an existential type
+ -- variable for 'a'. We distinguish these from all others
+ -- on one place, namely InstEnv.lookupInstEnv.
+
| VanillaTv -- Everything else
isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
isSkolemTyVar :: TcTyVar -> Bool
isSkolemTyVar tv = case tcTyVarDetails tv of
- SigTv -> True
- ClsTv -> True
- InstTv -> True
- oteher -> False
+ SigTv -> True
+ ClsTv -> True
+ InstTv -> True
+ ExistTv -> True
+ other -> False
+
+isExistentialTyVar :: TcTyVar -> Bool
+isExistentialTyVar tv = case tcTyVarDetails tv of
+ ExistTv -> True
+ other -> False
tyVarBindingInfo :: TcTyVar -> SDoc -- Used in checkSigTyVars
tyVarBindingInfo tv
details ClsTv = ptext SLIT("class declaration")
details InstTv = ptext SLIT("instance declaration")
details PatSigTv = ptext SLIT("pattern type signature")
+ details ExistTv = ptext SLIT("existential constructor")
details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
\end{code}
checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
-- Look through newtypes
-- Non-recursive ones are transparent to splitTyConApp,
- -- but recursive ones aren't
+ -- but recursive ones aren't. Manuel had:
+ -- newtype T = MkT (Ptr T)
+ -- and wanted it to work...
checkRepTyCon check_tc ty
| Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
| otherwise = False
| v `elemVarSet` tmpls
= -- v is a template variable
case lookupSubstEnv senv v of
- Nothing | typeKind ty == tyVarKind v
+ Nothing | typeKind ty `isSubKind` tyVarKind v
-- We do a kind check, just as in the uVarX above
-- The kind check is needed to avoid bogus matches
-- of (a b) with (c d), where the kinds don't match
match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
= match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
+ -- If the template is an application, try to make the
+ -- thing we are matching look like an application
match (AppTy fun1 arg1) ty2 tmpls k senv
= case tcSplitAppTy_maybe ty2 of
Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
Nothing -> Nothing -- Fail
--- Newtypes are opaque; predicate types should not happen
+ -- Newtypes are opaque; predicate types should not happen
match (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) tmpls k senv
| tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv