Merge pull request #4908 from melted/idris-release-1.3.4

Idris release 1.3.4

Author: melted

Diff for: CHANGELOG.md

@@ -1,5 +1,9 @@
 # New since last release
 
+# New in 1.3.4
++ Renamed 'forall' function for compability with future GHC releases
++ Updated version bounds
++ Bugfixes
 # New in 1.3.3
 + Updated to work with GHC 8.8 and cabal 3.0
 + Bugfixes and documentation updates

Diff for: appveyor.yml

@@ -1,19 +1,19 @@
 version: 1.0.{build}
 init:
 - ps: >-
-    choco install cabal --no-progress
+    choco install cabal --version=3.4.1.0 --no-progress
 
     mkdir C:\ghc
 
-    Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.8.2/ghc-8.8.2-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
+    Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.10.7/ghc-8.10.7-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
 
     7z x C:\ghc\ghc.tar.xz -oC:\ghc
 
     7z x C:\ghc\ghc.tar -oC:\ghc
 
-    $env:PATH="$env:PATH;c:\ghc\ghc-8.8.2\bin;$HOME\AppData\Roaming\cabal\bin"
+    $env:PATH="$env:PATH;c:\ghc\ghc-8.10.7\bin;$HOME\AppData\Roaming\cabal\bin"
 
-    cabal v1-update
+    cabal update
 
     $env:current_posix=c:\msys64\usr\bin\cygpath -u $(pwd)
 

Diff for: idris.cabal

@@ -1,6 +1,6 @@
 Cabal-Version:  2.4
 Name:           idris
-Version:        1.3.3
+Version:        1.3.4
 License:        BSD-3-Clause
 License-file:   LICENSE
 Author:         Edwin Brady

Diff for: src/Idris/Core/Elaborate.hs

@@ -434,8 +434,8 @@ intro n = processTactic' (Intro n)
 introTy :: Raw -> Maybe Name -> Elab' aux ()
 introTy ty n = processTactic' (IntroTy ty n)
 
-forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
-forall n r i t = processTactic' (Forall n r i t)
+forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
+forAll n r i t = processTactic' (Forall n r i t)
 
 letbind :: Name -> RigCount -> Raw -> Raw -> Elab' aux ()
 letbind n rig t v = processTactic' (LetBind n rig t v)
@@ -823,7 +823,7 @@ arg :: Name -> RigCount -> Maybe ImplicitInfo -> Name -> Elab' aux ()
 arg n r i tyhole = do ty <- unique_hole tyhole
                       claim ty RType
                       movelast ty
-                      forall n r i (Var ty)
+                      forAll n r i (Var ty)
 
 -- try a tactic, if it adds any unification problem, return an error
 no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()

Diff for: src/Idris/Core/ProofState.hs

@@ -658,13 +658,13 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
            _ -> lift $ tfail $ CantIntroduce t'
 intro n ctxt env _ = fail "Can't introduce here."
 
-forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic
-forall n rig impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
+forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic
+forAll n rig impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
     do (tyv, tyt) <- lift $ check ctxt env ty
        unify' ctxt env (tyt, Nothing) (TType (UVar [] 0), Nothing)
        unify' ctxt env (t, Nothing) (TType (UVar [] 0), Nothing)
        return $ Bind n (Pi rig impl tyv (TType (UVar [] 0))) (Bind x (Hole t) (P Bound x t))
-forall n rig impl ty ctxt env _ = fail "Can't pi bind here"
+forAll n rig impl ty ctxt env _ = fail "Can't pi bind here"
 
 patvar :: Name -> RunTactic
 patvar n ctxt env (Bind x (Hole t) sc) =
@@ -1052,7 +1052,7 @@ process t h = tactic (Just h) (mktac t)
          mktac WHNF_ComputeArgs  = whnf_compute_args
          mktac (Intro n)         = intro n
          mktac (IntroTy ty n)    = introTy ty n
-         mktac (Forall n r i t)  = forall n r i t
+         mktac (Forall n r i t)  = forAll n r i t
          mktac (LetBind n r t v) = letbind n r t v
          mktac (ExpandLet n b)   = expandLet n b
          mktac (Rewrite t)       = rewrite t

Diff for: src/Idris/Elab/Term.hs

@@ -685,7 +685,7 @@ elab ist info emode opts fn tm
                     _ -> unless (LinearTypes `elem` idris_language_extensions ist
                                        || e_qq ina) $
                            lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a linear argument")
-               forall n' (pcount p) (is_scoped p) (Var tyn)
+               forAll n' (pcount p) (is_scoped p) (Var tyn)
                addAutoBind p n'
                addPSname n' -- okay for proof search
                focus tyn
@@ -2107,7 +2107,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
       = do ~[n, ty] <- tacTmArgs 2 tac args
            n' <- reifyTTName n
            ty' <- reifyRaw ty
-           forall n' RigW Nothing ty'
+           forAll n' RigW Nothing ty'
            returnUnit
       | n == tacN "Prim__PatVar"
       = do ~[n] <- tacTmArgs 1 tac args