"Occurs check" error in generated Haskell code

[gallais]

Compiling the following module using agda --compile --no-main InfiniteType.agda yields the error:

/home/gallais/languages/agda/MAlonzo/Code/InfiniteType.hs:61:1: error:
    • Occurs check: cannot construct the infinite type:
        t1 ~ MAlonzo.Code.Data.Vec.T8 Integer a1 t1
      Expected type: Integer
                     -> MAlonzo.Code.Data.Vec.T8 Integer a1 t1 -> a -> t
        Actual type: Integer -> t1 -> a -> t
    • Relevant bindings include
        d88 :: Integer -> MAlonzo.Code.Data.Vec.T8 Integer a1 t1 -> a -> t
          (bound at /home/gallais/languages/agda/MAlonzo/Code/InfiniteType.hs:61:1)

module InfiniteType where

open import Data.Vec hiding (_⊛_)
open import Data.Nat
open import Data.Fin
open import Data.Maybe
open import Data.String as String

data RTm : Set where
  Var  : String → RTm
  Case : String → RTm → String → RTm → RTm

data Tm (n : ℕ) : Set where
  Var  : Fin n → Tm n
  Case : Tm (suc n) → Tm (suc n) → Tm n

open import Category.Monad
import Level
open RawMonad (monad {Level.zero})
open import Relation.Nullary

scopeFin : ∀ {n} → Vec String n → String → Maybe (Fin n)
scopeFin []      x = nothing
scopeFin (y ∷ ρ) x with x String.≟ y
... | yes p = just zero
... | no ¬p = suc <$> scopeFin ρ x

scopeTm : ∀ {n} → Vec String n → RTm → Maybe (Tm n)
scopeTm ρ (Var x)        = Var <$> scopeFin ρ x
scopeTm ρ (Case x l y r) = Case <$> scopeTm (x ∷ ρ) l ⊛ scopeTm (y ∷ ρ) r

The problem occurs in the scopeTm ρ (Case x l y r) case. If we look at the generated code we can see a discrepancy between the two recursive calls to scopeTm: the second one is coerced a few times whereas the first one isn't.

d88 (addInt (1 :: Integer) v0) (MAlonzo.Code.Data.Vec.C22 v0 v3 v1) v4

coe d88 (coe addInt (1 :: Integer) v0) (coe MAlonzo.Code.Data.Vec.C22 v0 v5 v1) v6

Weirdly enough removing the Var constructor makes the issue go away. I'm not sure what happens here...