Use implication constraints to improve type inference
[ghc-hetmet.git] / compiler / typecheck / TcBinds.lhs
index 4223af4..9e0b583 100644 (file)
@@ -1,4 +1,5 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcBinds]{TcBinds}
@@ -15,57 +16,36 @@ module TcBinds ( tcLocalBinds, tcTopBinds,
 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
 
-import DynFlags                ( dopt, DynFlags,
-                         DynFlag(Opt_MonomorphismRestriction, Opt_MonoPatBinds, Opt_GlasgowExts) )
-import HsSyn           ( HsExpr(..), HsBind(..), LHsBinds, LHsBind, Sig(..),
-                         HsLocalBinds(..), HsValBinds(..), HsIPBinds(..),
-                         LSig, Match(..), IPBind(..), Prag(..),
-                         HsType(..), LHsType, HsExplicitForAll(..), hsLTyVarNames, 
-                         isVanillaLSig, sigName, placeHolderNames, isPragLSig,
-                         LPat, GRHSs, MatchGroup(..), pprLHsBinds, mkHsCoerce,
-                         collectHsBindBinders, collectPatBinders, pprPatBind, isBangHsBind
-                       )
-import TcHsSyn         ( zonkId )
+import DynFlags
+import HsSyn
+import TcHsSyn
 
 import TcRnMonad
-import Inst            ( newDictBndrs, newIPDict, instToId )
-import TcEnv           ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2, 
-                         pprBinders, tcLookupId,
-                         tcGetGlobalTyVars )
-import TcUnify         ( tcInfer, tcSubExp, unifyTheta, 
-                         bleatEscapedTvs, sigCtxt )
-import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, 
-                         tcSimplifyRestricted, tcSimplifyIPs )
-import TcHsType                ( tcHsSigType, UserTypeCtxt(..) )
-import TcPat           ( tcLetPat )
-import TcSimplify      ( bindInstsOfLocalFuns )
-import TcMType         ( newFlexiTyVarTy, zonkQuantifiedTyVar, zonkSigTyVar,
-                         tcInstSigTyVars, tcInstSkolTyVars, tcInstType, 
-                         zonkTcType, zonkTcTypes, zonkTcTyVar )
-import TcType          ( TcType, TcTyVar, TcThetaType, 
-                         SkolemInfo(SigSkol), UserTypeCtxt(FunSigCtxt), 
-                         TcTauType, TcSigmaType, isUnboxedTupleType,
-                         mkTyVarTy, mkForAllTys, mkFunTys, exactTyVarsOfType, 
-                         mkForAllTy, isUnLiftedType, tcGetTyVar, 
-                         mkTyVarTys, tidyOpenTyVar )
-import {- Kind parts of -} Type                ( argTypeKind )
-import VarEnv          ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv ) 
-import TysPrim         ( alphaTyVar )
-import Id              ( Id, mkLocalId, mkVanillaGlobal )
-import IdInfo          ( vanillaIdInfo )
-import Var             ( TyVar, idType, idName )
-import Name            ( Name )
+import Inst
+import TcEnv
+import TcUnify
+import TcSimplify
+import TcHsType
+import TcPat
+import TcMType
+import TcType
+import {- Kind parts of -} Type
+import VarEnv
+import TysPrim
+import Id
+import IdInfo
+import Var ( TyVar )
+import Name
 import NameSet
 import NameEnv
 import VarSet
-import SrcLoc          ( Located(..), unLoc, getLoc )
+import SrcLoc
 import Bag
-import ErrUtils                ( Message )
-import Digraph         ( SCC(..), stronglyConnComp )
-import Maybes          ( expectJust, isJust, isNothing, orElse )
-import Util            ( singleton )
-import BasicTypes      ( TopLevelFlag(..), isTopLevel, isNotTopLevel,
-                         RecFlag(..), isNonRec, InlineSpec, defaultInlineSpec )
+import ErrUtils
+import Digraph
+import Maybes
+import Util
+import BasicTypes
 import Outputable
 \end{code}
 
@@ -439,7 +419,7 @@ tcSpecPrag poly_id hs_ty inl
        ; (co_fn, lie) <- getLIE (tcSubExp (idType poly_id) spec_ty)
        ; extendLIEs lie
        ; let const_dicts = map instToId lie
-       ; return (SpecPrag (mkHsCoerce co_fn (HsVar poly_id)) spec_ty const_dicts inl) }
+       ; return (SpecPrag (mkHsWrap co_fn (HsVar poly_id)) spec_ty const_dicts inl) }
        -- Most of the work of specialisation is done by 
        -- the desugarer, guided by the SpecPrag
   
@@ -546,7 +526,7 @@ tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf,
        ; let mono_id = mkLocalId mono_name zonked_rhs_ty
        ; return (unitBag (L b_loc (FunBind { fun_id = L nm_loc mono_id, fun_infix = inf,
                                              fun_matches = matches', bind_fvs = fvs,
-                                             fun_co_fn = co_fn })),
+                                             fun_co_fn = co_fn, fun_tick = Nothing })),
                  [(name, Nothing, mono_id)]) }
 
 tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf, 
@@ -570,7 +550,8 @@ tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf,
 
        ; let fun_bind' = FunBind { fun_id = L nm_loc mono_id, 
                                    fun_infix = inf, fun_matches = matches',
-                                   bind_fvs = placeHolderNames, fun_co_fn = co_fn }
+                                   bind_fvs = placeHolderNames, fun_co_fn = co_fn, 
+                                   fun_tick = Nothing }
        ; return (unitBag (L b_loc fun_bind'),
                  [(name, Just tc_sig, mono_id)]) }
 
@@ -675,7 +656,8 @@ tcRhs (TcFunBind info fun'@(L _ mono_id) inf matches)
   = do { (co_fn, matches') <- tcMatchesFun (idName mono_id) matches 
                                            (idType mono_id)
        ; return (FunBind { fun_id = fun', fun_infix = inf, fun_matches = matches',
-                           bind_fvs = placeHolderNames, fun_co_fn = co_fn }) }
+                           bind_fvs = placeHolderNames, fun_co_fn = co_fn,
+                           fun_tick = Nothing }) }
 
 tcRhs bind@(TcPatBind _ pat' grhss pat_ty)
   = do { grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
@@ -728,16 +710,17 @@ generalise dflags top_lvl bind_list sig_fn mono_infos lie_req
   = tcSimplifyInfer doc tau_tvs lie_req
 
   | otherwise  -- UNRESTRICTED CASE, WITH TYPE SIGS
-  = do { sig_lie <- unifyCtxts sigs    -- sigs is non-empty
+  = do { sig_lie <- unifyCtxts sigs    -- sigs is non-empty; sig_lie is zonked
        ; let   -- The "sig_avails" is the stuff available.  We get that from
                -- the context of the type signature, BUT ALSO the lie_avail
                -- so that polymorphic recursion works right (see Note [Polymorphic recursion])
                local_meths = [mkMethInst sig mono_id | (_, Just sig, mono_id) <- mono_infos]
                sig_avails = sig_lie ++ local_meths
+               loc = sig_loc (head sigs)
 
        -- Check that the needed dicts can be
        -- expressed in terms of the signature ones
-       ; (forall_tvs, dict_binds) <- tcSimplifyInferCheck doc tau_tvs sig_avails lie_req
+       ; (forall_tvs, dict_binds) <- tcSimplifyInferCheck loc tau_tvs sig_avails lie_req
        
        -- Check that signature type variables are OK
        ; final_qtvs <- checkSigsTyVars forall_tvs sigs
@@ -754,7 +737,8 @@ generalise dflags top_lvl bind_list sig_fn mono_infos lie_req
 
     mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, 
                            sig_theta = theta, sig_loc = loc }) mono_id
-      = Method mono_id poly_id (mkTyVarTys tvs) theta loc
+      = Method {tci_id = mono_id, tci_oid = poly_id, tci_tys = mkTyVarTys tvs,
+               tci_theta = theta, tci_loc = loc}
 \end{code}
 
 unifyCtxts checks that all the signature contexts are the same
@@ -771,14 +755,16 @@ might not otherwise be related.  This is a rather subtle issue.
 
 \begin{code}
 unifyCtxts :: [TcSigInfo] -> TcM [Inst]
+-- Post-condition: the returned Insts are full zonked
 unifyCtxts (sig1 : sigs)       -- Argument is always non-empty
   = do { mapM unify_ctxt sigs
-       ; newDictBndrs (sig_loc sig1) (sig_theta sig1) }
+       ; theta <- zonkTcThetaType (sig_theta sig1)
+       ; newDictBndrs (sig_loc sig1) theta }
   where
     theta1 = sig_theta sig1
     unify_ctxt :: TcSigInfo -> TcM ()
     unify_ctxt sig@(TcSigInfo { sig_theta = theta })
-       = setSrcSpan (instLocSrcSpan (sig_loc sig))     $
+       = setSrcSpan (instLocSpan (sig_loc sig))        $
          addErrCtxt (sigContextsCtxt sig1 sig)         $
          unifyTheta theta1 theta
 
@@ -973,13 +959,12 @@ mkTcSigFun :: [LSig Name] -> TcSigFun
 -- Precondition: no duplicates
 mkTcSigFun sigs = lookupNameEnv env
   where
-    env = mkNameEnv [(name, scoped_tyvars hs_ty)
-                   | L span (TypeSig (L _ name) (L _ hs_ty)) <- sigs]
-    scoped_tyvars (HsForAllTy Explicit tvs _ _) = hsLTyVarNames tvs
-    scoped_tyvars other                                = []
+    env = mkNameEnv [(name, hsExplicitTvs lhs_ty)
+                   | L span (TypeSig (L _ name) lhs_ty) <- sigs]
        -- The scoped names are the ones explicitly mentioned
        -- in the HsForAll.  (There may be more in sigma_ty, because
        -- of nested type synonyms.  See Note [Scoped] with TcSigInfo.)
+       -- See Note [Only scoped tyvars are in the TyVarEnv]
 
 ---------------
 data TcSigInfo
@@ -998,6 +983,19 @@ data TcSigInfo
        sig_loc    :: InstLoc           -- The location of the signature
     }
 
+
+--     Note [Only scoped tyvars are in the TyVarEnv]
+-- We are careful to keep only the *lexically scoped* type variables in
+-- the type environment.  Why?  After all, the renamer has ensured
+-- that only legal occurrences occur, so we could put all type variables
+-- into the type env.
+--
+-- But we want to check that two distinct lexically scoped type variables
+-- do not map to the same internal type variable.  So we need to know which
+-- the lexically-scoped ones are... and at the moment we do that by putting
+-- only the lexically scoped ones into the environment.
+
+
 --     Note [Scoped]
 -- There may be more instantiated type variables than scoped 
 -- ones.  For example:
@@ -1010,7 +1008,7 @@ data TcSigInfo
 -- and remember the names from the original HsForAllTy in sig_scoped
 
 --     Note [Instantiate sig]
--- It's vital to instantiate a type signature with fresh variable.
+-- It's vital to instantiate a type signature with fresh variables.
 -- For example:
 --     type S = forall a. a->a
 --     f,g :: S
@@ -1046,7 +1044,7 @@ tcInstSig :: Bool -> Name -> [Name] -> TcM TcSigInfo
 -- Instantiate the signature, with either skolems or meta-type variables
 -- depending on the use_skols boolean.  This variable is set True
 -- when we are typechecking a single function binding; and False for
--- pattern bindigs and a group of several function bindings.
+-- pattern bindings and a group of several function bindings.
 -- Reason: in the latter cases, the "skolems" can be unified together, 
 --        so they aren't properly rigid in the type-refinement sense.
 -- NB: unless we are doing H98, each function with a sig will be done
@@ -1065,8 +1063,7 @@ tcInstSig use_skols name scoped_names
   = do { poly_id <- tcLookupId name    -- Cannot fail; the poly ids are put into 
                                        -- scope when starting the binding group
        ; let skol_info = SigSkol (FunSigCtxt name)
-             inst_tyvars | use_skols = tcInstSkolTyVars skol_info
-                         | otherwise = tcInstSigTyVars  skol_info
+             inst_tyvars = tcInstSigTyVars use_skols skol_info
        ; (tvs, theta, tau) <- tcInstType inst_tyvars (idType poly_id)
        ; loc <- getInstLoc (SigOrigin skol_info)
        ; return (TcSigInfo { sig_id = poly_id,