TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
SkolemInfo( GenSkol ), MetaDetails(..),
pprTcTyVar, isTauTy, isSigmaTy, mkFunTy, mkFunTys, mkTyConApp,
- tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
- tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
+ tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcEqType,
+ tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, isMetaTyVar,
typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
- pprType, tidySkolemTyVar, isSkolemTyVar )
+ pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar )
import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
openTypeKind, liftedTypeKind, mkArrowKind,
isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
import TcSimplify ( tcSimplifyCheck )
import TcIface ( checkWiredInTyCon )
import TcEnv ( tcGetGlobalTyVars, findGlobals )
-import TyCon ( TyCon, tyConArity, tyConTyVars )
+import TyCon ( TyCon, tyConArity, tyConTyVars, isFunTyCon )
import TysWiredIn ( listTyCon )
import Id ( Id, mkSysLocal )
import Var ( Var, varName, tyVarKind )
-> TcM [TcType] -- Element types, a b c
-- Insists that the Expected type is not a forall-type
-- It's used for wired-in tycons, so we call checkWiredInTyCOn
+ -- Precondition: never called with FunTyCon
zapToTyConApp tc (Check ty)
- = do { checkWiredInTyCon tc ; unifyTyConApp tc ty } -- NB: fails for a forall-type
+ = ASSERT( not (isFunTyCon tc) ) -- Never called with FunTyCon
+ do { checkWiredInTyCon tc ; unifyTyConApp tc ty } -- NB: fails for a forall-type
zapToTyConApp tc (Infer hole)
- = do { (tc_app, elt_tys) <- newTyConApp tc
+ = do { (_, elt_tys, _) <- tcInstTyVars (tyConTyVars tc)
+ ; let tc_app = mkTyConApp tc elt_tys
; writeMutVar hole tc_app
; traceTc (text "zap" <+> ppr tc)
; checkWiredInTyCon tc
----------------------
unifyTyConApp :: TyCon -> TcType -> TcM [TcType]
-unifyTyConApp tc ty = unify_tc_app True tc ty
- -- Add a boolean flag to remember whether to use
- -- the type refinement or not
+unifyTyConApp tc ty
+ = ASSERT( not (isFunTyCon tc) ) -- Never called with FunTyCon
+ unify_tc_app (tyConArity tc) True tc ty
+ -- Add a boolean flag to remember whether
+ -- to use the type refinement or not
unifyListTy :: TcType -> TcM TcType -- Special case for lists
unifyListTy exp_ty = do { [elt_ty] <- unifyTyConApp listTyCon exp_ty
; return elt_ty }
----------
-unify_tc_app use_refinement tc (NoteTy _ ty)
- = unify_tc_app use_refinement tc ty
-
-unify_tc_app use_refinement tc ty@(TyVarTy tyvar)
- = do { details <- condLookupTcTyVar use_refinement tyvar
+unify_tc_app n_args use_refinement tc (NoteTy _ ty)
+ = unify_tc_app n_args use_refinement tc ty
+
+unify_tc_app n_args use_refinement tc (TyConApp tycon arg_tys)
+ | tycon == tc
+ = ASSERT( n_args == length arg_tys ) -- ty::*
+ mapM (wobblify use_refinement) arg_tys
+
+unify_tc_app n_args use_refinement tc (AppTy fun_ty arg_ty)
+ = do { arg_ty' <- wobblify use_refinement arg_ty
+ ; arg_tys <- unify_tc_app (n_args - 1) use_refinement tc fun_ty
+ ; return (arg_tys ++ [arg_ty']) }
+
+unify_tc_app n_args use_refinement tc ty@(TyVarTy tyvar)
+ = do { traceTc (text "unify_tc_app: tyvar" <+> pprTcTyVar tyvar)
+ ; details <- condLookupTcTyVar use_refinement tyvar
; case details of
- IndirectTv use' ty' -> unify_tc_app use' tc ty'
- other -> unify_tc_app_help tc ty
+ IndirectTv use' ty' -> unify_tc_app n_args use' tc ty'
+ other -> unify_tc_app_help n_args tc ty
}
-unify_tc_app use_refinement tc ty
- | Just (tycon, arg_tys) <- tcSplitTyConApp_maybe ty,
- tycon == tc
- = ASSERT( tyConArity tycon == length arg_tys ) -- ty::*
- mapM (wobblify use_refinement) arg_tys
-
-unify_tc_app use_refinement tc ty = unify_tc_app_help tc ty
+unify_tc_app n_args use_refinement tc ty = unify_tc_app_help n_args tc ty
-unify_tc_app_help tc ty -- Revert to ordinary unification
- = do { (tc_app, arg_tys) <- newTyConApp tc
+unify_tc_app_help n_args tc ty -- Revert to ordinary unification
+ = do { (_, elt_tys, _) <- tcInstTyVars (take n_args (tyConTyVars tc))
+ ; let tc_app = mkTyConApp tc elt_tys
; if not (isTauTy ty) then -- Can happen if we call zapToTyConApp tc (forall a. ty)
unifyMisMatch ty tc_app
else do
{ unifyTauTy ty tc_app
- ; returnM arg_tys } }
+ ; returnM elt_tys } }
----------------------
-> TcM TcTauType
-- Return a wobbly type. At the moment we do that by
-- allocating a fresh meta type variable.
-wobblify True ty = return ty
+wobblify True ty = return ty -- Don't wobblify
+
+wobblify False ty@(TyVarTy tv)
+ | isMetaTyVar tv = return ty -- Already wobbly
+
wobblify False ty = do { uniq <- newUnique
; tv <- newMetaTyVar (mkSysTvName uniq FSLIT("w"))
(typeKind ty)
(Indirect ty)
; return (mkTyVarTy tv) }
-
-----------------------
-newTyConApp :: TyCon -> TcM (TcTauType, [TcTauType])
-newTyConApp tc = do { (tvs, args, _) <- tcInstTyVars (tyConTyVars tc)
- ; return (mkTyConApp tc args, args) }
\end{code}
-- See Note [Pattern coercions] in TcPat
-- However, we can't call unify directly, because both types might be
-- polymorphic; hence the call to tcSub, followed by a check for
--- the identity coercion
+-- equal types. (We can't just check for the identity coercion, because
+-- in the polymorphic case we might get back something eta-equivalent to
+-- the identity coercion, but that's not easy to tell.)
tcSubPat sig_ty (Infer hole)
= do { sig_ty' <- zonkTcType sig_ty
; writeMutVar hole sig_ty' -- See notes with tcSubExp above
; return () }
+-- This tcSub followed by tcEqType checks for identical types
+-- It'd be done more neatly by augmenting the unifier to deal with
+-- (identically shaped) for-all types.
+
tcSubPat sig_ty (Check exp_ty)
= do { co_fn <- tcSub sig_ty exp_ty
-
- ; if isIdCoercion co_fn then
+ ; sig_ty' <- zonkTcType sig_ty
+ ; exp_ty' <- zonkTcType exp_ty
+ ; if tcEqType sig_ty' exp_ty' then
return ()
- else
- unifyMisMatch sig_ty exp_ty }
+ else do
+ { (env, msg) <- misMatchMsg sig_ty' exp_ty'
+ ; failWithTcM (env, msg $$ extra) } }
+ where
+ extra | isTauTy sig_ty = empty
+ | otherwise = ptext SLIT("Polymorphic types must match exactly in patterns")
\end{code}
pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
unifyMisMatch ty1 ty2
+ = do { (env, msg) <- misMatchMsg ty1 ty2
+ ; failWithTcM (env, msg) }
+
+misMatchMsg ty1 ty2
= do { (env1, pp1, extra1) <- ppr_ty emptyTidyEnv ty1
; (env2, pp2, extra2) <- ppr_ty env1 ty2
- ; let msg = sep [sep [ptext SLIT("Couldn't match") <+> pp1, nest 7 (ptext SLIT("against") <+> pp2)],
- nest 2 extra1, nest 2 extra2]
- in
- failWithTcM (env2, msg) }
+ ; return (env2, sep [sep [ptext SLIT("Couldn't match") <+> pp1,
+ nest 7 (ptext SLIT("against") <+> pp2)],
+ nest 2 extra1, nest 2 extra2]) }
ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
ppr_ty env ty
(act_as, _) = splitKindFunTys act_kind
n_exp_as = length exp_as
n_act_as = length act_as
+
+ (env1, tidy_exp_kind) = tidyKind emptyTidyEnv exp_kind
+ (env2, tidy_act_kind) = tidyKind env1 act_kind
err | n_exp_as < n_act_as -- E.g. [Maybe]
= quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
= ptext SLIT("Kind mis-match")
more_info = sep [ ptext SLIT("Expected kind") <+>
- quotes (pprKind exp_kind) <> comma,
+ quotes (pprKind tidy_exp_kind) <> comma,
ptext SLIT("but") <+> quotes (ppr ty) <+>
- ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
+ ptext SLIT("has kind") <+> quotes (pprKind tidy_act_kind)]
in
- failWithTc (err $$ more_info)
+ failWithTcM (env2, err $$ more_info)
}
\end{code}
projects / ghc-hetmet.git / blobdiff