[project @ 2001-12-21 10:05:11 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMatches.lhs
index f0ab170..fbc20af 100644 (file)
@@ -17,30 +17,30 @@ import HsSyn                ( HsBinds(..), Match(..), GRHSs(..), GRHS(..),
                          pprMatch, getMatchLoc, pprMatchContext, isDoExpr,
                          mkMonoBind, nullMonoBinds, collectSigTysFromPats
                        )
-import RnHsSyn         ( RenamedMatch, RenamedGRHSs, RenamedStmt, RenamedPat, RenamedHsType,
-                         RenamedMatchContext, extractHsTyVars )
+import RnHsSyn         ( RenamedMatch, RenamedGRHSs, RenamedStmt, RenamedPat, RenamedMatchContext )
 import TcHsSyn         ( TcMatch, TcGRHSs, TcStmt, TcDictBinds, TypecheckedPat )
 
 import TcMonad
-import TcMonoType      ( kcHsSigTypes, tcScopedTyVars, checkSigTyVars, tcHsSigType, UserTypeCtxt(..), sigPatCtxt )
+import TcMonoType      ( tcAddScopedTyVars, tcHsSigType, UserTypeCtxt(..) )
 import Inst            ( LIE, isEmptyLIE, plusLIE, emptyLIE, plusLIEs, lieToList )
-import TcEnv           ( TcId, tcLookupLocalIds, tcExtendLocalValEnv, tcExtendGlobalTyVars,
-                         tcInLocalScope )
+import TcEnv           ( TcId, tcLookupLocalIds, tcExtendLocalValEnv, tcExtendGlobalTyVars )
 import TcPat           ( tcPat, tcMonoPatBndr, polyPatSig )
-import TcMType         ( newTyVarTy, unifyFunTy, unifyTauTy )
-import TcType          ( tyVarsOfType, isTauTy,  mkFunTy, isOverloadedTy,
-                         liftedTypeKind, openTypeKind  )
+import TcMType         ( newTyVarTy )
+import TcType          ( TcType, TcTyVar, tyVarsOfType, isTauTy,  
+                         mkFunTy, isOverloadedTy, liftedTypeKind, openTypeKind  )
 import TcBinds         ( tcBindsAndThen )
+import TcUnify         ( subFunTy, unifyTauTy, checkSigTyVars, sigPatCtxt )
 import TcSimplify      ( tcSimplifyCheck, bindInstsOfLocalFuns )
 import Name            ( Name )
 import TysWiredIn      ( boolTy )
 import Id              ( idType )
 import BasicTypes      ( RecFlag(..) )
-import NameSet
 import VarSet
 import Var             ( Id )
 import Bag
+import Util            ( isSingleton )
 import Outputable
+
 import List            ( nub )
 \end{code}
 
@@ -78,7 +78,7 @@ tcMatchesFun xve fun_name expected_ty matches@(first_match:_)
        -- because inconsistency between branches
        -- may show up as something wrong with the (non-existent) type signature
 
-       -- No need to zonk expected_ty, because unifyFunTy does that on the fly
+       -- No need to zonk expected_ty, because subFunTy does that on the fly
     tcMatches xve (FunRhs fun_name) matches expected_ty
 \end{code}
 
@@ -127,42 +127,46 @@ tcMatches xve fun_or_case matches expected_ty
 tcMatch :: [(Name,Id)]
        -> RenamedMatchContext
        -> RenamedMatch
-       -> TcType               -- Expected result-type of the Match.
-                               -- Early unification with this guy gives better error messages
+       -> TcType       -- Expected result-type of the Match.
+                       -- Early unification with this guy gives better error messages
+                       -- We regard the Match as having type 
+                       --      (ty1 -> ... -> tyn -> result_ty)
+                       -- where there are n patterns.
        -> TcM (TcMatch, LIE)
 
-tcMatch xve1 ctxt match@(Match sig_tvs pats maybe_rhs_sig grhss) expected_ty
+tcMatch xve1 ctxt match@(Match pats maybe_rhs_sig grhss) expected_ty
   = tcAddSrcLoc (getMatchLoc match)            $       -- At one stage I removed this;
     tcAddErrCtxt (matchCtxt ctxt match)                $       -- I'm not sure why, so I put it back
     
     tcMatchPats pats expected_ty tc_grhss      `thenTc` \ ((pats', grhss'), lie, ex_binds) ->
-    returnTc (Match [] pats' Nothing (glue_on Recursive ex_binds grhss'), lie)
+    returnTc (Match pats' Nothing (glue_on Recursive ex_binds grhss'), lie)
 
   where
     tc_grhss pats' rhs_ty 
        =       -- Check that the remaining "expected type" is not a rank-2 type
                -- If it is it'll mess up the unifier when checking the RHS
-         checkTc (isTauTy rhs_ty) lurkingRank2SigErr           `thenTc_`
+         checkTc (isTauTy rhs_ty) lurkingRank2SigErr   `thenTc` \_ -> 
 
                -- Deal with the result signature
-         tc_result_sig maybe_rhs_sig   ( 
+               -- It "wraps" the rest of the body typecheck because it may
+               -- bring into scope the type variables in the signature
+         tc_result_sig maybe_rhs_sig rhs_ty            $
 
                -- Typecheck the body
-               tcExtendLocalValEnv xve1        $
-               tcGRHSs ctxt grhss rhs_ty       `thenTc` \ (grhss', lie) ->
-               returnTc ((pats', grhss'), lie)
-         )
+         tcExtendLocalValEnv xve1                      $
+         tcGRHSs ctxt grhss rhs_ty                     `thenTc` \ (grhss', lie) ->
+         returnTc ((pats', grhss'), lie)
 
-    tc_result_sig Nothing thing_inside
+    tc_result_sig Nothing rhs_ty thing_inside
        = thing_inside
-    tc_result_sig (Just sig) thing_inside
+    tc_result_sig (Just sig) rhs_ty thing_inside
        = tcAddScopedTyVars [sig]                       $
          tcHsSigType ResSigCtxt sig                    `thenTc` \ sig_ty ->
 
                -- Check that the signature isn't a polymorphic one, which
                -- we don't permit (at present, anyway)
          checkTc (isTauTy sig_ty) (polyPatSig sig_ty)  `thenTc_`
-         unifyTauTy expected_ty sig_ty                 `thenTc_`
+         unifyTauTy sig_ty rhs_ty                      `thenTc_`
          thing_inside
 
 
@@ -207,54 +211,44 @@ tcMatchPats
 
 tcMatchPats pats expected_ty thing_inside
   =    -- STEP 1: Bring pattern-signature type variables into scope
-    tcAddScopedTyVars (collectSigTysFromPats pats)                     $
+    tcAddScopedTyVars (collectSigTysFromPats pats)     (
 
        -- STEP 2: Typecheck the patterns themselves, gathering all the stuff
-    tc_match_pats pats expected_ty     `thenTc` \ (rhs_ty, pats', lie_req1, ex_tvs, pat_bndrs, lie_avail) ->
+        tc_match_pats pats expected_ty `thenTc` \ (rhs_ty, pats', lie_req1, ex_tvs, pat_bndrs, lie_avail) ->
     
        -- STEP 3: Extend the environment, and do the thing inside
-    let
+       let
          xve     = bagToList pat_bndrs
          pat_ids = map snd xve
-    in
-    tcExtendLocalValEnv xve (thing_inside pats' rhs_ty)                `thenTc` \ (result, lie_req2) ->
+       in
+       tcExtendLocalValEnv xve (thing_inside pats' rhs_ty)             `thenTc` \ (result, lie_req2) ->
+
+       returnTc (rhs_ty, lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2)
+    ) `thenTc` \ (rhs_ty, lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2) -> 
 
        -- STEP 4: Check for existentially bound type variables
+       -- Do this *outside* the scope of the tcAddScopedTyVars, else checkSigTyVars
+       -- complains that 'a' is captured by the inscope 'a'!  (Test (d) in checkSigTyVars.)
+       --
        -- I'm a bit concerned that lie_req1 from an 'inner' pattern in the list
        -- might need (via lie_req2) something made available from an 'outer' 
        -- pattern.  But it's inconvenient to deal with, and I can't find an example
-    tcCheckExistentialPat pat_ids ex_tvs lie_avail lie_req2 rhs_ty     `thenTc` \ (lie_req2', ex_binds) ->
+    tcCheckExistentialPat pat_ids ex_tvs lie_avail lie_req2 expected_ty        `thenTc` \ (lie_req2', ex_binds) ->
+       -- NB: we *must* pass "expected_ty" not "result_ty" to tcCheckExistentialPat
+       -- For example, we must reject this program:
+       --      data C = forall a. C (a -> Int) 
+       --      f (C g) x = g x
+       -- Here, result_ty will be simply Int, but expected_ty is (a -> Int).
 
     returnTc (result, lie_req1 `plusLIE` lie_req2', ex_binds)
 
-tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
--- Find the not-already-in-scope signature type variables,
--- kind-check them, and bring them into scope
---
--- We no longer specify that these type variables must be univerally 
--- quantified (lots of email on the subject).  If you want to put that 
--- back in, you need to
---     a) Do a checkSigTyVars after thing_inside
---     b) More insidiously, don't pass in expected_ty, else
---        we unify with it too early and checkSigTyVars barfs
---        Instead you have to pass in a fresh ty var, and unify
---        it with expected_ty afterwards
-tcAddScopedTyVars sig_tys thing_inside
-  = tcGetEnv                                   `thenNF_Tc` \ env ->
-    let
-       all_sig_tvs = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
-       sig_tvs = filter not_in_scope (nameSetToList all_sig_tvs)
-       not_in_scope tv = not (tcInLocalScope env tv)
-    in       
-    tcScopedTyVars sig_tvs (kcHsSigTypes sig_tys) thing_inside
-
 tcCheckExistentialPat :: [TcId]                -- Ids bound by this pattern
                      -> Bag TcTyVar    -- Existentially quantified tyvars bound by pattern
                      -> LIE            --   and context
                      -> LIE            -- Required context
-                     -> TcType         --   and result type; vars in here must not escape
+                     -> TcType         --   and type of the Match; vars in here must not escape
                      -> TcM (LIE, TcDictBinds) -- LIE to float out and dict bindings
-tcCheckExistentialPat ids ex_tvs lie_avail lie_req result_ty
+tcCheckExistentialPat ids ex_tvs lie_avail lie_req match_ty
   | isEmptyBag ex_tvs && all not_overloaded ids
        -- Short cut for case when there are no existentials
        -- and no polymorphic overloaded variables
@@ -265,7 +259,7 @@ tcCheckExistentialPat ids ex_tvs lie_avail lie_req result_ty
     returnTc (lie_req, EmptyMonoBinds)
 
   | otherwise
-  = tcExtendGlobalTyVars (tyVarsOfType result_ty)              $
+  = tcExtendGlobalTyVars (tyVarsOfType match_ty)               $
     tcAddErrCtxtM (sigPatCtxt tv_list ids)                     $
 
        -- In case there are any polymorpic, overloaded binders in the pattern
@@ -274,8 +268,7 @@ tcCheckExistentialPat ids ex_tvs lie_avail lie_req result_ty
     bindInstsOfLocalFuns lie_req ids                           `thenTc` \ (lie1, inst_binds) ->
 
        -- Deal with overloaded functions bound by the pattern
-    tcSimplifyCheck doc tv_list
-                   (lieToList lie_avail) lie1          `thenTc` \ (lie2, dict_binds) ->
+    tcSimplifyCheck doc tv_list (lieToList lie_avail) lie1     `thenTc` \ (lie2, dict_binds) ->
     checkSigTyVars tv_list emptyVarSet                         `thenTc_` 
 
     returnTc (lie2, dict_binds `AndMonoBinds` inst_binds)
@@ -288,7 +281,10 @@ tc_match_pats [] expected_ty
   = returnTc (expected_ty, [], emptyLIE, emptyBag, emptyBag, emptyLIE)
 
 tc_match_pats (pat:pats) expected_ty
-  = unifyFunTy expected_ty             `thenTc` \ (arg_ty, rest_ty) ->
+  = subFunTy expected_ty               `thenTc` \ (arg_ty, rest_ty) ->
+       -- This is the unique place we call subFunTy
+       -- The point is that if expected_y is a "hole", we want 
+       -- to make arg_ty and rest_ty as "holes" too.
     tcPat tcMonoPatBndr pat arg_ty     `thenTc` \ (pat', lie_req, pat_tvs, pat_ids, lie_avail) ->
     tc_match_pats pats rest_ty         `thenTc` \ (rhs_ty, pats', lie_reqs, pats_tvs, pats_ids, lie_avails) ->
     returnTc ( rhs_ty, 
@@ -443,10 +439,10 @@ number of args are used in each equation.
 
 \begin{code}
 sameNoOfArgs :: [RenamedMatch] -> Bool
-sameNoOfArgs matches = length (nub (map args_in_match matches)) == 1
+sameNoOfArgs matches = isSingleton (nub (map args_in_match matches))
   where
     args_in_match :: RenamedMatch -> Int
-    args_in_match (Match _ pats _ _) = length pats
+    args_in_match (Match pats _ _) = length pats
 \end{code}
 
 \begin{code}