From e70309951a888dfa8629b2e07dbc30795550f868 Mon Sep 17 00:00:00 2001 From: simonpj Date: Wed, 13 Feb 2002 15:14:07 +0000 Subject: [PATCH] [project @ 2002-02-13 15:14:06 by simonpj] -------------------------------------------- Fix a bugs in type inference for rank-N types -------------------------------------------- We discovered this bug when looking at type rules! 1. When type checking (e :: sigma-ty), we must specialise sigma-ty, else we lose the invariant that tcMonoType has. 2. In tcExpr_id, we should pass in a Hole tyvar not an ordinary tyvar. As usual, I moved some functions around in consequence. --- ghc/compiler/typecheck/Inst.lhs | 77 ++++++------------------------- ghc/compiler/typecheck/TcExpr.lhs | 80 +++++++++++++++++++++++++++++---- ghc/compiler/typecheck/TcSimplify.lhs | 4 +- ghc/compiler/typecheck/TcType.lhs | 14 +++--- ghc/compiler/typecheck/TcUnify.lhs | 15 ++----- 5 files changed, 100 insertions(+), 90 deletions(-) diff --git a/ghc/compiler/typecheck/Inst.lhs b/ghc/compiler/typecheck/Inst.lhs index 64889ef..7d51052 100644 --- a/ghc/compiler/typecheck/Inst.lhs +++ b/ghc/compiler/typecheck/Inst.lhs @@ -13,7 +13,7 @@ module Inst ( newDictsFromOld, newDicts, cloneDict, newMethod, newMethodWithGivenTy, newMethodAtLoc, - newOverloadedLit, newIPDict, tcInstId, + newOverloadedLit, newIPDict, tcInstCall, tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, ipNamesOfInst, ipNamesOfInsts, predsOfInst, predsOfInsts, @@ -21,7 +21,8 @@ module Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..), - isDict, isClassDict, isMethod, isLinearInst, linearInstType, + isDict, isClassDict, isMethod, + isLinearInst, linearInstType, isTyVarDict, isStdClassTyVarDict, isMethodFor, instBindingRequired, instCanBeGeneralised, @@ -35,7 +36,7 @@ module Inst ( import CmdLineOpts ( opt_NoMethodSharing ) import HsSyn ( HsLit(..), HsOverLit(..), HsExpr(..) ) -import TcHsSyn ( TcExpr, TcId, +import TcHsSyn ( TcExpr, TcId, TypecheckedHsExpr, mkHsTyApp, mkHsDictApp, mkHsConApp, zonkId ) import TcMonad @@ -51,7 +52,7 @@ import TcType ( Type, TcType, TcThetaType, TcPredType, TcTauType, TcTyVarSet, isIntTy,isFloatTy, isIntegerTy, isDoubleTy, tcIsTyVarTy, mkPredTy, mkTyVarTy, mkTyVarTys, tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tidyPred, - isClassPred, isTyVarClassPred, + isClassPred, isTyVarClassPred, isLinearPred, getClassPredTys, getClassPredTys_maybe, mkPredName, tidyType, tidyTypes, tidyFreeTyVars, tcCmpType, tcCmpTypes, tcCmpPred @@ -272,11 +273,7 @@ isLinearInst other = False -- We never build Method Insts that have -- linear implicit paramters in them. -- Hence no need to look for Methods - -- See Inst.tcInstId - -isLinearPred :: TcPredType -> Bool -isLinearPred (IParam (Linear n) _) = True -isLinearPred other = False + -- See TcExpr.tcId linearInstType :: Inst -> TcType -- %x::t --> t linearInstType (Dict _ (IParam _ ty) _) = ty @@ -358,62 +355,16 @@ newIPDict orig ip_name ty %* * %************************************************************************ -tcInstId instantiates an occurrence of an Id. -The instantiate_it loop runs round instantiating the Id. -It has to be a loop because we are now prepared to entertain -types like - f:: forall a. Eq a => forall b. Baz b => tau -We want to instantiate this to - f2::tau {f2 = f1 b (Baz b), f1 = f a (Eq a)} - -The -fno-method-sharing flag controls what happens so far as the LIE -is concerned. The default case is that for an overloaded function we -generate a "method" Id, and add the Method Inst to the LIE. So you get -something like - f :: Num a => a -> a - f = /\a (d:Num a) -> let m = (+) a d in \ (x:a) -> m x x -If you specify -fno-method-sharing, the dictionary application -isn't shared, so we get - f :: Num a => a -> a - f = /\a (d:Num a) (x:a) -> (+) a d x x -This gets a bit less sharing, but - a) it's better for RULEs involving overloaded functions - b) perhaps fewer separated lambdas - \begin{code} -tcInstId :: Id -> NF_TcM (TcExpr, LIE, TcType) -tcInstId fun - = loop (HsVar fun) emptyLIE (idType fun) - where - orig = OccurrenceOf fun - loop fun lie fun_ty = tcInstType fun_ty `thenNF_Tc` \ (tyvars, theta, tau) -> - loop_help fun lie (mkTyVarTys tyvars) theta tau - - loop_help fun lie arg_tys [] tau -- Not overloaded - = returnNF_Tc (mkHsTyApp fun arg_tys, lie, tau) - - loop_help (HsVar fun_id) lie arg_tys theta tau - | can_share theta -- Sharable method binding - = newMethodWithGivenTy orig fun_id arg_tys theta tau `thenNF_Tc` \ meth -> - loop (HsVar (instToId meth)) - (unitLIE meth `plusLIE` lie) tau - - loop_help fun lie arg_tys theta tau -- The general case - = newDicts orig theta `thenNF_Tc` \ dicts -> - loop (mkHsDictApp (mkHsTyApp fun arg_tys) (map instToId dicts)) - (mkLIE dicts `plusLIE` lie) tau - - can_share theta | opt_NoMethodSharing = False - | otherwise = not (any isLinearPred theta) - -- This is a slight hack. - -- If f :: (%x :: T) => Int -> Int - -- Then if we have two separate calls, (f 3, f 4), we cannot - -- make a method constraint that then gets shared, thus: - -- let m = f %x in (m 3, m 4) - -- because that loses the linearity of the constraint. - -- The simplest thing to do is never to construct a method constraint - -- in the first place that has a linear implicit parameter in it. +tcInstCall :: InstOrigin -> TcType -> NF_TcM (TypecheckedHsExpr -> TypecheckedHsExpr, LIE, TcType) +tcInstCall orig fun_ty -- fun_ty is usually a sigma-type + = tcInstType fun_ty `thenNF_Tc` \ (tyvars, theta, tau) -> + newDicts orig theta `thenNF_Tc` \ dicts -> + let + inst_fn e = mkHsDictApp (mkHsTyApp e (mkTyVarTys tyvars)) (map instToId dicts) + in + returnNF_Tc (inst_fn, mkLIE dicts, tau) newMethod :: InstOrigin -> TcId diff --git a/ghc/compiler/typecheck/TcExpr.lhs b/ghc/compiler/typecheck/TcExpr.lhs index 56fc0e3..81614cb 100644 --- a/ghc/compiler/typecheck/TcExpr.lhs +++ b/ghc/compiler/typecheck/TcExpr.lhs @@ -22,8 +22,8 @@ import BasicTypes ( RecFlag(..), isMarkedStrict ) import Inst ( InstOrigin(..), LIE, mkLIE, emptyLIE, unitLIE, plusLIE, plusLIEs, newOverloadedLit, newMethod, newIPDict, - newDicts, - instToId, tcInstId + newDicts, newMethodWithGivenTy, + instToId, tcInstCall ) import TcBinds ( tcBindsAndThen ) import TcEnv ( tcLookupClass, tcLookupGlobalId, tcLookupGlobal_maybe, @@ -33,12 +33,13 @@ import TcMatches ( tcMatchesCase, tcMatchLambda, tcStmts ) import TcMonoType ( tcHsSigType, UserTypeCtxt(..) ) import TcPat ( badFieldCon ) import TcSimplify ( tcSimplifyIPs ) -import TcMType ( tcInstTyVars, newTyVarTy, newTyVarTys, zonkTcType ) +import TcMType ( tcInstTyVars, tcInstType, newHoleTyVarTy, + newTyVarTy, newTyVarTys, zonkTcType ) import TcType ( TcType, TcSigmaType, TcPhiType, - tcSplitFunTys, tcSplitTyConApp, + tcSplitFunTys, tcSplitTyConApp, mkTyVarTys, isSigmaTy, mkFunTy, mkAppTy, mkTyConTy, mkTyConApp, mkClassPred, tcFunArgTy, - tyVarsOfTypes, + tyVarsOfTypes, isLinearPred, liftedTypeKind, openTypeKind, mkArrowKind, tcSplitSigmaTy, tcTyConAppTyCon, tidyOpenType @@ -130,8 +131,14 @@ tcMonoExpr in_expr@(ExprWithTySig expr poly_ty) res_ty = tcHsSigType ExprSigCtxt poly_ty `thenTc` \ sig_tc_ty -> tcAddErrCtxt (exprSigCtxt in_expr) $ tcExpr expr sig_tc_ty `thenTc` \ (expr', lie1) -> - tcSub res_ty sig_tc_ty `thenTc` \ (co_fn, lie2) -> - returnTc (co_fn <$> expr', lie1 `plusLIE` lie2) + + -- Must instantiate the outer for-alls of sig_tc_ty + -- else we risk instantiating a ? res_ty to a forall-type + -- which breaks the invariant that tcMonoExpr only returns phi-types + tcInstCall SignatureOrigin sig_tc_ty `thenNF_Tc` \ (inst_fn, lie2, inst_sig_ty) -> + tcSub res_ty inst_sig_ty `thenTc` \ (co_fn, lie3) -> + + returnTc (co_fn <$> inst_fn expr', lie1 `plusLIE` lie2 `plusLIE` lie3) \end{code} @@ -703,19 +710,74 @@ tcArg the_fun (arg, expected_arg_ty, arg_no) %* * %************************************************************************ +tcId instantiates an occurrence of an Id. +The instantiate_it loop runs round instantiating the Id. +It has to be a loop because we are now prepared to entertain +types like + f:: forall a. Eq a => forall b. Baz b => tau +We want to instantiate this to + f2::tau {f2 = f1 b (Baz b), f1 = f a (Eq a)} + +The -fno-method-sharing flag controls what happens so far as the LIE +is concerned. The default case is that for an overloaded function we +generate a "method" Id, and add the Method Inst to the LIE. So you get +something like + f :: Num a => a -> a + f = /\a (d:Num a) -> let m = (+) a d in \ (x:a) -> m x x +If you specify -fno-method-sharing, the dictionary application +isn't shared, so we get + f :: Num a => a -> a + f = /\a (d:Num a) (x:a) -> (+) a d x x +This gets a bit less sharing, but + a) it's better for RULEs involving overloaded functions + b) perhaps fewer separated lambdas + \begin{code} tcId :: Name -> NF_TcM (TcExpr, LIE, TcType) tcId name -- Look up the Id and instantiate its type = tcLookupId name `thenNF_Tc` \ id -> - tcInstId id + loop (OccurrenceOf id) (HsVar id) emptyLIE (idType id) + where + loop orig (HsVar fun_id) lie fun_ty + | want_method_inst fun_ty + = tcInstType fun_ty `thenNF_Tc` \ (tyvars, theta, tau) -> + newMethodWithGivenTy orig fun_id + (mkTyVarTys tyvars) theta tau `thenNF_Tc` \ meth -> + loop orig (HsVar (instToId meth)) + (unitLIE meth `plusLIE` lie) tau + + loop orig fun lie fun_ty + | isSigmaTy fun_ty + = tcInstCall orig fun_ty `thenNF_Tc` \ (inst_fn, inst_lie, tau) -> + loop orig (inst_fn fun) (inst_lie `plusLIE` lie) tau + + | otherwise + = returnNF_Tc (fun, lie, fun_ty) + + want_method_inst fun_ty + | opt_NoMethodSharing = False + | otherwise = case tcSplitSigmaTy fun_ty of + (_,[],_) -> False -- Not overloaded + (_,theta,_) -> not (any isLinearPred theta) + -- This is a slight hack. + -- If f :: (%x :: T) => Int -> Int + -- Then if we have two separate calls, (f 3, f 4), we cannot + -- make a method constraint that then gets shared, thus: + -- let m = f %x in (m 3, m 4) + -- because that loses the linearity of the constraint. + -- The simplest thing to do is never to construct a method constraint + -- in the first place that has a linear implicit parameter in it. \end{code} Typecheck expression which in most cases will be an Id. +The expression can return a higher-ranked type, such as + (forall a. a->a) -> Int +so we must create a HoleTyVarTy to pass in as the expected tyvar. \begin{code} tcExpr_id :: RenamedHsExpr -> TcM (TcExpr, LIE, TcType) tcExpr_id (HsVar name) = tcId name -tcExpr_id expr = newTyVarTy openTypeKind `thenNF_Tc` \ id_ty -> +tcExpr_id expr = newHoleTyVarTy `thenNF_Tc` \ id_ty -> tcMonoExpr expr id_ty `thenTc` \ (expr', lie_id) -> returnTc (expr', lie_id, id_ty) \end{code} diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs index edf0659..5ef2132 100644 --- a/ghc/compiler/typecheck/TcSimplify.lhs +++ b/ghc/compiler/typecheck/TcSimplify.lhs @@ -44,7 +44,7 @@ import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity ) import TcType ( TcTyVar, TcTyVarSet, ThetaType, mkClassPred, isOverloadedTy, mkTyConApp, mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys, - tyVarsOfPred, isIPPred, inheritablePred, predHasFDs ) + tyVarsOfPred, isIPPred, isInheritablePred, predHasFDs ) import Id ( idType, mkUserLocal ) import Var ( TyVar ) import Name ( getOccName, getSrcLoc ) @@ -635,7 +635,7 @@ The net effect of [NO TYVARS] isFreeWhenInferring :: TyVarSet -> Inst -> Bool isFreeWhenInferring qtvs inst = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars - && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved + && all isInheritablePred (predsOfInst inst) -- And no implicit parameter involved -- (see "Notes on implicit parameters") isFreeWhenChecking :: TyVarSet -- Quantified tyvars diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index 205292b..b8f0878 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -59,7 +59,7 @@ module TcType ( isPredTy, isClassPred, isTyVarClassPred, predHasFDs, mkDictTy, tcSplitPredTy_maybe, predTyUnique, isDictTy, tcSplitDFunTy, predTyUnique, - mkClassPred, inheritablePred, isIPPred, mkPredName, + mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, --------------------------------- -- Foreign import and export @@ -137,7 +137,7 @@ import OccName ( OccName, mkDictOcc ) import NameSet import PrelNames -- Lots (e.g. in isFFIArgumentTy) import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon ) -import BasicTypes ( ipNameName ) +import BasicTypes ( IPName(..), ipNameName ) import Unique ( Unique, Uniquable(..) ) import SrcLoc ( SrcLoc ) import Util ( cmpList, thenCmp, equalLength ) @@ -530,7 +530,7 @@ isIPPred :: SourceType -> Bool isIPPred (IParam _ _) = True isIPPred other = False -inheritablePred :: PredType -> Bool +isInheritablePred :: PredType -> Bool -- Can be inherited by a context. For example, consider -- f x = let g y = (?v, y+x) -- in (g 3 with ?v = 8, @@ -539,8 +539,12 @@ inheritablePred :: PredType -> Bool -- g :: (?v :: a) => a -> a -- but it doesn't need to be quantified over the Num a dictionary -- which can be free in g's rhs, and shared by both calls to g -inheritablePred (ClassP _ _) = True -inheritablePred other = False +isInheritablePred (ClassP _ _) = True +isInheritablePred other = False + +isLinearPred :: TcPredType -> Bool +isLinearPred (IParam (Linear n) _) = True +isLinearPred other = False \end{code} diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index 87cd14e..593a735 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -45,7 +45,7 @@ import TcType ( TcKind, TcType, TcSigmaType, TcPhiType, TcTyVar, TcTauType, ) import qualified Type ( getTyVar_maybe ) import Inst ( LIE, emptyLIE, plusLIE, mkLIE, - newDicts, instToId + newDicts, instToId, tcInstCall ) import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy, @@ -160,16 +160,9 @@ tc_sub exp_sty expected_ty act_sty actual_ty tc_sub exp_sty expected_ty act_sty actual_ty | isSigmaTy actual_ty - = tcInstType actual_ty `thenNF_Tc` \ (tvs, theta, body_ty) -> - newDicts orig theta `thenNF_Tc` \ dicts -> - let - inst_fn e = mkHsDictApp (mkHsTyApp e (mkTyVarTys tvs)) - (map instToId dicts) - in - tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie) -> - returnTc (co_fn <.> mkCoercion inst_fn, lie `plusLIE` mkLIE dicts) - where - orig = Rank2Origin + = tcInstCall Rank2Origin actual_ty `thenNF_Tc` \ (inst_fn, lie1, body_ty) -> + tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie2) -> + returnTc (co_fn <.> mkCoercion inst_fn, lie1 `plusLIE` lie2) ----------------------------------- -- Function case -- 1.7.10.4