Fix error in conversion check
Fixes issue #187
commit06bfa758101ae84dc0a48e7e78accf57f4ea0b3d
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 18 Feb 2013, 13:08 (14 years ago)
parent4e19c35
CHANGELOG+1
@@ -8,6 +8,7 @@ Internal changes:
88* Change unification so that it keeps track of failed constraints in case
99 later information helps to resolve them
1010* Distinguishing parameters and indices in data types
11+* Faster termination/coverage checking
1112
1213New in 0.9.6:
1314-------------
src/Core/Typecheck.hs+2−2
@@ -29,10 +29,10 @@ convertsC ctxt env x y
2929converts :: Context -> Env -> Term -> Term -> TC ()
3030converts ctxt env x y
3131 = case convEq' ctxt x y of
32− OK _ -> return ()
32+ OK True -> return ()
3333 _ -> case convEq' ctxt (finalise (normalise ctxt env x))
3434 (finalise (normalise ctxt env y)) of
35− OK _ -> return ()
35+ OK True -> return ()
3636 _ -> tfail (CantConvert
3737 (finalise (normalise ctxt env x))
3838 (finalise (normalise ctxt env y)) (errEnv env))
src/Idris/ElabDecls.hs+1−1
@@ -557,7 +557,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
557557 logLvl 3 ("Elaborated: " ++ show lhs_tm)
558558 logLvl 3 ("Elaborated type: " ++ show lhs_ty)
559559 (clhs, clhsty) <- recheckC fc [] lhs_tm
560− logLvl 5 ("Checked " ++ show clhs)
560+ logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
561561 -- Elaborate where block
562562 ist <- getIState
563563 windex <- getName
test/test002/run+1−1
@@ -1,3 +1,3 @@
11#!/bin/bash
22idris $@ test002.idr --check --noprelude
3−
3+rm -f *.ibc