From: simonpj Date: Wed, 12 Oct 2005 13:31:12 +0000 (+0000) Subject: [project @ 2005-10-12 13:31:12 by simonpj] X-Git-Tag: Initial_conversion_from_CVS_complete~174 X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=9334e393c162616a61c787833b126d3bde404dfa [project @ 2005-10-12 13:31:12 by simonpj] MERGE TO STABLE Fix a bug in TcUnify.unifyTyConApp that made a GADT program fail. The trouble happens if the type that we are expecting to be a TyConApp is of form (m a b), where 'm' is refined to a type constructor. Then we want to get nice rigid results, and we weren't. --- diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index 1aa32b6..97487ce 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -38,7 +38,7 @@ import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType, SkolemInfo( GenSkol ), MetaDetails(..), pprTcTyVar, isTauTy, isSigmaTy, mkFunTy, mkFunTys, mkTyConApp, tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcEqType, - tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, + tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, isMetaTyVar, typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy, tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar ) @@ -54,7 +54,7 @@ import TcMType ( condLookupTcTyVar, LookupTyVarResult(..), 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 ) @@ -293,11 +293,14 @@ zapToTyConApp :: TyCon -- T :: k1 -> ... -> kn -> * -> 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 @@ -309,40 +312,48 @@ zapToListTy exp_ty = do { [elt_ty] <- zapToTyConApp listTyCon exp_ty ---------------------- 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 } } ---------------------- @@ -382,17 +393,16 @@ wobblify :: Bool -- True <=> don't wobblify -> 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}