Fix error with linearity checking in patterns

lib/Prelude.idr

@@ -268,7 +268,6 @@ data Mode = Read | Write | ReadWrite
 partial
 openFile : String -> Mode -> IO File
 openFile f m = fopen f (modeStr m) where 
-  modeStr : Mode -> String
   modeStr Read  = "r"
   modeStr Write = "w"
   modeStr ReadWrite = "r+"

lib/Prelude/Strings.idr

@@ -36,7 +36,7 @@ strM x with (choose (not (x == "")))
 unpack : String -> List Char
 unpack s with (strM s)
   unpack ""             | StrNil = []
-  unpack (strCons x xs) | (StrCons _ xs) = x :: unpack xs
+  unpack (strCons x xs) | (StrCons x xs) = x :: unpack xs
 
 pack : List Char -> String
 pack [] = ""

src/Idris/AbsSyntax.hs

@@ -914,6 +914,39 @@ aiFn inpat expat ist fc f as
          | n == n' = Just (t, reverse acc ++ gs)
     find n (g : gs) acc = find n gs (g : acc)
 
+-- replace non-linear occurrences with _
+stripLinear :: IState -> PTerm -> PTerm
+stripLinear i tm = evalState (sl tm) [] where 
+    sl :: PTerm -> State [Name] PTerm
+    sl (PRef fc f) 
+         | (_:_) <- lookupTy Nothing f (tt_ctxt i)
+              = return $ PRef fc f
+         | otherwise = do ns <- get
+                          trace (show (f, ns)) $ if (f `elem` ns)
+                             then return Placeholder
+                             else do put (f : ns)
+                                     return (PRef fc f)
+    sl (PPatvar fc f) 
+                     = do ns <- get
+                          if (f `elem` ns)
+                             then return Placeholder
+                             else do put (f : ns)
+                                     return (PRef fc f)
+    sl (PApp fc fn args) = do fn' <- sl fn
+                              args' <- mapM slA args
+                              return $ PApp fc fn' args'
+       where slA (PImp p l n t d) = do t' <- sl t
+                                       return $ PImp p l n t' d
+             slA (PExp p l t d) = do t' <- sl t
+                                     return $ PExp p l t' d
+             slA (PConstraint p l t d) 
+                                = do t' <- sl t
+                                     return $ PConstraint p l t' d
+             slA (PTacImplicit p l n sc t d) 
+                                = do t' <- sl t
+                                     return $ PTacImplicit p l n sc t' d
+    sl x = return x
+
 mkPApp fc a f [] = f
 mkPApp fc a f as = let rest = drop a as in
                        appRest fc (PApp fc f (take a as)) rest

src/Idris/ElabDecls.hs

@@ -548,7 +548,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
                          [t] -> t
                          _ -> [] 
         let params = getParamsInType i [] fn_is fn_ty
-        let lhs = addImplPat i (propagateParams params lhs_in)
+        let lhs = stripLinear i $ addImplPat i (propagateParams params lhs_in)
         logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)
         logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
         ((lhs', dlhs, []), _) <- 

src/Idris/ElabTerm.hs

@@ -198,19 +198,23 @@ elab ist info pattern tcgen fn tm
               trySeq' deferr (x : xs) 
                   = try' (elab' ina x) (trySeq' deferr xs) True
     elab' ina (PPatvar fc n) | pattern = patvar n
+--         = do env <- get_env
+--              case lookup n env of
+--                 Just (PVar _) -> elab' ina Placeholder
+--                 _ -> patvar n
     elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
-                         = do ctxt <- get_context
-                              let iscon = isConName Nothing n ctxt
-                              let defined = case lookupTy Nothing n ctxt of
-                                                [] -> False
-                                                _ -> True
-                            -- this is to stop us resolve type classes recursively
-                              -- trace (show (n, guarded)) $
-                              if (tcname n && ina) then erun fc $ patvar n
-                                else if (defined && not guarded)
-                                        then do apply (Var n) []; solve
-                                        else try (do apply (Var n) []; solve)
-                                                 (patvar n)
+        = do ctxt <- get_context
+             env <- get_env
+             let defined = case lookupTy Nothing n ctxt of
+                               [] -> False
+                               _ -> True
+           -- this is to stop us resolve type classes recursively
+             -- trace (show (n, guarded)) $
+             if (tcname n && ina) then erun fc $ patvar n
+               else if (defined && not guarded)
+                       then do apply (Var n) []; solve
+                       else try (do apply (Var n) []; solve)
+                                (patvar n)
       where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of
                                 [] -> False
                                 _ -> True

src/Idris/Prover.hs

@@ -20,6 +20,7 @@ import System.Console.Haskeline.History
 import Control.Monad.State
 
 import Util.Pretty
+import Debug.Trace
 
 prover :: Bool -> Name -> Idris ()
 prover lit x =
@@ -159,6 +160,7 @@ ploop d prompt prf e h
                               return (False, e, True, prf)
               Right tac -> do (_, e) <- elabStep e saveState
                               (_, st) <- elabStep e (runTac True i tac)
+--                               trace (show (problems (proof st))) $ 
                               return (True, st, False, prf ++ [step]))
            (\err -> do iputStrLn (show err)
                        return (False, e, False, prf))

test/reg005/reg005.idr

@@ -20,15 +20,15 @@ rle [] = REnd
 rle (x :: xs) with (rle xs)
    rle (x :: Vect.Nil)             | REnd = RChar O x REnd
    rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)
-     rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just p 
+     rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just refl
            = RChar (S n) x rs
      rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing 
            = RChar O x (RChar n y rs)
 
 compress : Vect Char n -> String
 compress xs with (rle xs)
   compress Nil                 | REnd         = ""
-  compress (rep (S n) x ++ xs) | RChar n x rs 
+  compress (rep (S n) x ++ xs) | RChar _ _ rs 
          = let ni : Int = cast (S n) in
                show ni ++ show x ++ compress xs
 

test/reg010/expected

@@ -0,0 +1,4 @@
+reg010.idr:5:Can't unify P x with P y
+
+Specifically:
+	Can't unify x with y

test/reg010/reg010.idr

@@ -0,0 +1,5 @@
+module usubst
+
+total unsafeSubst : (P : a -> Type) -> (x : a) -> (y : a) -> P x -> P y
+unsafeSubst P x y px with (O)
+  unsafeSubst P x x px | _ = px

test/reg010/run

@@ -0,0 +1,2 @@
+#!/bin/bash
+idris $@ reg010.idr --check