@@ -11,14 +11,14 @@ public export
1111data Resource : Type where
1212 MkRes : label -> Type -> Resource
1313
14+export
15+data Var = MkVar -- Phantom, just for labelling purposes
16+
1417%error_reverse
1518public export
16−(:::) : label -> Type -> Resource
19+(:::) : Var -> Type -> Resource
1720(:::) = MkRes
1821
19−export
20−data Var = MkVar -- Phantom, just for labelling purposes
21−
2222{- Contexts for holding current resources states -}
2323namespace Resources
2424 public export
@@ -33,7 +33,7 @@ namespace Resources
3333
3434{- Proof that a label has a particular type in a given context -}
3535public export
36−data InState : lbl -> Type -> Resources -> Type where
36+data InState : Var -> Type -> Resources -> Type where
3737 Here : InState lbl st (MkRes lbl st :: rs)
3838 There : InState lbl st rs -> InState lbl st (r :: rs)
3939
@@ -221,14 +221,14 @@ infix 6 :->
221221
222222public export
223223data Action : Type -> Type where
224− Stable : lbl -> Type -> Action ty
225− Trans : lbl -> Type -> (ty -> Type) -> Action ty
226− Remove : lbl -> Type -> Action ty
224+ Stable : Var -> Type -> Action ty
225+ Trans : Var -> Type -> (ty -> Type) -> Action ty
226+ Remove : Var -> Type -> Action ty
227227 Add : (ty -> Resources) -> Action ty
228228
229229namespace Stable
230230 public export %error_reduce
231− (:::) : lbl -> Type -> Action ty
231+ (:::) : Var -> Type -> Action ty
232232 (:::) = Stable
233233
234234namespace Trans
@@ -236,7 +236,7 @@ namespace Trans
236236 data Trans ty = (:->) Type Type
237237
238238 public export %error_reduce
239− (:::) : lbl -> Trans ty -> Action ty
239+ (:::) : Var -> Trans ty -> Action ty
240240 (:::) lbl (st :-> st') = Trans lbl st (const st')
241241
242242namespace DepTrans
@@ -244,7 +244,7 @@ namespace DepTrans
244244 data DepTrans ty = (:->) Type (ty -> Type)
245245
246246 public export %error_reduce
247− (:::) : lbl -> DepTrans ty -> Action ty
247+ (:::) : Var -> DepTrans ty -> Action ty
248248 (:::) lbl (st :-> st') = Trans lbl st st'
249249
250250public export
@@ -252,19 +252,19 @@ or : a -> a -> Either b c -> a
252252or x y = either (const x) (const y)
253253
254254public export %error_reduce
255−add : Type -> Action a
255+add : Type -> Action Var
256256add ty = Add (\var => [var ::: ty])
257257
258258public export %error_reduce
259−remove : lbl -> Type -> Action ty
259+remove : Var -> Type -> Action ty
260260remove = Remove
261261
262262public export %error_reduce
263−addIfRight : Type -> Action (Either a b)
263+addIfRight : Type -> Action (Either a Var)
264264addIfRight ty = Add (either (const []) (\var => [var ::: ty]))
265265
266266public export %error_reduce
267−addIfJust : Type -> Action (Maybe a)
267+addIfJust : Type -> Action (Maybe Var)
268268addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
269269
270270public export