[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

@@ -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

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}

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

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}
 
 

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