Rename forall

It will become reserved in GHC 9.2
Vekhir · Oct 22, 2021 · 4b91a95 · 4b91a95
1 parent b1f3dd7
commit 4b91a95
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git a/src/Idris/Core/Elaborate.hs b/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 --git a/src/Idris/Core/ProofState.hs b/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 --git a/src/Idris/Elab/Term.hs b/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