- -> [LPat Name]
- -> [Expected TcSigmaType] -- Excess types discarded
- -> TcM a
- -> TcM ([LPat TcId], [TcTyVar], a)
-
-tcPats ctxt [] _ thing_inside
- = do { res <- thing_inside
- ; return ([], [], res) }
-
-tcPats ctxt (p:ps) (ty:tys) thing_inside
- = do { (p', p_tvs, (ps', ps_tvs, res))
- <- tcPat ctxt p ty $
- tcPats ctxt ps tys thing_inside
- ; return (p':ps', p_tvs ++ ps_tvs, res) }
-
---------------------
-tcCheckPats :: PatCtxt
- -> [LPat Name] -> [TcSigmaType]
- -> TcM a
- -> TcM ([LPat TcId], [TcTyVar], a)
-tcCheckPats ctxt pats tys thing_inside -- A trivial wrapper
- = tcPats ctxt pats (map Check tys) thing_inside
+ -> [LPat Name] -- Patterns,
+ -> [BoxySigmaType] -- and their types
+ -> BoxyRhoType -- Result type,
+ -> (BoxyRhoType -> TcM a) -- and the checker for the body
+ -> TcM ([LPat TcId], a)
+
+-- This is the externally-callable wrapper function
+-- Typecheck the patterns, extend the environment to bind the variables,
+-- do the thing inside, use any existentially-bound dictionaries to
+-- discharge parts of the returning LIE, and deal with pattern type
+-- signatures
+
+-- 1. Initialise the PatState
+-- 2. Check the patterns
+-- 3. Apply the refinement
+-- 4. Check the body
+-- 5. Check that no existentials escape
+
+tcPats ctxt pats tys res_ty thing_inside
+ = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst }
+
+ ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' ->
+ refineEnvironment (pat_reft pstate') $
+ thing_inside (refineType (pat_reft pstate') res_ty)
+
+ ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty
+
+ ; returnM (pats', res) }
+
+
+-----------------
+tcPat :: PatCtxt
+ -> LPat Name -> TcType
+ -> BoxyRhoType -- Result type
+ -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
+ -> TcM (LPat TcId, a)
+tcPat ctxt pat pat_ty res_ty thing_inside
+ = do { ([pat'],thing) <- tcPats ctxt [pat] [pat_ty] res_ty thing_inside
+ ; return (pat', thing) }
+
+
+-----------------
+tcCheckExistentialPat :: PatCtxt
+ -> [LPat TcId] -- Patterns (just for error message)
+ -> [TcTyVar] -- Existentially quantified tyvars bound by pattern
+ -> [BoxySigmaType] -- Types of the patterns
+ -> BoxyRhoType -- Type of the body of the match
+ -- Tyvars in either of these must not escape
+ -> TcM ()
+-- NB: we *must* pass "pats_tys" not just "body_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 (C -> a -> Int).
+
+tcCheckExistentialPat ctxt pats [] pat_tys body_ty
+ = return () -- Short cut for case when there are no existentials
+
+tcCheckExistentialPat (LetPat _) pats ex_tvs pat_tys body_ty
+ -- Don't know how to deal with pattern-bound existentials yet
+ = failWithTc (existentialExplode pats)
+
+tcCheckExistentialPat ctxt pats ex_tvs pat_tys body_ty
+ = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys) $
+ checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
+
+data PatState = PS {
+ pat_ctxt :: PatCtxt,
+ pat_reft :: GadtRefinement -- Binds rigid TcTyVars to their refinements
+ }
+
+data PatCtxt
+ = LamPat
+ | LetPat (Name -> Maybe TcRhoType) -- Used for let(rec) bindings
+
+patSigCtxt :: PatState -> UserTypeCtxt
+patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
+patSigCtxt other = LamPatSigCtxt