Remove linearity subtyping

It's disappointing to have to do this, but I think necessary because
various issue reports have shown it to be unsound (at least as far as
inference goes) and, at the very least, confusing. This patch brings us
back to the basic rules of QTT.

On the one hand, this makes the 1 multiplicity less useful, because it
means we can't flag arguments as being used exactly once which would be
useful for optimisation purposes as well as precision in the type. On
the other hand, it removes some complexity (and a hack) from
unification, and has the advantage of being correct! Also, I still
consider the 1 multiplicity an experiment.

We can still do interesting things like protocol state tracking, which
is my primary motivation at least.

Ideally, if the 1 multiplicity is going to be more generall useful,
we'll need some kind of way of doing multiplicity polymorphism in the
future. I don't think subtyping is the way (I've pretty much always come
to regret adding some form of subtyping).

Fixes idris-lang#73 (and maybe some others).

Author: edwinb

CHANGELOG.md

@@ -15,7 +15,7 @@ Command-line options changes:
   provided.  An explicit `0` has the effect of simulating a terminal with
   unbounded width.
 
-Compiler changes:
+Language and compiler changes:
 
 * Added new syntax for named applications and the bind-all-explicits pattern:
 
@@ -31,6 +31,14 @@ Compiler changes:
   boundaries to the AST nodes `FC`.
 * New experimental ``refc`` code generator, which generates C with reference
   counting.
+* `%hint` annotations one local definitions (in `let` or `where` blocks) now
+  work, meaning that local definitions can be searched in auto implicit search.
+* Local implementations of interfaces now work.
+* Removed multiplicity subtyping, as this appears to be unsound and causes more
+  problems than it solves. Unfortunately, this means you sometimes now need to
+  write linear versions of functions as special cases. (Though note that the 1
+  multiplicity is still considered experimental, so hopefully this will change
+  for the better in the future!)
 
 REPL/IDE mode changes:
 

libs/base/Control/App.idr

@@ -213,21 +213,21 @@ get tag @{MkState r}
           MkAppRes (Right val)
 
 export
-put : (0 tag : _) -> State tag t e => (1 val : t) -> App {l} e ()
+put : (0 tag : _) -> State tag t e => (val : t) -> App {l} e ()
 put tag @{MkState r} val
     = MkApp $
           prim_app_bind (toPrimApp $ writeIORef r val) $ \val =>
           MkAppRes (Right ())
 
 export
-modify : (0 tag : _) -> State tag t e => (1 p : t -> t) -> App {l} e ()
+modify : (0 tag : _) -> State tag t e => (p : t -> t) -> App {l} e ()
 modify tag f
     = let (>>=) = bindL in
           do x <- get tag
              put tag (f x)
 
 export
-new : t -> (1 p : State tag t e => App {l} e a) -> App {l} e a
+new : t -> (p : State tag t e => App {l} e a) -> App {l} e a
 new val prog
     = MkApp $
          prim_app_bind (toPrimApp $ newIORef val) $ \ref =>

libs/base/Control/Monad/Either.idr

@@ -19,7 +19,7 @@ import Control.Monad.State
 
 public export
 data EitherT : (e : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
-  MkEitherT : (1 _ : m (Either e a)) -> EitherT e m a
+  MkEitherT : m (Either e a) -> EitherT e m a
 
 export
 %inline

libs/base/Control/Monad/ST.idr

@@ -23,7 +23,7 @@ mutual
 
   export
   Applicative (ST s) where
-    pure = MkST . pure
+    pure x = MkST (pure x)
     (<*>) f a = pure $ !f !a
 
   export

libs/base/Data/IORef.idr

@@ -25,7 +25,7 @@ readIORef (MkRef m) = primIO (prim__readIORef m)
 
 %inline
 export
-writeIORef : HasIO io => IORef a -> (1 val : a) -> io ()
+writeIORef : HasIO io => IORef a -> (val : a) -> io ()
 writeIORef (MkRef m) val = primIO (prim__writeIORef m val)
 
 export

libs/base/Data/List1.idr

@@ -15,20 +15,20 @@ record List1 a where
 
 ||| Forget that a list is non-empty
 public export
-forget : (1 xs : List1 a) -> List a
+forget : (xs : List1 a) -> List a
 forget (x ::: xs) = x :: xs
 
 ||| Check whether a list is non-empty
 export
-fromList : (1 xs : List a) -> Maybe (List1 a)
+fromList : (xs : List a) -> Maybe (List1 a)
 fromList [] = Nothing
 fromList (x :: xs) = Just (x ::: xs)
 
 ------------------------------------------------------------------------
 -- Basic functions
 
 public export
-singleton : (1 x : a) -> List1 a
+singleton : (x : a) -> List1 a
 singleton a = a ::: []
 
 export
@@ -59,39 +59,39 @@ foldl1 n c (x ::: xs) = foldl c (n x) xs
 -- Append
 
 export
-appendl : (1 xs : List1 a) -> (1 ys : List a) -> List1 a
+appendl : (xs : List1 a) -> (ys : List a) -> List1 a
 appendl (x ::: xs) ys = x ::: xs ++ ys
 
 export
-append : (1 xs, ys : List1 a) -> List1 a
+append : (xs, ys : List1 a) -> List1 a
 append xs ys = appendl xs (forget ys)
 
 export
-lappend : (1 xs : List a) -> (1 ys : List1 a) -> List1 a
+lappend : (xs : List a) -> (ys : List1 a) -> List1 a
 lappend [] ys = ys
 lappend (x :: xs) ys = append (x ::: xs) ys
 
 ------------------------------------------------------------------------
 -- Cons/Snoc
 
 public export
-cons : (1 x : a) -> (1 xs : List1 a) -> List1 a
+cons : (x : a) -> (xs : List1 a) -> List1 a
 cons x xs = x ::: forget xs
 
 export
-snoc : (1 xs : List1 a) -> (1 x : a) -> List1 a
+snoc : (xs : List1 a) -> (x : a) -> List1 a
 snoc xs x = append xs (singleton x)
 
 ------------------------------------------------------------------------
 -- Reverse
 
 public export
-reverseOnto : (1 acc : List1 a) -> (1 xs : List a) -> List1 a
+reverseOnto : (acc : List1 a) -> (xs : List a) -> List1 a
 reverseOnto acc [] = acc
 reverseOnto acc (x :: xs) = reverseOnto (x ::: forget acc) xs
 
 public export
-reverse : (1 xs : List1 a) -> List1 a
+reverse : (xs : List1 a) -> List1 a
 reverse (x ::: xs) = reverseOnto (singleton x) xs
 
 ------------------------------------------------------------------------

libs/base/Data/Vect.idr

@@ -14,7 +14,7 @@ data Vect : (len : Nat) -> (elem : Type) -> Type where
   Nil  : Vect Z elem
   ||| A non-empty vector of length `S len`, consisting of a head element and
   ||| the rest of the list, of length `len`.
-  (::) : (1 x : elem) -> (1 xs : Vect len elem) -> Vect (S len) elem
+  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
 
 -- Hints for interactive editing
 %name Vect xs,ys,zs,ws
@@ -101,7 +101,7 @@ index (FS k) (_::xs) = index k xs
 ||| insertAt 1 8 [1,2,3,4]
 ||| ```
 public export
-insertAt : (1 idx : Fin (S len)) -> (1 x : elem) -> (1 xs : Vect len elem) -> Vect (S len) elem
+insertAt : (idx : Fin (S len)) -> (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
 insertAt FZ     y xs      = y :: xs
 insertAt (FS k) y (x::xs) = x :: insertAt k y xs
 
@@ -145,7 +145,7 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
 ||| [1,2,3,4] ++ [5,6]
 ||| ```
 public export
-(++) : (1 xs : Vect m elem) -> (1 ys : Vect n elem) -> Vect (m + n) elem
+(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
 (++) []      ys = ys
 (++) (x::xs) ys = x :: xs ++ ys
 
@@ -207,9 +207,9 @@ merge = mergeBy compare
 ||| reverse [1,2,3,4]
 ||| ```
 public export
-reverse : (1 xs : Vect len elem) -> Vect len elem
+reverse : (xs : Vect len elem) -> Vect len elem
 reverse xs = go [] xs
-  where go : (1 _ : Vect n elem) -> (1 _ : Vect m elem) -> Vect (n+m) elem
+  where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
         go {n}         acc []        = rewrite plusZeroRightNeutral n in acc
         go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
                                        in go (x::acc) xs
@@ -244,7 +244,7 @@ toVect (S k) (x :: xs)
 toVect _ _ = Nothing
 
 public export
-fromList' : (1 xs : Vect len elem) -> (1 l : List elem) -> Vect (length l + len) elem
+fromList' : (xs : Vect len elem) -> (l : List elem) -> Vect (length l + len) elem
 fromList' ys [] = ys
 fromList' {len} ys (x::xs) =
   rewrite (plusSuccRightSucc (length xs) len) in
@@ -258,7 +258,7 @@ fromList' {len} ys (x::xs) =
 ||| fromList [1,2,3,4]
 ||| ```
 public export
-fromList : (1 l : List elem) -> Vect (length l) elem
+fromList : (xs : List elem) -> Vect (length xs) elem
 fromList l =
   rewrite (sym $ plusZeroRightNeutral (length l)) in
   reverse $ fromList' [] l
@@ -283,16 +283,13 @@ zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
 
 ||| Linear version
 public export
-lzipWith : (f : (1 _ : a) -> (1 _ : b) -> c)
-      -> (1 _ : Vect n a)
-      -> (1 _ : Vect n b)
-      -> Vect n c
+lzipWith : (f : a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
 lzipWith _ [] [] = []
 lzipWith f (x::xs) (y::ys) = f x y :: lzipWith f xs ys
 
 ||| Extensional correctness lemma
 export
-lzipWithSpec : (f : (1 _ : a) -> (1 _ : b) -> c)
+lzipWithSpec : (f : a -> b -> c)
          -> (xs : Vect n a) -> (ys : Vect n b)
          -> lzipWith f xs ys = zipWith f xs ys
 lzipWithSpec _ [] [] = Refl
@@ -314,7 +311,7 @@ zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
 ||| zip (fromList [1,2,3,4]) (fromList [1,2,3,4])
 ||| ```
 public export
-zip : (1 xs : Vect n a) -> (1 ys : Vect n b) -> Vect n (a, b)
+zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
 zip []      []      = []
 zip (x::xs) (y::ys) = (x, y) :: zip xs ys
 
@@ -324,7 +321,7 @@ zip (x::xs) (y::ys) = (x, y) :: zip xs ys
 ||| zip3 (fromList [1,2,3,4]) (fromList [1,2,3,4]) (fromList [1,2,3,4])
 ||| ```
 public export
-zip3 : (1 xs : Vect n a) -> (1 ys : Vect n b) -> (1 zs : Vect n c) -> Vect n (a, b, c)
+zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
 zip3 []      []      []      = []
 zip3 (x::xs) (y::ys) (z::zs) = (x, y, z) :: zip3 xs ys zs
 
@@ -334,7 +331,7 @@ zip3 (x::xs) (y::ys) (z::zs) = (x, y, z) :: zip3 xs ys zs
 ||| unzip (fromList [(1,2), (1,2)])
 ||| ```
 public export
-unzip : (1 xs : Vect n (a, b)) -> (Vect n a, Vect n b)
+unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
 unzip []           = ([], [])
 unzip ((l, r)::xs) = let (lefts, rights) = unzip xs
                      in (l::lefts, r::rights)
@@ -345,7 +342,7 @@ unzip ((l, r)::xs) = let (lefts, rights) = unzip xs
 ||| unzip3 (fromList [(1,2,3), (1,2,3)])
 ||| ```
 public export
-unzip3 : (1 xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
+unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
 unzip3 []            = ([], [], [])
 unzip3 ((l,c,r)::xs) = let (lefts, centers, rights) = unzip3 xs
                        in (l::lefts, c::centers, r::rights)
@@ -436,7 +433,7 @@ implementation Foldable (Vect n) where
 ||| concat [[1,2,3], [4,5,6]]
 ||| ```
 public export
-concat : (1 xss : Vect m (Vect n elem)) -> Vect (m * n) elem
+concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
 concat []      = []
 concat (v::vs) = v ++ Vect.concat vs
 
@@ -810,7 +807,7 @@ vectToMaybe (x::xs) = Just x
 ||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
 ||| ```
 public export
-catMaybes : (1 xs : Vect n (Maybe elem)) -> (p ** Vect p elem)
+catMaybes : (xs : Vect n (Maybe elem)) -> (p ** Vect p elem)
 catMaybes []             = (_ ** [])
 catMaybes (Nothing::xs)  = catMaybes xs
 catMaybes ((Just j)::xs) =
@@ -845,7 +842,7 @@ range {len=S _} = FZ :: map FS range
 ||| transpose [[1,2], [3,4], [5,6], [7,8]]
 ||| ```
 public export
-transpose : {n : _} -> (1 array : Vect m (Vect n elem)) -> Vect n (Vect m elem)
+transpose : {n : _} -> (array : Vect m (Vect n elem)) -> Vect n (Vect m elem)
 transpose []        = replicate _ []                 -- = [| [] |]
 transpose (x :: xs) = lzipWith (::) x (transpose xs) -- = [| x :: xs |]
 

libs/contrib/Control/Linear/LIO.idr

@@ -95,7 +95,7 @@ Applicative io => Applicative (L io) where
 
 export
 (Applicative m, LinearBind m) => Monad (L m) where
-  (>>=) = Bind
+  (>>=) a k = Bind a k
 
 -- prioritise this one for concrete LIO, so we get the most useful
 -- linearity annotations.

libs/contrib/Data/HVect.idr

@@ -21,7 +21,7 @@ data HVect : Vect k Type -> Type where
 ||| 1
 ||| ```
 public export
-index : (1 i : Fin k) -> (1 _ : HVect ts) -> index i ts
+index : (i : Fin k) -> HVect ts -> index i ts
 index FZ (x :: xs) = x
 index (FS j) (x :: xs) = index j xs
 
@@ -32,7 +32,7 @@ index (FS j) (x :: xs) = index j xs
 ||| ["string"]
 ||| ```
 public export
-deleteAt : (1 i : Fin (S l)) -> (1 _ : HVect ts) -> HVect (deleteAt i ts)
+deleteAt : (i : Fin (S l)) -> HVect ts -> HVect (deleteAt i ts)
 deleteAt FZ (x :: xs) = xs
 deleteAt (FS FZ) (x :: (y :: xs)) = x :: xs
 deleteAt (FS (FS j)) (x :: (y :: xs)) = x :: deleteAt (FS j) (y :: xs)
@@ -44,7 +44,7 @@ deleteAt (FS (FS j)) (x :: (y :: xs)) = x :: deleteAt (FS j) (y :: xs)
 ||| ["firstString", "string"]
 ||| ```
 public export
-replaceAt : (1 i : Fin k) -> t -> (1 _ : HVect ts) -> HVect (replaceAt i t ts)
+replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)
 replaceAt FZ y (x :: xs) = y :: xs
 replaceAt (FS j) y (x :: xs) = x :: replaceAt j y xs
 
@@ -55,7 +55,7 @@ replaceAt (FS j) y (x :: xs) = x :: replaceAt j y xs
 ||| [True, "string"]
 ||| ```
 public export
-updateAt : (1 i : Fin k) -> (index i ts -> t) -> (1 _ : HVect ts) -> HVect (replaceAt i t ts)
+updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)
 updateAt FZ f (x :: xs) = f x :: xs
 updateAt (FS j) f (x :: xs) = x :: updateAt j f xs
 
@@ -66,7 +66,7 @@ updateAt (FS j) f (x :: xs) = x :: updateAt j f xs
 ||| [1, "string"]
 ||| ```
 public export
-(++) : (1 _ : HVect ts) -> HVect us -> HVect (ts ++ us)
+(++) : HVect ts -> HVect us -> HVect (ts ++ us)
 (++) [] ys = ys
 (++) (x :: xs) ys = x :: (xs ++ ys)
 
@@ -79,11 +79,11 @@ public export
   (x :: xs) == (y :: ys) = x == y && xs == ys
 
 public export
-consInjective1 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (1 _ : x :: xs = y :: ys) -> x = y
+consInjective1 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (x :: xs = y :: ys) -> x = y
 consInjective1 Refl = Refl
 
 public export
-consInjective2 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (1 _ : x :: xs = y :: ys) -> xs = ys
+consInjective2 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (x :: xs = y :: ys) -> xs = ys
 consInjective2 Refl = Refl
 
 public export

libs/contrib/Data/Linear/Array.idr

@@ -19,8 +19,8 @@ interface Array arr => MArray arr where
   -- Array is unchanged if the index is out of bounds
   write : (1 _ : arr t) -> Int -> t -> arr t
 
-  mread : (1 _ : arr t) -> Int -> LPair (Maybe t) (arr t)
-  msize : (1 _ : arr t) -> LPair Int (arr t)
+  mread : (1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))
+  msize : (1 _ : arr t) -> Res Int (const (arr t))
 
 export
 data IArray : Type -> Type where
@@ -57,16 +57,17 @@ Array IArray where
   size (MkIArray a) = max a
 
 export
-copyArray : MArray arr => (newsize : Int) -> (1 _ : arr t) -> (arr t, arr t)
+copyArray : MArray arr => (newsize : Int) -> (1 _ : arr t) ->
+            LPair (arr t) (arr t)
 copyArray newsize a
     = let size # a = msize a in
           newArray newsize $
             (\a' => copyContent (min (newsize - 1) (size - 1)) a a')
   where
-    copyContent : Int -> (1 _ : arr t) -> (1 _ : arr t) -> (arr t, arr t)
+    copyContent : Int -> (1 _ : arr t) -> (1 _ : arr t) -> LPair (arr t) (arr t)
     copyContent pos a a'
         = if pos < 0
-             then (a, a')
+             then a # a'
              else let val # a = mread a pos
                       1 a' = case val of
                                   Nothing => a'