14cce81 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Normalise before looking for coercions

14cce81Edwin Brady14 years ago

src/Core/ProofState.hs+1

@@ -508,6 +508,7 @@ patbind n ctxt env _ = fail "Can't pattern bind here"

508compute :: RunTactic

509compute ctxt env (Bind x (Hole ty) sc) =

510 do return $ Bind x (Hole (normalise ctxt env ty)) sc

511+compute ctxt env t = return t

511

512

512hnf_compute :: RunTactic

513hnf_compute :: RunTactic

513hnf_compute ctxt env (Bind x (Hole ty) sc) =

514hnf_compute ctxt env (Bind x (Hole ty) sc) =

src/Idris/ElabTerm.hs+3−1

@@ -449,7 +449,9 @@ elab ist info pattern tcgen fn tm

449 do ty <- goal

450 -- Check for possible coercions to get to the goal

451 -- and add them as 'alternatives'

452+ env <- get_env

453+ let ty' = normalise (tt_ctxt ist) env ty

452− let cs = getCoercionsTo ist ty

454+ let cs = getCoercionsTo ist ty'

453 let t' = case (t, cs) of

455 let t' = case (t, cs) of

454 (PCoerced tm, _) -> tm

456 (PCoerced tm, _) -> tm

455 (_, []) -> t

457 (_, []) -> t