#include "HsVersions.h"
-import HsSyn ( HsExpr(..) , MatchGroup(..), hsLMatchPats )
-import TcHsSyn ( mkHsLet, mkHsDictLam,
+import HsSyn ( HsExpr(..) , MatchGroup(..), HsMatchContext(..),
+ hsLMatchPats, pprMatches, pprMatchContext )
+import TcHsSyn ( mkHsDictLet, mkHsDictLam,
ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
import TypeRep ( Type(..), PredType(..), TyNote(..) )
import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
SkolemInfo( GenSkol ), MetaDetails(..),
- pprTcTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
- tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
- tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
+ pprTcTyVar, isTauTy, isSigmaTy, mkFunTy, mkFunTys, mkTyConApp,
+ 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 )
import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
import VarEnv
-import Name ( isSystemName, mkSysTvName )
+import Name ( Name, isSystemName, mkSysTvName )
import ErrUtils ( Message )
import SrcLoc ( noLoc )
import BasicTypes ( Arity )
type variables, so we should create new ordinary type variables
\begin{code}
-subFunTys :: MatchGroup name
+subFunTys :: HsMatchContext Name
+ -> MatchGroup Name
-> Expected TcRhoType -- Fail if ty isn't a function type
-> ([Expected TcRhoType] -> Expected TcRhoType -> TcM a)
-> TcM a
-subFunTys (MatchGroup (match:null_matches) _) (Infer hole) thing_inside
+subFunTys ctxt (MatchGroup (match:null_matches) _) (Infer hole) thing_inside
= -- This is the interesting case
ASSERT( null null_matches )
do { pat_holes <- mapM (\ _ -> newHole) (hsLMatchPats match)
-- And return the answer
; return res }
-subFunTys (MatchGroup (match:matches) _) (Check ty) thing_inside
- = ASSERT( all ((== length (hsLMatchPats match)) . length . hsLMatchPats) matches )
+subFunTys ctxt group@(MatchGroup (match:matches) _) (Check ty) thing_inside
+ = ASSERT( all ((== n_pats) . length . hsLMatchPats) matches )
-- Assertion just checks that all the matches have the same number of pats
- do { (pat_tys, res_ty) <- unifyFunTys (length (hsLMatchPats match)) ty
+ do { (pat_tys, res_ty) <- unifyFunTys msg n_pats ty
; thing_inside (map Check pat_tys) (Check res_ty) }
-
-unifyFunTys :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
+ where
+ n_pats = length (hsLMatchPats match)
+ msg = case ctxt of
+ FunRhs fun -> ptext SLIT("The equation(s) for") <+> quotes (ppr fun)
+ <+> ptext SLIT("have") <+> speakNOf n_pats (ptext SLIT("argument"))
+ LambdaExpr -> sep [ ptext SLIT("The lambda expression")
+ <+> quotes (pprSetDepth 1 $ pprMatches ctxt group),
+ -- The pprSetDepth makes the abstraction print briefly
+ ptext SLIT("has") <+> speakNOf n_pats (ptext SLIT("arguments"))]
+ other -> pprPanic "subFunTys" (pprMatchContext ctxt)
+
+
+unifyFunTys :: SDoc -> Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
-- Fail if ty isn't a function type, otherwise return arg and result types
-- The result types are guaranteed wobbly if the argument is wobbly
--
--
-- (b) GADTs: if the argument is not wobbly we do not want the result to be
-unifyFunTys arity ty = unify_fun_ty True arity ty
+{-
+ Error messages from unifyFunTys
+ The first line is passed in as error_herald
+
+ The abstraction `\Just 1 -> ...' has two arguments
+ but its type `Maybe a -> a' has only one
+
+ The equation(s) for `f' have two arguments
+ but its type `Maybe a -> a' has only one
+
+ The section `(f 3)' requires 'f' to take two arguments
+ but its type `Int -> Int' has only one
+
+ The function 'f' is applied to two arguments
+ but its type `Int -> Int' has only one
+-}
+
+unifyFunTys error_herald arity ty
+ -- error_herald is the whole first line of the error message above
+ = do { (ok, args, res) <- unify_fun_ty True arity ty
+ ; if ok then return (args, res)
+ else failWithTc (mk_msg (length args)) }
+ where
+ mk_msg n_actual
+ = error_herald <> comma $$
+ sep [ptext SLIT("but its type") <+> quotes (pprType ty),
+ if n_actual == 0 then ptext SLIT("has none")
+ else ptext SLIT("has only") <+> speakN n_actual]
+
+unify_fun_ty :: Bool -> Arity -> TcRhoType
+ -> TcM (Bool, -- Arity satisfied?
+ [TcSigmaType], -- Arg types found; length <= arity
+ TcRhoType) -- Result type
unify_fun_ty use_refinement arity ty
| arity == 0
= do { res_ty <- wobblify use_refinement ty
- ; return ([], ty) }
+ ; return (True, [], ty) }
unify_fun_ty use_refinement arity (NoteTy _ ty)
= unify_fun_ty use_refinement arity ty
= do { details <- condLookupTcTyVar use_refinement tv
; case details of
IndirectTv use' ty' -> unify_fun_ty use' arity ty'
- other -> unify_fun_help arity ty
+ DoneTv (MetaTv ref) -> ASSERT( liftedTypeKind `isSubKind` tyVarKind tv )
+ -- The argument to unifyFunTys is always a type
+ -- Occurs check can't happen, of course
+ do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind)
+ ; res <- newTyFlexiVarTy openTypeKind
+ ; writeMutVar ref (Indirect (mkFunTys args res))
+ ; return (True, args, res) }
+ DoneTv skol -> return (False, [], ty)
}
unify_fun_ty use_refinement arity ty
- = case tcSplitFunTy_maybe ty of
- Just (arg,res) -> do { arg' <- wobblify use_refinement arg
- ; (args', res') <- unify_fun_ty use_refinement (arity-1) res
- ; return (arg':args', res') }
-
- Nothing -> unify_fun_help arity ty
- -- Usually an error, but ty could be (a Int Bool), which can match
-
-unify_fun_help :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
-unify_fun_help arity ty
- = do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind)
- ; res <- newTyFlexiVarTy openTypeKind
- ; unifyTauTy ty (mkFunTys args res)
- ; return (args, res) }
+ | Just (arg,res) <- tcSplitFunTy_maybe ty
+ = do { arg' <- wobblify use_refinement arg
+ ; (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res
+ ; return (ok, arg':args', res') }
+
+unify_fun_ty use_refinement arity ty
+-- Common cases are all done by now
+-- At this point we usually have an error, but ty could
+-- be (a Int Bool), or (a Bool), which can match
+-- So just use the unifier. But catch any error so we just
+-- return the success/fail boolean
+ = do { arg <- newTyFlexiVarTy argTypeKind
+ ; res <- newTyFlexiVarTy openTypeKind
+ ; let fun_ty = mkFunTy arg res
+ ; (_, mb_unit) <- tryTc (uTys True ty ty True fun_ty fun_ty)
+ ; case mb_unit of {
+ Nothing -> return (False, [], ty) ;
+ Just _ ->
+ do { (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res
+ ; return (ok, arg:args', res')
+ } } }
\end{code}
\begin{code}
-> 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}
-- I'm not quite sure what to do about this!
tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty
- = do { ([act_arg], act_res) <- unifyFunTys 1 act_ty
+ = do { (act_arg, act_res) <- unify_fun act_ty
; tcSub_fun exp_arg exp_res act_arg act_res }
tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res)
- = do { ([exp_arg], exp_res) <- unifyFunTys 1 exp_ty
+ = do { (exp_arg, exp_res) <- unify_fun exp_ty
; tcSub_fun exp_arg exp_res act_arg act_res }
-----------------------------------
tc_sub exp_sty expected_ty act_sty actual_ty
= uTys True exp_sty expected_ty True act_sty actual_ty `thenM_`
returnM idCoercion
+
+-----------------------------------
+-- A helper to make a function type match
+-- The error message isn't very good, but that's a problem with
+-- all of this subsumption code
+unify_fun ty
+ = do { (ok, args, res) <- unify_fun_ty True 1 ty
+ ; if ok then return (head args, res)
+ else failWithTc (ptext SLIT("Expecting a function type, but found") <+> quotes (ppr ty))}
\end{code}
\begin{code}
-- It's a bit out of place here, but using AbsBind involves inventing
-- a couple of new names which seems worse.
dict_ids = map instToId dicts
- co_fn e = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsLet inst_binds (noLoc e)))
+ co_fn e = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsDictLet inst_binds (noLoc e)))
; returnM (mkCoercion co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
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