2acbdf6 · Idris-dev · git.iko.soy

src/Core/Evaluate.hs+1−1

compare with master

unifiedsplit

@@ -552,7 +552,7 @@ convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool

552convEq ctxt = ceq [] where

553 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool

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

555− | (xt == yt && x ==y ) || (x, y) `elem` ps || (y,x) `elem` ps = return True

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

556 | otherwise = sameDefs ps x y

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

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

src/Core/Typecheck.hs+6−5

@@ -28,11 +28,12 @@ convertsC ctxt env x y

28

29converts :: Context -> Env -> Term -> Term -> TC ()

30converts ctxt env x y

31+ = case convEq' ctxt x y of

31− = if x == y then return () else

32+ OK _ -> return ()

32− if (finalise (normalise ctxt env x) ==

33+ _ -> case convEq' ctxt (finalise (normalise ctxt env x))

33− finalise (normalise ctxt env y))

34+ (finalise (normalise ctxt env y)) of

34− then return ()

35+ OK _ -> return ()

35− else tfail (CantConvert

36+ _ -> tfail (CantConvert

36 (finalise (normalise ctxt env x))

37 (finalise (normalise ctxt env x))

37 (finalise (normalise ctxt env y)) (errEnv env))

38 (finalise (normalise ctxt env y)) (errEnv env))

38

39

src/Idris/ElabDecls.hs+2−2

@@ -566,7 +566,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

566 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

567 case converts ctxt [] clhsty crhsty of

568 OK _ -> return ()

569− Error _ -> ierror (At fc (CantUnify False clhsty crhsty (Msg "") [] 0))

569+ Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

570 i <- get

571 checkInferred fc (delab' i crhs True) rhs

572 return $ Right (clhs, crhs)

@@ -794,7 +794,7 @@ elabClass info syn doc fc constraints tn ps ds

794 pibind [] x = x

795 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

796

797− mdec (UN n) = (UN ('!':n))

797+ mdec (UN n) = UN ('!':n)

798 mdec (NS x n) = NS (mdec x) n

799 mdec x = x

800