git.iko.soy/Idris-dev
on master help sign in
Transform rules and constraints

Transform rules shouldn't be adding things to the global set of universe constraints, since they have nothing to do with them. This turns off universe constraints in partial evaluator generated definitions in particular, which should not interfere with type checking of the rest of the program.

commit908f2f241f29eae649424d3e4a1ef4cc23a9ffa7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 1 Sep 2015, 15:18 (11 years ago) parent2e170bf
3 files changed+13−10
compare with master
unifiedsplit
src/Idris/Elab/Clause.hs+7−4 src/Idris/Elab/Transform.hs+2−2 src/Idris/Elab/Utils.hs+4−4
src/Idris/Elab/Clause.hs+7−4
@@ -579,7 +579,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
579579 -- If we're inferring metavariables in the type, don't recheck,
580580 -- because we're only doing this to try to work out those metavariables
581581 (clhs_c, clhsty) <- if not inf
582− then recheckC fc id [] lhs_tm
582+ then recheckC_borrowing False (PEGenerated `notElem` opts)
583+ [] fc id [] lhs_tm
583584 else return (lhs_tm, lhs_ty)
584585 let clhs = normalise ctxt [] clhs_c
585586 let borrowed = borrowedNames [] clhs
@@ -681,14 +682,16 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
681682 logLvl 6 $ " ==> " ++ show (forget rhs')
682683
683684 (crhs, crhsty) <- if not inf
684− then recheckC_borrowing True borrowed fc id [] rhs'
685+ then recheckC_borrowing True (PEGenerated `notElem` opts)
686+ borrowed fc id [] rhs'
685687 else return (rhs', clhsty)
686688 logLvl 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty
687689 ctxt <- getContext
688690 let constv = next_tvar ctxt
689691 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of
690− OK (_, cs) -> do addConstraints fc cs
691− logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs
692+ OK (_, cs) -> when (PEGenerated `notElem` opts) $ do
693+ addConstraints fc cs
694+ logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)
692695 return ()
693696 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))
694697 i <- getIState
src/Idris/Elab/Transform.hs+2−2
@@ -65,7 +65,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in
6565 let lhs_ty = getInferType lhs'
6666 let newargs = pvars i lhs_tm
6767
68− (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm
68+ (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] fc id [] lhs_tm
6969 let clhs_tm = renamepats pnames clhs_tm_in
7070 logLvl 3 ("Transform LHS " ++ show clhs_tm)
7171 logLvl 3 ("Transform type " ++ show clhs_ty)
@@ -86,7 +86,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in
8686 processTacticDecls info newDecls
8787 sendHighlighting highlights
8888
89− (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'
89+ (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs'
9090 let crhs_tm = renamepats pnames crhs_tm_in
9191 logLvl 3 ("Transform RHS " ++ show crhs_tm)
9292
src/Idris/Elab/Utils.hs+4−4
@@ -23,9 +23,9 @@ import Debug.Trace
2323
2424import qualified Data.Map as Map
2525
26−recheckC = recheckC_borrowing False []
26+recheckC = recheckC_borrowing False True []
2727
28−recheckC_borrowing uniq_check bs fc mkerr env t
28+recheckC_borrowing uniq_check addConstrs bs fc mkerr env t
2929 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
3030 ctxt <- getContext
3131 t' <- case safeForget t of
@@ -34,8 +34,8 @@ recheckC_borrowing uniq_check bs fc mkerr env t
3434 (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of
3535 Error e -> tfail (At fc (mkerr e))
3636 OK x -> return x
37− logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs
38− addConstraints fc cs
37+ logLvl 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)
38+ when addConstrs $ addConstraints fc cs
3939 return (tm, ty)
4040
4141iderr :: Name -> Err -> Err