Commit 4226903d authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.

Remove GADT refinements, part 1

- A while ago, I changed the type checker to use equality constraints together
  with implication constraints to track local type refinement due to GADT
  pattern matching.  This patch is the first of a number of surgical strikes
  to remove the resulting dead code of the previous GADT refinement machinery.

  Hurray to code simplification!
parent 78ec7aab
......@@ -62,7 +62,7 @@ tcProc pat cmd exp_ty
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)
......@@ -90,27 +90,27 @@ mkCmdArrTy env t1 t2 = mkAppTys (cmd_arr env) [t1, t2]
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
......@@ -224,7 +224,7 @@ tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats maybe_rhs_sig g
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
......@@ -301,7 +301,7 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty)
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])
......
......@@ -122,8 +122,7 @@ tcMatchLambda match res_ty
\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 }
......@@ -145,8 +144,9 @@ tcMatches :: TcMatchCtxt
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 _)
......@@ -173,10 +173,10 @@ tcMatch ctxt pat_tys rhs_ty match
= 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"
......@@ -186,7 +186,7 @@ tcMatch ctxt pat_tys rhs_ty match
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
......@@ -202,7 +202,7 @@ tcGRHSs ctxt (GRHSs grhss binds) res_ty
; 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 $
......@@ -228,7 +228,7 @@ tcDoStmts :: HsStmtContext Name
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)) }
......@@ -236,14 +236,14 @@ tcDoStmts ListComp stmts body res_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) }
......@@ -254,7 +254,7 @@ tcDoStmts ctxt@(MDoExpr _) 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]
......@@ -265,12 +265,12 @@ tcDoStmts ctxt@(MDoExpr _) stmts body res_ty
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}
......@@ -284,18 +284,15 @@ tcBody body (reft, res_ty)
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
......@@ -384,7 +381,7 @@ tcLcStmt m_tc ctxt (ParStmt bndr_stmts_s) elt_ty thing_inside
; 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)
......@@ -467,14 +464,15 @@ tcLcStmt m_tc ctxt stmt elt_ty thing_inside
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
......@@ -492,12 +490,12 @@ tcDoStmt ctxt (BindStmt pat rhs bind_op fail_op) (reft,res_ty) thing_inside
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
......@@ -506,7 +504,7 @@ tcDoStmt ctxt (ExprStmt rhs then_op _) (reft,res_ty) thing_inside
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
......
......@@ -67,10 +67,10 @@ tcLetPat :: (Name -> Maybe TcRhoType)
-> 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)
......@@ -78,10 +78,10 @@ tcLetPat sig_fn pat pat_ty thing_inside
; 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
......@@ -92,17 +92,16 @@ tcLamPats :: [LPat Name] -- Patterns,
-- 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
......@@ -115,17 +114,16 @@ tc_lam_pat ctxt pat pat_ty res_ty thing_inside
-----------------
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
......@@ -155,7 +153,6 @@ tcCheckExistentialPat pats ex_tvs pat_tys body_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
}
......@@ -302,22 +299,8 @@ tc_lpat :: LPat Name
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
......@@ -589,7 +572,7 @@ correct Core, this coercion needs to be used to case the type of the scrutinee
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
......@@ -602,11 +585,9 @@ instantiation of x with (a, b) must be global; ie, it must be valid in *all*
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:
......@@ -689,8 +670,7 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
; 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',
......@@ -805,9 +785,6 @@ tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
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}
......@@ -851,69 +828,6 @@ plan for ordinary vanilla patterns to bypass the constraint
simplification step.
%************************************************************************
%* *
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
......
......@@ -1058,8 +1058,7 @@ tcGhciStmts stmts
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) ;
......
......@@ -921,16 +921,16 @@ tcSimplifyCheck loc qtvs givens wanteds
-----------------------------------------------------------
-- 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) }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment