Normalise before looking for coercions
commit14cce81e262c47553442c5c94c6f3f2d4bfccc88
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateWed 27 Feb 2013, 23:43 (14 years ago)
parent34909f5
src/Core/ProofState.hs+1
@@ -508,6 +508,7 @@ patbind n ctxt env _ = fail "Can't pattern bind here"
508508compute :: RunTactic
509509compute ctxt env (Bind x (Hole ty) sc) =
510510 do return $ Bind x (Hole (normalise ctxt env ty)) sc
511+compute ctxt env t = return t
511512
512513hnf_compute :: RunTactic
513514hnf_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
449449 do ty <- goal
450450 -- Check for possible coercions to get to the goal
451451 -- and add them as 'alternatives'
452− let cs = getCoercionsTo ist ty
452+ env <- get_env
453+ let ty' = normalise (tt_ctxt ist) env ty
454+ let cs = getCoercionsTo ist ty'
453455 let t' = case (t, cs) of
454456 (PCoerced tm, _) -> tm
455457 (_, []) -> t