f65d7ad · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Eta in conversion, consistent with unification

We had a conversion rule that f converts with \x => f x, but it has never worked because I did it wrong. Now it does. Fixes #710, fixes #2071 (which are duplicates) (This patch scares me slightly, for reasons I can't quite work out...)

commitf65d7ad5586d316dd2e5a5f32ff46e825a121f13 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 30 Mar 2015, 18:45 (12 years ago) parent967c0e1

2 files changed+5−3

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+4−2 src/Idris/Elab/Clause.hs+1−1

src/Idris/Core/Evaluate.hs+4−2

@@ -576,8 +576,10 @@ convEq ctxt holes topx topy = ceq [] topx topy where

576576 | x `elem` holes || y `elem` holes = return True

577577 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

578578 | otherwise = sameDefs ps x y

579− ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y

580− ceq ps (Bind n (Lam t) (App x (V 0))) y = ceq ps x y

579+ ceq ps x (Bind n (Lam t) (App y (V 0)))

580+ = ceq ps x (substV (P Bound n t) y)

581+ ceq ps (Bind n (Lam t) (App x (V 0))) y

582+ = ceq ps (substV (P Bound n t) x) y

581583 ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))

582584 | n == n' = ceq ps x y

583585 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

src/Idris/Elab/Clause.hs+1−1

@@ -702,7 +702,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

702702 (crhs, crhsty) <- if not inf

703703 then recheckC_borrowing True borrowed fc id [] rhs'

704704 else return (rhs', clhsty)

705− logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

705+ logLvl 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty

706706 ctxt <- getContext

707707 let constv = next_tvar ctxt

708708 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of