[project @ 2002-02-13 15:14:06 by simonpj]
authorsimonpj <unknown>
Wed, 13 Feb 2002 15:14:07 +0000 (15:14 +0000)
committersimonpj <unknown>
Wed, 13 Feb 2002 15:14:07 +0000 (15:14 +0000)
--------------------------------------------
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
ghc/compiler/typecheck/TcExpr.lhs
ghc/compiler/typecheck/TcSimplify.lhs
ghc/compiler/typecheck/TcType.lhs
ghc/compiler/typecheck/TcUnify.lhs

index 64889ef..7d51052 100644 (file)
@@ -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
index 56fc0e3..81614cb 100644 (file)
@@ -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}
index edf0659..5ef2132 100644 (file)
@@ -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
index 205292b..b8f0878 100644 (file)
@@ -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}
 
 
index 87cd14e..593a735 100644 (file)
@@ -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