do { ((exp_ty1, res_ty), coi) <- boxySplitAppTy exp_ty
; ((arr_ty, arg_ty), coi1) <- boxySplitAppTy exp_ty1
; let cmd_env = CmdEnv { cmd_arr = arr_ty }
- ; (pat', cmd') <- tcProcPat pat arg_ty (emptyRefinement, res_ty) $
+ ; (pat', cmd') <- tcProcPat pat arg_ty res_ty $
tcCmdTop cmd_env cmd []
; let res_coi = mkTransCoI coi (mkAppTyCoI exp_ty1 coi1 res_ty IdCo)
; return (pat', cmd', res_coi)
tcCmdTop :: CmdEnv
-> LHsCmdTop Name
-> CmdStack
- -> (Refinement, TcTauType) -- Expected result type; always a monotype
- -- We know exactly how many cmd args are expected,
- -- albeit perhaps not their types; so we can pass
- -- in a CmdStack
+ -> TcTauType -- Expected result type; always a monotype
+ -- We know exactly how many cmd args are expected,
+ -- albeit perhaps not their types; so we can pass
+ -- in a CmdStack
-> TcM (LHsCmdTop TcId)
-tcCmdTop env (L loc (HsCmdTop cmd _ _ names)) cmd_stk reft_res_ty@(_,res_ty)
+tcCmdTop env (L loc (HsCmdTop cmd _ _ names)) cmd_stk res_ty
= setSrcSpan loc $
- do { cmd' <- tcGuardedCmd env cmd cmd_stk reft_res_ty
+ do { cmd' <- tcGuardedCmd env cmd cmd_stk res_ty
; names' <- mapM (tcSyntaxName ProcOrigin (cmd_arr env)) names
; return (L loc $ HsCmdTop cmd' cmd_stk res_ty names') }
----------------------------------------
tcGuardedCmd :: CmdEnv -> LHsExpr Name -> CmdStack
- -> (Refinement, TcTauType) -> TcM (LHsExpr TcId)
+ -> TcTauType -> TcM (LHsExpr TcId)
-- A wrapper that deals with the refinement (if any)
-tcGuardedCmd env expr stk (reft, res_ty)
- = do { let (co, res_ty') = refineResType reft res_ty
- ; body <- tcCmd env expr (stk, res_ty')
- ; return (mkLHsWrap co body) }
+tcGuardedCmd env expr stk res_ty
+ = do { body <- tcCmd env expr (stk, res_ty)
+ ; return body
+ }
tcCmd :: CmdEnv -> LHsExpr Name -> (CmdStack, TcTauType) -> TcM (LHsExpr TcId)
-- The main recursive function
tc_cmd env cmd@(HsDo do_or_lc stmts body ty) (cmd_stk, res_ty)
= do { checkTc (null cmd_stk) (nonEmptyCmdStkErr cmd)
- ; (stmts', body') <- tcStmts do_or_lc tc_stmt stmts (emptyRefinement, res_ty) $
+ ; (stmts', body') <- tcStmts do_or_lc tc_stmt stmts res_ty $
tcGuardedCmd env body []
; return (HsDo do_or_lc stmts' body' res_ty) }
where
not (w_tv `elemVarSet` tyVarsOfTypes arg_tys))
(badFormFun i tup_ty')
- ; tcCmdTop (env { cmd_arr = b }) cmd arg_tys (emptyRefinement, s) }
+ ; tcCmdTop (env { cmd_arr = b }) cmd arg_tys s }
unscramble :: TcType -> (TcType, [TcType])
-- unscramble ((w,s1) .. sn) = (w, [s1..sn])
\begin{code}
tcGRHSsPat :: GRHSs Name -> BoxyRhoType -> TcM (GRHSs TcId)
-- Used for pattern bindings
-tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss (emptyRefinement, res_ty)
- -- emptyRefinement: no refinement in a pattern binding
+tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss res_ty
where
match_ctxt = MC { mc_what = PatBindRhs,
mc_body = tcBody }
data TcMatchCtxt -- c.f. TcStmtCtxt, also in this module
= MC { mc_what :: HsMatchContext Name, -- What kind of thing this is
- mc_body :: LHsExpr Name -- Type checker for a body of an alternative
- -> (Refinement, BoxyRhoType)
+ mc_body :: LHsExpr Name -- Type checker for a body of
+ -- an alternative
+ -> BoxyRhoType
-> TcM (LHsExpr TcId) }
tcMatches ctxt pat_tys rhs_ty (MatchGroup matches _)
= tcGRHSs ctxt grhss rhs_ty -- No result signature
-- Result type sigs are no longer supported
- tc_grhss ctxt (Just res_sig) grhss (co, rhs_ty)
+ tc_grhss ctxt (Just res_sig) grhss rhs_ty
= do { addErr (ptext SLIT("Ignoring (deprecated) result type signature")
<+> ppr res_sig)
- ; tcGRHSs ctxt grhss (co, rhs_ty) }
+ ; tcGRHSs ctxt grhss rhs_ty }
-- For (\x -> e), tcExpr has already said "In the expresssion \x->e"
-- so we don't want to add "In the lambda abstraction \x->e"
m_ctxt -> addErrCtxt (matchCtxt m_ctxt match) thing_inside
-------------
-tcGRHSs :: TcMatchCtxt -> GRHSs Name -> (Refinement, BoxyRhoType)
+tcGRHSs :: TcMatchCtxt -> GRHSs Name -> BoxyRhoType
-> TcM (GRHSs TcId)
-- Notice that we pass in the full res_ty, so that we get
; return (GRHSs grhss' binds') }
-------------
-tcGRHS :: TcMatchCtxt -> (Refinement, BoxyRhoType) -> GRHS Name -> TcM (GRHS TcId)
+tcGRHS :: TcMatchCtxt -> BoxyRhoType -> GRHS Name -> TcM (GRHS TcId)
tcGRHS ctxt res_ty (GRHS guards rhs)
= do { (guards', rhs') <- tcStmts stmt_ctxt tcGuardStmt guards res_ty $
tcDoStmts ListComp stmts body res_ty
= do { (elt_ty, coi) <- boxySplitListTy res_ty
; (stmts', body') <- tcStmts ListComp (tcLcStmt listTyCon) stmts
- (emptyRefinement,elt_ty) $
+ elt_ty $
tcBody body
; return $ mkHsWrapCoI coi
(HsDo ListComp stmts' body' (mkListTy elt_ty)) }
tcDoStmts PArrComp stmts body res_ty
= do { (elt_ty, coi) <- boxySplitPArrTy res_ty
; (stmts', body') <- tcStmts PArrComp (tcLcStmt parrTyCon) stmts
- (emptyRefinement, elt_ty) $
+ elt_ty $
tcBody body
; return $ mkHsWrapCoI coi
(HsDo PArrComp stmts' body' (mkPArrTy elt_ty)) }
tcDoStmts DoExpr stmts body res_ty
= do { (stmts', body') <- tcStmts DoExpr tcDoStmt stmts
- (emptyRefinement, res_ty) $
+ res_ty $
tcBody body
; return (HsDo DoExpr stmts' body' res_ty) }
tcMonoExpr rhs (mkAppTy m_ty pat_ty)
; (stmts', body') <- tcStmts ctxt (tcMDoStmt tc_rhs) stmts
- (emptyRefinement, res_ty') $
+ res_ty' $
tcBody body
; let names = [mfixName, bindMName, thenMName, returnMName, failMName]
tcDoStmts ctxt stmts body res_ty = pprPanic "tcDoStmts" (pprStmtContext ctxt)
-tcBody :: LHsExpr Name -> (Refinement, BoxyRhoType) -> TcM (LHsExpr TcId)
-tcBody body (reft, res_ty)
- = do { traceTc (text "tcBody" <+> ppr res_ty <+> ppr reft)
- ; let (co, res_ty') = refineResType reft res_ty
- ; body' <- tcPolyExpr body res_ty'
- ; return (mkLHsWrap co body') }
+tcBody :: LHsExpr Name -> BoxyRhoType -> TcM (LHsExpr TcId)
+tcBody body res_ty
+ = do { traceTc (text "tcBody" <+> ppr res_ty)
+ ; body' <- tcPolyExpr body res_ty
+ ; return body'
+ }
\end{code}
type TcStmtChecker
= forall thing. HsStmtContext Name
-> Stmt Name
- -> (Refinement, BoxyRhoType) -- Result type for comprehension
- -> ((Refinement,BoxyRhoType) -> TcM thing) -- Checker for what follows the stmt
+ -> BoxyRhoType -- Result type for comprehension
+ -> (BoxyRhoType -> TcM thing) -- Checker for what follows the stmt
-> TcM (Stmt TcId, thing)
- -- The incoming BoxyRhoType may be refined by type refinements
- -- before being passed to the thing_inside
-
tcStmts :: HsStmtContext Name
-> TcStmtChecker -- NB: higher-rank type
-> [LStmt Name]
- -> (Refinement, BoxyRhoType)
- -> ((Refinement, BoxyRhoType) -> TcM thing)
+ -> BoxyRhoType
+ -> (BoxyRhoType -> TcM thing)
-> TcM ([LStmt TcId], thing)
-- Note the higher-rank type. stmt_chk is applied at different
; return (ParStmt pairs', thing) }
where
-- loop :: [([LStmt Name], [Name])] -> TcM ([([LStmt TcId], [TcId])], thing)
- loop [] = do { thing <- thing_inside elt_ty -- No refinement from pattern
+ loop [] = do { thing <- thing_inside elt_ty
; return ([], thing) } -- matching in the branches
loop ((stmts, names) : pairs)
tcDoStmt :: TcStmtChecker
-tcDoStmt ctxt (BindStmt pat rhs bind_op fail_op) (reft,res_ty) thing_inside
+tcDoStmt ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
= do { (rhs', rhs_ty) <- tcInferRho rhs
- -- We should use type *inference* for the RHS computations, becuase of GADTs.
+ -- We should use type *inference* for the RHS computations,
+ -- becuase of GADTs.
-- do { pat <- rhs; <rest> }
-- is rather like
-- case rhs of { pat -> <rest> }
- -- We do inference on rhs, so that information about its type can be refined
- -- when type-checking the pattern.
+ -- We do inference on rhs, so that information about its type
+ -- can be refined when type-checking the pattern.
-- Deal with rebindable syntax:
-- (>>=) :: rhs_ty -> (pat_ty -> new_res_ty) -> res_ty
then return noSyntaxExpr
else tcSyntaxOp DoOrigin fail_op (mkFunTy stringTy new_res_ty)
- ; (pat', thing) <- tcLamPat pat pat_ty (reft, new_res_ty) thing_inside
+ ; (pat', thing) <- tcLamPat pat pat_ty new_res_ty thing_inside
; return (BindStmt pat' rhs' bind_op' fail_op', thing) }
-tcDoStmt ctxt (ExprStmt rhs then_op _) (reft,res_ty) thing_inside
+tcDoStmt ctxt (ExprStmt rhs then_op _) res_ty thing_inside
= do { (rhs', rhs_ty) <- tcInferRho rhs
-- Deal with rebindable syntax; (>>) :: rhs_ty -> new_res_ty -> res_ty
tcSyntaxOp DoOrigin then_op
(mkFunTys [rhs_ty, new_res_ty] res_ty)
- ; thing <- thing_inside (reft, new_res_ty)
+ ; thing <- thing_inside new_res_ty
; return (ExprStmt rhs' then_op' rhs_ty, thing) }
tcDoStmt ctxt (RecStmt {}) res_ty thing_inside
-> TcM a
-> TcM (LPat TcId, a)
tcLetPat sig_fn pat pat_ty thing_inside
- = do { let init_state = PS { pat_ctxt = LetPat sig_fn,
- pat_reft = emptyRefinement,
+ = do { let init_state = PS { pat_ctxt = LetPat sig_fn,
pat_eqs = False }
- ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
+ ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state
+ (\ _ -> thing_inside)
-- Don't know how to deal with pattern-bound existentials yet
; checkTc (null ex_tvs) (existentialExplode pat)
; return (pat', res) }
-----------------
-tcLamPats :: [LPat Name] -- Patterns,
- -> [BoxySigmaType] -- and their types
- -> BoxyRhoType -- Result type,
- -> ((Refinement, BoxyRhoType) -> TcM a) -- and the checker for the body
+tcLamPats :: [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
-- 1. Initialise the PatState
-- 2. Check the patterns
--- 3. Apply the refinement to the environment and result type
--- 4. Check the body
--- 5. Check that no existentials escape
+-- 3. Check the body
+-- 4. Check that no existentials escape
tcLamPats pats tys res_ty thing_inside
= tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys)
- (emptyRefinement, res_ty) thing_inside
+ res_ty thing_inside
tcLamPat :: LPat Name -> BoxySigmaType
- -> (Refinement,BoxyRhoType) -- Result type
- -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
+ -> BoxyRhoType -- Result type
+ -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
-> TcM (LPat TcId, a)
tcProcPat = tc_lam_pat ProcPat
-----------------
tc_lam_pats :: PatCtxt
-> [(LPat Name,BoxySigmaType)]
- -> (Refinement,BoxyRhoType) -- Result type
- -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
+ -> BoxyRhoType -- Result type
+ -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
-> TcM ([LPat TcId], a)
-tc_lam_pats ctxt pat_ty_prs (reft, res_ty) thing_inside
- = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = reft, pat_eqs = False }
+tc_lam_pats ctxt pat_ty_prs res_ty thing_inside
+ = do { let init_state = PS { pat_ctxt = ctxt, pat_eqs = False }
; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
- refineEnvironment (pat_reft pstate') (pat_eqs pstate') $
if (pat_eqs pstate' && (not $ isRigidTy res_ty))
then failWithTc (nonRigidResult res_ty)
- else thing_inside (pat_reft pstate', res_ty)
+ else thing_inside res_ty
; let tys = map snd pat_ty_prs
; tcCheckExistentialPat pats' ex_tvs tys res_ty
data PatState = PS {
pat_ctxt :: PatCtxt,
- pat_reft :: Refinement, -- Binds rigid TcTyVars to their refinements
pat_eqs :: Bool -- <=> there are GADT equational constraints
-- for refinement
}
tc_lpat (L span pat) pat_ty pstate thing_inside
= setSrcSpan span $
maybeAddErrCtxt (patCtxt pat) $
- do { let mb_reft = refineType (pat_reft pstate) pat_ty
- pat_ty' = case mb_reft of { Just (_, ty') -> ty'; Nothing -> pat_ty }
-
- -- Make sure the result type reflects the current refinement
- -- We must do this here, so that it correctly ``sees'' all
- -- the refinements to the left. Example:
- -- Suppose C :: forall a. T a -> a -> Foo
- -- Pattern C a p1 True
- -- So p1 might refine 'a' to True, and the True
- -- pattern had better see it.
-
- ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
- ; let final_pat = case mb_reft of
- Nothing -> pat'
- Just (co,_) -> CoPat (WpCo co) pat' pat_ty
- ; return (L span final_pat, tvs, res) }
+ do { (pat', tvs, res) <- tc_pat pstate pat pat_ty thing_inside
+ ; return (L span pat', tvs, res) }
--------------------
tc_pat :: PatState
from the family to the representation type. This is achieved by
unwrapFamInstScrutinee using a CoPat around the result pattern.
-Now it might appear seem as if we could have used the existing GADT type
+Now it might appear seem as if we could have used the previous GADT type
refinement infrastructure of refineAlt and friends instead of the explicit
unification and CoPat generation. However, that would be wrong. Why? The
whole point of GADT refinement is that the refinement is local to the case
alternatives of the case expression, whereas in the GADT case it might vary
between alternatives.
-In fact, if we have a data instance declaration defining a GADT, eq_spec will
-be non-empty and we will get a mixture of global instantiations and local
-refinement from a single match. This neatly reflects that, as soon as we
-have constrained the type of the scrutinee to the required type index, all
-further type refinement is local to the alternative.
+RIP GADT refinement: refinements have been replaced by the use of explicit
+equality constraints that are used in conjunction with implication constraints
+to express the local scope of GADT refinements.
\begin{code}
-- Running example:
; loc <- getInstLoc origin
; dicts <- newDictBndrs loc theta'
- ; dict_binds <- tcSimplifyCheckPat loc [] emptyRefinement
- ex_tvs' dicts lie_req
+ ; dict_binds <- tcSimplifyCheckPat loc [] ex_tvs' dicts lie_req
; let res_pat = ConPatOut { pat_con = L con_span data_con,
pat_tvs = ex_tvs',
tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
tcConArg (arg_pat, arg_ty) pstate thing_inside
= tc_lpat arg_pat arg_ty pstate thing_inside
- -- NB: the tc_lpat will refine pat_ty if necessary
- -- based on the current pstate, which may include
- -- refinements from peer argument patterns to the left
\end{code}
\begin{code}
%************************************************************************
%* *
- Type refinement
-%* *
-%************************************************************************
-
-\begin{code}
-refineAlt :: DataCon -- For tracing only
- -> PatState
- -> [TcTyVar] -- Existentials
- -> [CoVar] -- Equational constraints
- -> BoxySigmaType -- Pattern type
- -> TcM PatState
-
-refineAlt con pstate ex_tvs [] pat_ty
- | null $ dataConEqTheta con
- = return pstate -- Common case: no equational constraints
-
-refineAlt con pstate ex_tvs co_vars pat_ty
- = -- See Note [Flags and equational constraints]
- do { checkTc (isRigidTy pat_ty) (nonRigidMatch con)
- -- We are matching against a GADT constructor with non-trivial
- -- constraints, but pattern type is wobbly. For now we fail.
- -- We can make sense of this, however:
- -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a
- -- (\x -> case x of { MkT v -> v })
- -- We can infer that x must have type T [c], for some wobbly 'c'
- -- and translate to
- -- (\(x::T [c]) -> case x of
- -- MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g
- -- To implement this, we'd first instantiate the equational
- -- constraints with *wobbly* type variables for the existentials;
- -- then unify these constraints to make pat_ty the right shape;
- -- then proceed exactly as in the rigid case
-
- -- In the rigid case, we perform type refinement
- ; case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
- Failed msg -> failWithTc (inaccessibleAlt msg) ;
- Succeeded reft -> do { traceTc trace_msg
- ; return (pstate { pat_reft = reft, pat_eqs = (pat_eqs pstate || not (null $ dataConEqTheta con)) }) }
- -- DO NOT refine the envt right away, because we
- -- might be inside a lazy pattern. Instead, refine pstate
- where
-
- trace_msg = text "refineAlt:match" <+>
- vcat [ ppr con <+> ppr ex_tvs,
- ppr [(v, tyVarKind v) | v <- co_vars],
- ppr reft]
- } }
-\end{code}
-
-Note [Flags and equational constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If there are equational constraints, we take account of them
-regardless of flag settings; -XGADTs etc applies only to the
-*definition* of a data type.
-
-An alternative would be also to reject a program that *used*
-constructors with equational constraints. But want we should avoid at
-all costs is simply to *ignore* the constraints, since that gives
-incomprehensible errors (Trac #2004).
-
-
-%************************************************************************
-%* *
Overloaded literals
%* *
%************************************************************************
let {
ret_ty = mkListTy unitTy ;
io_ret_ty = mkTyConApp ioTyCon [ret_ty] ;
- tc_io_stmts stmts = tcStmts DoExpr tcDoStmt stmts
- (emptyRefinement, io_ret_ty) ;
+ tc_io_stmts stmts = tcStmts DoExpr tcDoStmt stmts io_ret_ty ;
names = map unLoc (collectLStmtsBinders stmts) ;
-----------------------------------------------------------
-- tcSimplifyCheckPat is used for existential pattern match
tcSimplifyCheckPat :: InstLoc
- -> [CoVar] -> Refinement
+ -> [CoVar]
-> [TcTyVar] -- Quantify over these
-> [Inst] -- Given
-> [Inst] -- Wanted
-> TcM TcDictBinds -- Bindings
-tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
+tcSimplifyCheckPat loc co_vars qtvs givens wanteds
= ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
do { traceTc (text "tcSimplifyCheckPat")
; (irreds, binds) <- gentleCheckLoop loc givens wanteds
- ; implic_bind <- bindIrredsR loc qtvs co_vars reft
+ ; implic_bind <- bindIrredsR loc qtvs co_vars emptyRefinement
givens irreds
; return (binds `unionBags` implic_bind) }
projects / ghc-hetmet.git / commitdiff