update some tests

frontend/tests/cases/negative/polymorphism/patternArity.gr.output

@@ -1,3 +1,3 @@
-Type checking failed: blappy.gr:
-Pattern arity error: blappy.gr:4:10:
+Type checking failed:
+Pattern arity error: frontend/tests/cases/negative/polymorphism/patternArity.gr:4:10:
 Data constructor `Cons` is applied to wrong number of arguments. Expecting 2 but pattern match has 1 patterns.

frontend/tests/cases/positive/deriving/drop.gr

@@ -8,7 +8,7 @@ data Store a b =
   One a | Two a b
 
 dropStore : forall {b : Type} . {Dropable b} => Store Int b -> ()
-dropStore = drop @Store
+dropStore = drop @(Store Int b)
 
 main : ((), ())
 main = let x : (Store Int Int) = (One 42)

frontend/tests/cases/positive/effect-handlers/effects_state.gr

@@ -1,23 +1,29 @@
+-- Example of using algebraic effects and handlers in Granule to capture
+-- state effects
+
+-- Uses the builtin `call` and `handle` operations.
+-- See https://granule-project.github.io/docs/modules/Primitives.html#algebraiceffectsandhandlers
+
 import State
 
 -- # State operations
 
 data Labels = Get | Put
 
 -- Operations
-data StateOps (s : Type) (r : Type) : Set Labels -> Type where
- GetOp : ()         -> (s -> r) [1 : Ext Nat]  -> StateOps s r {Get};
- PutOp : s [0..Inf] -> (() -> r) [1 : Ext Nat] -> StateOps s r {Put}
+data StateOps (s : Type) : (Set Labels) -> Type -> Type where
+ GetOp : forall {r : Type} . ()         -> (s  -> r) [1] -> StateOps s {Get} r;
+ PutOp : forall {r : Type} . s [0..Inf] -> (() -> r) [1] -> StateOps s {Put} r
 
  -- Functoriality of operations
 fmap_stateops : forall {s a b : Type, l : Set Labels}
-              . (a -> b) [0..Inf] -> StateOps s a l -> StateOps s b l
+              . (a -> b) [0..Inf] -> StateOps s l a -> StateOps s l b
 fmap_stateops [f] (GetOp () [k]) = GetOp () [f . k];
 fmap_stateops [f] (PutOp [s] [k]) = PutOp [s] [f . k]
 
 -- Handler to state monad
 stateHandler : forall {s r : Type, l : Set Labels}
-             . StateOps s (State s r) l -> State s r
+             . StateOps s l (State s r) -> State s r
 stateHandler (GetOp () [k]) = join_state (State (\([s] : s [0..Inf]) -> (k s, [s])));
 stateHandler (PutOp s [k])  = join_state (State (\([_] : s [0..Inf]) -> (k (), s)))
 

frontend/tests/cases/positive/graded-base/case.gr

@@ -2,8 +2,8 @@ language GradedBase
 
 data N = S N | Z
 
-drop : forall a .  N %(0 : Ext Nat)..(∞ : Ext Nat) -> ()
-drop x =
+dropper : forall a .  N %(0 : Ext Nat)..(∞ : Ext Nat) -> ()
+dropper x =
     (case x of
       Z -> ();
       S z -> (drop z))

frontend/tests/cases/positive/graded/resolutionIntervalInf.gr

@@ -1,5 +1,5 @@
 extract : forall {a : Type} . a [0..∞] -> a
 extract [x] = x
 
-drop : forall {a : Type} . a [0..∞] -> ()
-drop [x] = ()
+dropper : forall {a : Type} . a [0..∞] -> ()
+dropper [x] = ()