How to use Cabal dependencies from Agda's Haskell FFI?

I have some simple code to plot some data using the Chart Haskell library:

-- Dynamical/Plot/src/HsPlot.hs
module HsPlot where

import Graphics.Rendering.Chart.Easy
import Graphics.Rendering.Chart.Backend.Cairo

plotToFile :: Double -> [Double] -> [Double] -> IO ()
plotToFile dt r f = toFile def "plot.png" $ do
    layout_title .= "Dynamics idk"
    setColors [opaque blue, opaque red]
    plot (line "rabbits" [zip [0, dt..] r ])
    plot (line "foxes" [zip [0, dt..] f])

and some Agda code which I intend to call it from:

-- Dynamical/Plot/Plot.agda
{-# OPTIONS --sized-types --guardedness #-}

module Dynamical.Plot.Plot where

open import Agda.Builtin.IO
open import Data.Float
open import Data.Unit
open import Data.List as List using (List)
open import Data.Product

postulate
  plotDynamics  : Float → List Float → List Float → IO ⊤

{-# FOREIGN GHC import HsPlot #-}
{-# COMPILE GHC plotDynamics = plotToFile #-}

open import Dynamical.LotkaVolterra
import Data.Vec as Vec

main = do
  -- lvList is a Vec of Floats, needs to be a list
  let dyn = Vec.toList lvList
  let r , f = List.unzip dyn
  plotDynamics 0.1 r f

There is also a cabal file listing Chart and Chart-cairo as dependencies in the directory Dynamical/Plot, so right next to the Agda file. Trying to agda -c Dynamical/Plot/Plot.agda --ghc-flag=-iDynamical/Plot/src will give me

/Users/deco/work/poly/MAlonzo/Code/Dynamical/Plot/Plot.hs:29:1: error:
    Could not find module ‘HsPlot’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
29 | import HsPlot

So it doesn't even find my Haskell module, let alone the Cabal dependencies. I'm trying to avoid using the flag --ghc-dont-call-ghc because that just generates a mountain of Haskell code which would be annoying to integrate with my little plotting code. I don't see any option to give the GHC backend instructions on how to find the cabal file or any modules I might have. How do I do this?

Here's the directory structure in full, too:

> tree
.
├── Categorical
│   ├── Adjunction.agda
│   ├── CartesianClosed.agda
│   ├── CompositionMonoid.agda
│   ├── Coproduct.agda
│   ├── CubicalPoly.agda
│   ├── Exponential.agda
│   ├── Functor
│   │   ├── Constant.agda
│   │   ├── Linear.agda
│   │   ├── PlugInOne.agda
│   │   └── PlugInZero.agda
│   ├── Gist.agda
│   ├── Initial.agda
│   ├── ParallelProductMonoid.agda
│   ├── Product.agda
│   └── Terminal.agda
├── Common
│   └── CategoryData.agda
└── Dynamical
    ├── Fibonacci.agda
    ├── HodgkinHuxley.agda
    ├── LotkaVolterra.agda
    ├── Plot
    │   ├── HsPlot.cabal
    │   ├── Plot.agda
    │   ├── hie.yaml
    │   └── src
    │       └── HsPlot.hs
    ├── System.agda
    └── Turing.agda

Solution

Found a solution. First of all, the Haskell module was imported as the wrong thing. Since I'm giving the raw directory to Agda, I should have just written {-# FOREIGN GHC import HsPlot #-}.

I didn't want to have to install things locally, so I ended up with this nix expression. Key part is haskellDeps and customGhc; callCabal2Nix will read the cabal file it's given and turn it into a nix expression (with package dependencies appearing as propagatedBuildInputs), and the ghcWithPackages function will add the haskell packages it's given to a bespoke GHC package database.

{ pkgs ? import <nixpkgs> {} }:

let
  # So that we don't have to repeat ourselves in the configurePhase and the
  # agdaDeps variable.
  agdaDepsNames = [
    "standard-library"
    "agda-categories"
    "cubical"
  ];
  agdaDeps = builtins.map (n: pkgs.agdaPackages.${n}) agdaDepsNames;
  
  haskellDeps = 
    builtins.filter (d: !(isNull d)) (pkgs.haskellPackages.callCabal2nix "HsPlot" ./Dynamical/Plot/HsPlot.cabal {}).propagatedBuildInputs;
  # Create a custom GHC environment with the needed dependencies. What this will do is "install"
  # a GHC that has a package db listing the dependencies in the cabal file.
  customGhc = pkgs.haskellPackages.ghcWithPackages (ps: haskellDeps);

in
pkgs.stdenv.mkDerivation {
  name = "plot";
  src = ./.;

  nativeBuildInputs = with pkgs; [
    customGhc
    (agda.withPackages (p: agdaDeps))
  ];

  configurePhase = ''
    export AGDA_DIR=$PWD/.agda
    mkdir -p $AGDA_DIR

    for dep in ${pkgs.lib.concatStringsSep " " agdaDepsNames}; do
      echo $dep >> $AGDA_DIR/defaults
    done
  '';

  buildPhase = ''
    agda -c \
      --ghc-flag=-iDynamical/Plot/src \
      ${pkgs.lib.concatMapStrings (dep: "--ghc-flag=-package=${dep.name} ") haskellDeps} \
      --ghc-flag=-package-db=${customGhc}/lib/ghc-${customGhc.version}/package.conf.d \
      Dynamical/Plot/Plot.agda
  '';

  installPhase = ''
    mkdir -p $out/bin
    cp $TMP/poly/Plot $out/bin
  '';

  meta = with pkgs.lib; {
    description = "A simple Agda project that plots data using the Chart library";
    license = licenses.mit;
  };
}