Support mutually recursive types with `autoHsType`

[yveshauser]

I'm using the branch upstream-convertible-hstype.

The example

open import Class.HasHsType
open import Tactic.Derive.HsType

module Issue.Example where

data X : Set
data Y : Set

data X where
  MkX : Y → X

data Y where
  MkY : X → Y

instance
  HSTy-X : HasHsType X
  HSTy-Y : HasHsType Y

  HSTy-X = autoHsType X
  HSTy-Y = autoHsType Y

generates

data X = MkX (MAlonzo.Code.Class.HasHsType.HasHsType.HsType MAlonzo.Code.Issue.Example.HSTy-Y)
  deriving (Show, Eq, Generic)
data Y = MkY MAlonzo.Code.Issue.Example._.X
  deriving (Show, Eq, Generic)

where I would expect

data X = MkX MAlonzo.Code.Issue.Example.Y
  deriving (Show, Eq, Generic)
data Y = MkY MAlonzo.Code.Issue.Example.X
  deriving (Show, Eq, Generic)

[WhatisRT]

After looking into this with @zahnsimo it appears that fixing this would be quite complicated. There is no awareness of mutually recursive types, so what happens is that first X is encountered, which generates the following type (Note: I'm adding a ' to distinguish from the type we already have, what's being generated is a bit different but equivalent):

data X' : Set where
  MkX' : Y → X'

Y doesn't have a ' here because it doesn't know that a copy of Y should have been mutually defined with X'. This is why data X = MkX (MAlonzo.Code.Class.HasHsType.HasHsType.HsType MAlonzo.Code.Issue.Example.HSTy-Y) is being generated: there is no HSTy-Y yet, so this term doesn't reduce. Then the other type is generated:

data Y' : Set where
  MkY' : X' → Y'

Note that this time the type is correct, because now we have a generated type to resolve to. I guess the _ that appears for this on the Haskell is somehow an artefact of the duplicated names (it's part of the name that we get from Agda).

So in the end the real problem is that the types on the Agda side aren't correctly generated in the first place. Fixing this would probably be quite a large refactor where you pass in X and Y simultaneously and some detection of where the mutual invocations are (which would probably be quite brittle). I'm not sure it's worth the effort, especially because you can just provide the HasHsType and the FFI code by hand in this case.

[yveshauser]

Thanks for investigating this! Sure, I can just add those types and FFI code explicitly.