Agda 2.7.0.1 编译时启用性能分析(Profiling)的GHC内部错误分析

在Agda 2.7.0.1版本中，当尝试使用GHC的性能分析(profiling)功能编译某些Agda程序时，会遇到GHC编译器的内部错误(panic)。这个问题主要出现在使用GHC 9.12.2版本时，但在GHC 9.10.2版本中部分情况可以正常工作。

问题背景

Agda作为一种依赖类型的函数式编程语言，最终会通过MAlonzo后端将代码编译为Haskell，再通过GHC编译为可执行文件。当开发者尝试使用GHC的性能分析功能(通过--ghc-flag=-prof和--ghc-flag=-fprof-auto选项)来优化Agda程序时，在某些特定情况下会触发GHC的内部错误。

错误表现

典型的错误信息如下：

ghc: panic! (the 'impossible' happened)
GHC version 9.12.2:
getStgArgFromTrivialArg
case sat_s1qM @(*) @Any @(ZonkAny 67) of { UnsafeRefl co7_s1r4 ->
ww2_s1qK
`cast` (Sub (Sym co7_s1r4)
        ; SelCo:Fun(arg) (SelCo:Fun(res) (Sub co6_s1qU))
        :: Any ~R# [ZonkAny 68])
}

这种错误发生在GHC的核心到STG(Spineless Tagless G-machine)中间表示转换阶段，具体是在处理类型转换(cast)操作时。

最小复现案例

通过分析，可以提取出一个最小复现案例。以下Agda代码在启用性能分析编译时会触发该错误：

module OfSemiring where

record Sigma (A : Set) (B : A → Set) : Set where
  constructor pair
  field
    fst : A
    snd : B fst

data Nat : Set where
  zero : Nat
  suc : (n : Nat) → Nat

data List (A : Set) : Set where
  nil  : List A
  cons : (x : A) (xs : List A) → List A

{-# BUILTIN LIST List #-}

foldr : {A B : Set} → (A → B → B) → B → List A → B
foldr c n nil         = n
foldr c n (cons x xs) = c x (foldr c n xs)

record Semiring : Set₁ where
  field
    Carrier : Set
    plus    : Carrier → Carrier → Carrier
    zero    : Carrier
    trans   : {x y z : Carrier} → x ≡ y → y ≡ z → x ≡ z

module SemiringList (R : Semiring) where
  open Semiring R

  dotProduct : List Carrier → List Carrier → Carrier
  dotProduct xs ys = foldr plus zero (zipWith times xs ys)

  testSubList : List Carrier → List Carrier → Set
  testSubList bs cs = ∀ x → x ∈ bs → x ∈ cs
    where
      _∈_ : Carrier → List Carrier → Set
      x ∈ bs = Σ (List Carrier) λ qs → dotProduct qs bs ≡ x

问题分析

经过深入调查，发现这个问题与以下因素有关：

1. GHC版本：该问题在GHC 9.12.2中首次出现，在GHC 9.10.2中部分情况可以工作，但在更复杂的场景下仍会出错。

2. Agda编译选项：启用--auto-inline优化选项会增加触发此错误的概率。

3. 代码结构：当Agda代码中包含特定的递归定义和抽象块(abstract blocks)时更容易触发此错误。

4. 内置类型：使用BUILTIN LIST定义列表类型也是触发条件之一。

解决方案

目前推荐的解决方案包括：

1. 降级GHC版本：对于简单场景，使用GHC 9.10.2可以避免此问题。

2. 简化代码结构：通过重构代码，避免复杂的递归定义和抽象块组合。

3. 等待GHC修复：该问题已上报至GHC开发团队，未来版本可能会修复。

4. 避免特定优化：暂时不使用--auto-inline选项可以减少问题发生概率。

性能分析替代方案

在等待GHC修复期间，开发者可以考虑以下替代性能分析方案：

1. 手动插入计时点：在关键函数处手动添加时间测量代码。

2. 使用Agda的调试功能：通过--verbose选项获取更详细的编译信息。

3. 模块化测试：将大型程序拆分为小模块单独测试性能。

总结

这个问题展示了当高级语言(Agda)通过中间编译器(GHC)生成代码时可能遇到的底层问题。虽然性能分析是优化程序的重要工具，但在当前情况下需要谨慎使用。开发者应当根据具体情况选择合适的变通方案，同时关注GHC未来的更新以获取永久性修复。

对于Agda开发者来说，理解这类问题的本质有助于更好地设计代码结构，避免触发编译器边界情况，同时也为参与开源编译器开发提供了宝贵的实践经验。