[ refactor ] Get rid of DerivingClosure interface, nail in down

Author: buzden

src/Deriving/DepTyCheck/Gen/ForAllNeededTypes/Impl.idr

@@ -45,14 +45,14 @@ lookupLengthChecked intSig m = lookup intSig m >>= \(extSig, name) => (name,) <$
                                     Yes prf => Just $ Element extSig prf
                                     No _    => Nothing
 
-DeriveBodyForType => ClosuringContext m => Elaboration m => DerivationClosure m where
+Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface.DerivationClosure m = (DeriveBodyForType, Monad m, Elaboration m, ClosuringContext m)
 
-  needWeightFun ty = when (not !(gets $ contains ty.name)) $ do
+Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface.needWeightFun ty = when (not !(gets $ contains ty.name)) $ do
     modify {stateType=SortedSet Name} $ insert ty.name
     _ : (NamesInfoInTypes, ConsRecs) <- get
     whenJust (deriveWeightingFun ty) $ tell . mapHom singleton
 
-  callGen sig fuel values = do
+Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface.callGen sig fuel values = do
 
     -- look for external gens, and call it if exists
     let Nothing = lookupLengthChecked sig !ask

src/Deriving/DepTyCheck/Gen/ForAllNeededTypes/Interface.idr

@@ -10,17 +10,17 @@ import public Deriving.DepTyCheck.Gen.Signature
 --------------------------------------------------
 
 public export
-interface Monad m => DerivationClosure m where
-  needWeightFun : TypeInfo -> m ()
-  callGen : (sig : GenSignature) -> (fuel : TTImp) -> Vect sig.givenParams.size TTImp -> m (TTImp, Maybe (gend ** Vect gend $ Fin gend))
-  --                                                                                                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  --                                                                   this is a permutation of generated arguments --/
-  --                                                                   actually, `gend` can be calculated from `sig`, but we simplify things here
+DerivationClosure : (Type -> Type) -> Type
 
 export
-DerivationClosure m => MonadTrans t => Monad (t m) => DerivationClosure (t m) where
-  needWeightFun = lift . needWeightFun
-  callGen sig fuel params = lift $ callGen sig fuel params
+needWeightFun : DerivationClosure m => TypeInfo -> m ()
+
+export
+callGen : DerivationClosure m =>
+          (sig : GenSignature) -> (fuel : TTImp) -> Vect sig.givenParams.size TTImp -> m (TTImp, Maybe (gend ** Vect gend $ Fin gend))
+--                                                                                                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+--                                                                   this is a permutation of generated arguments --/
+--                                                                   actually, `gend` can be calculated from `sig`, but we simplify things here
 
 -------------------
 --- Conventions ---

src/Deriving/DepTyCheck/Gen/ForOneType/Impl.idr

@@ -58,7 +58,7 @@ DeriveBodyRhsForCon => DeriveBodyForType where
       | Nothing => fail "INTERNAL ERROR: unknown type for consRecs: \{show sig.targetType.name}"
 
     -- ask to derive all needed weigthing functions, if any
-    traverse_ needWeightFun $ mapMaybe (usedWeightFun . snd) consRecs
+    traverse_ (needWeightFun {m}) $ mapMaybe (usedWeightFun . snd) consRecs
 
     -- decide how to name a fuel argument on the LHS
     let fuelArg = "^fuel_arg^" -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend

src/Deriving/DepTyCheck/Gen/ForOneTypeConRhs/Impl.idr

@@ -287,7 +287,7 @@ export
           let subfuel = if mutRec then fuel else var outmostFuelArg
 
           -- Form an expression to call the subgen
-          (subgenCall, reordering) <- callGen subsig subfuel $ snd <$> subgivens
+          (subgenCall, reordering) <- lift $ callGen {m} subsig subfuel $ snd <$> subgivens
 
           -- Form an expression of binding the result of subgen
           let genedArg:::subgeneratedArgs = genedArg:::subgeneratedArgs <&> bindVar . flip Vect.index bindNames