e3a4097 · Idris-dev · git.iko.soy

src/Core/Evaluate.hs+6

@@ -525,6 +525,12 @@ convEq ctxt = ceq [] where

525 ceq ps (P xt x _) (P yt y _)

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

527 | otherwise = sameDefs ps x y

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

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

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

531+ | n == n' = ceq ps x y

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

533+ | n == n' = ceq ps x y

528 ceq ps (V x) (V y) = return (x == y)

534 ceq ps (V x) (V y) = return (x == y)

529 ceq ps (Bind _ xb xs) (Bind _ yb ys)

535 ceq ps (Bind _ xb xs) (Bind _ yb ys)

530 = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)

536 = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)

src/Core/ProofState.hs+1−2

@@ -358,9 +358,8 @@ exact _ _ _ _ = fail "Can't fill here."

358-- As exact, but attempts to solve other goals by unification

359

360fill :: Raw -> RunTactic

361−fill guess ctxt env (Bind x (Hole ty) sc) =

361+fill guess ctxt env (Bind x (Hole ty) sc) =

362 do (val, valty) <- lift $ check ctxt env guess

363− s <- get

364-- let valtyn = normalise ctxt env valty

363-- let valtyn = normalise ctxt env valty

365-- let tyn = normalise ctxt env ty

364-- let tyn = normalise ctxt env ty

366 ns <- unify' ctxt env valty ty

365 ns <- unify' ctxt env valty ty

test/reg015/expectednew file

No changes to the content.

test/reg015/reg015.idrnew file+3

@@ -0,0 +1,3 @@

1+using (A : Type, B : A->Type, C : Type)

2+ foo : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C)

3+ foo f p = f (getWitness p) (getProof p)

test/reg015/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg015.idr --check

3+rm -f *.ibc