f65d7ad · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Eta in conversion, consistent with unification

f65d7adEdwin Brady12 years ago

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

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

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

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

578 | otherwise = sameDefs ps x y

579− ceq ps x (Bind n (Lam t) (App y (V 0))) = 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)

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

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

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

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

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

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

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

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

585 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

702 (crhs, crhsty) <- if not inf

703 then recheckC_borrowing True borrowed fc id [] rhs'

704 else return (rhs', clhsty)

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

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

706 ctxt <- getContext

707 let constv = next_tvar ctxt

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