Evaluator bug fix

Weakening out of scope variables should not happen (we had a flawed
assumption about where the evaluator might be called from...)

idris.cabal

@@ -214,6 +214,10 @@ Extra-source-files:
                        test/reg034/run
                        test/reg034/*.idr
                        test/reg034/expected
+                       test/reg035/run
+                       test/reg035/*.idr
+                       test/reg035/*.lidr
+                       test/reg035/expected
 
                        test/basic001/run
                        test/basic001/*.idr

src/Idris/Core/Evaluate.hs

@@ -309,7 +309,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
     apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
          = do a' <- sc a
               app <- apply ntimes stk top env a' as
-              wknV (-1) app
+              wknV 1 app
     apply ntimes_in stk top env f@(VP Ref n ty) args
       | not top && hnf = case args of
                             [] -> return f
@@ -513,10 +513,10 @@ instance Quote Value where
     quote i (VTmp x)       = return $ V (i - x - 1)
 
 wknV :: Int -> Value -> Eval Value
-wknV i (VV x)         = return $ VV (x + i)
+wknV i (VV x) | x >= i = return $ VV (x - 1)
 wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
                                return $ VBind red n b' (\x -> do x' <- sc x
-                                                                 wknV i x')
+                                                                 wknV (i + 1) x')
 wknV i (VApp f a)     = liftM2 VApp (wknV i f) (wknV i a)
 wknV i t              = return t
 

src/Idris/Core/ProofState.hs

@@ -796,10 +796,12 @@ updateProblems ctxt ns ps inj holes = up ns ps where
         y' = updateSolved ns y
         err' = updateError ns err
         env' = updateEnv ns env in
-        case unify ctxt env' x' y' inj holes of
+--         trace ("Updating " ++ show (x',y')) $ 
+          case unify ctxt env' x' y' inj holes of
             OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
                                up (ns ++ v) ps
-            _ -> let (ns', ps') = up ns ps in
+            e -> -- trace ("Failed " ++ show e) $
+                  let (ns', ps') = up ns ps in
                      (ns', (x',y',env',err', um) : ps')
 
 -- attempt to solve remaining problems with match_unify
@@ -873,7 +875,9 @@ processTactic t ps
         (h:_)  -> do ps' <- execStateT (process t h) ps
                      let (ns', probs')
                                 = case solved ps' of
-                                    Just s -> updateProblems (context ps')
+                                    Just s -> traceWhen (unifylog ps')
+                                                ("SOLVED " ++ show s) $
+                                               updateProblems (context ps')
                                                       [s] (problems ps')
                                                       (injective ps')
                                                       (holes ps')

src/Idris/Core/Unify.hs

@@ -137,7 +137,7 @@ match_unify ctxt env topx topy inj holes =
         let v = highV (-1) tm in
             if v >= length ns
                then lift $ tfail (Msg "SCOPE ERROR")
-               else return [(x, bind (highV (-1) tm) ns tm)]
+               else return [(x, bind v ns tm)]
       where inst [] tm = tm
             inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
 
@@ -506,7 +506,7 @@ unify ctxt env topx topy inj holes =
         let v = highV (-1) tm in
             if v >= length ns
                then lift $ tfail (Msg "SCOPE ERROR")
-               else return [(x, bind (highV (-1) tm) ns tm)]
+               else return [(x, bind v ns tm)]
       where inst [] tm = tm
             inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
 

src/Idris/ElabTerm.hs

@@ -71,6 +71,8 @@ build ist info pattern opts fn tm
                                 resolveTC 7 g fn ist) ivs
          tm <- get_term
          ctxt <- get_context
+         probs <- get_probs
+
          when (not pattern) $ do matchProblems True; unifyProblems
          probs <- get_probs
          case probs of

test/reg035/expected

@@ -0,0 +1,4 @@
+reg035b.idr:7:6:Can't convert
+        Additive -> Nat
+with
+        Fin 0

test/reg035/reg035.idr

@@ -0,0 +1,15 @@
+elimId : (a : Type) ->
+         (a1 : a) ->
+         (a2 : a) ->
+         (m : (x : a) -> (y : a) -> x = y -> Type) ->
+         (f : (x : a) -> m x x refl) ->
+         (id : a1 = a2) ->
+         m a1 a2 id
+elimId _ x _ _ f refl = f x
+
+tran : (a : Type) -> (b : a) -> (c : a) -> (d : a) ->  
+       (e : b = c) ->  (f : c = d) ->  b = d
+tran = \ a : Type , b : a , c : a , d : a , e : b = c =>
+    (elimId a b c (\ f : a , g : a , h : f = g => 
+                         (i : a) ->  (j : g = i) ->  f = i)
+                 (\ f : a , g : a , h : f = g =>  h) e d)

test/reg035/reg035a.lidr

@@ -0,0 +1,66 @@
+> module Set
+
+> %default total
+
+> postulate soAndIntro : (p : alpha -> Bool) ->
+>                        (q : beta -> Bool) -> 
+>                        (a : alpha) ->
+>                        (b : beta) ->
+>                        so (p a) ->
+>                        so (q b) ->
+>                        so (p a && q b)
+
+> hasNoDuplicates : (Eq alpha) => List alpha -> Bool
+> hasNoDuplicates as = as == nub as
+
+> %assert_total
+> setEq : (Eq alpha) => List alpha -> List alpha -> Bool
+> setEq Nil Nil = True
+> setEq Nil (y :: ys) = False
+> setEq (x :: xs) Nil = False
+> setEq {alpha} (x :: xs) (y :: ys) =
+>   (x == y && setEq xs ys) 
+>   ||
+>   (elem x ys && elem y xs && 
+>    setEq (filter (/= y) xs) (filter (/= x) ys)
+>   )
+
+> data Set : Type -> Type where
+>   setify : (as : List a) -> Set a
+
+> instance (Eq a) => Eq (Set a) where
+>   (==) (setify as) (setify bs) = setEq as bs
+
+> postulate reflexive_Set_eqeq : (Eq a) => 
+>                                (as : Set a) -> 
+>                                so (as == as)
+
+> unwrap : Set a -> List a
+> unwrap (setify as) = as
+
+> union : Set (Set a) -> Set a
+> union (setify ss) = setify (concat (map unwrap ss)) 
+
+> listify : (Eq a) => Set a -> List a
+> listify = nub . unwrap
+
+> arePairwiseDisjoint : (Eq a) => Set (Set a) -> Bool
+> arePairwiseDisjoint (setify ss) = 
+>   hasNoDuplicates (concat (map listify ss))
+
+> isPartition : (Eq a) => Set (Set a) -> Set a -> Bool
+> isPartition ass as = arePairwiseDisjoint ass && union ass == as
+
+> partitionLemma0 : (Eq alpha) => 
+>                   (ass : Set (Set alpha)) -> 
+>                   so (arePairwiseDisjoint ass) ->
+>                   so (ass `isPartition` union ass)
+> partitionLemma0 ass asspd = (soAndIntro (\ xss => arePairwiseDisjoint xss)
+>                                        (\ xs => union ass == xs)
+>                                        ass
+>                                        (union ass)
+>                                        asspd 
+>                                        uasseqas) where
+>   uasseqas : so (union ass == union ass)
+>   uasseqas = reflexive_Set_eqeq (union ass)
+

test/reg035/reg035b.idr

@@ -0,0 +1,11 @@
+import Data.Vect
+
+total
+finZEmpty : Fin Z -> a
+
+fins : (n : Nat) -> (xs : Vect n (Fin n) ** ((x : Fin n) -> Elem x xs))
+fins Z     = ([] ** (finZEmpty {a=_}))
+
+-- f : (a : Nat) -> a = S a -> _|_
+-- f a = believe_me
+

test/reg035/run

@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+idris --check reg035.idr
+idris --check reg035a.lidr
+idris --check reg035b.idr
+rm -f *.ibc