Skipping compilation for up-to-date files results in mis-compilation

Open
  • Is something wrong?
#486 2 comments 0 reactions 1 assignee View on GitHub

Maintainers usually reply within 1 day

@jespercockx is already working on this.

Since Nov 13, 2026.

  • #490 by @jespercockx — open

Assessment

Difficulty
3/5
Estimated time
1-2 days
Newbie friendliness
52/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Tech stack
haskell
Domain
build-system, tooling

Research direction

Start by reading the compilation path that handles up-to-date files and the generated Haskell for Issue486.File1 and Issue486.File2. Reproduce the sequence in the issue: compile from scratch, remove the generated Issue486.File2.hs, then compile again. Done means the regenerated file correctly compiles away Vec and num, as it does on a clean build.

Written by the indexing model from the issue text.

Description

bug

Consider the following files:

module Issue486.File1 where

open import Haskell.Prelude

private variable
  @0 n : Nat

data Vec (a : Type) : @0 Nat → Type where
  []  : Vec a zero
  _∷_ : a → Vec a n → Vec a (suc n)
{-# COMPILE AGDA2HS Vec to List #-}

foo : Vec a 0
foo = []
{-# COMPILE AGDA2HS foo #-}

num : Nat
num = 42
{-# COMPILE AGDA2HS num inline #-}

module Issue486.File2 where

open import Haskell.Prelude

open import Issue486.File1

bar : Vec a 0
bar = foo
{-# COMPILE AGDA2HS bar #-}

num' : Nat
num' = num
{-# COMPILE AGDA2HS num' #-}

agda2hs generates correct code if we start from scratch. However, if we then remove Issue485.File2.hs and compile again, agda2hs generates this invalid code in which Vec and num aren't compiled away:

module Issue486.File2
  (bar, num')
where

import Issue486.File1 (Vec, foo, num)
import Numeric.Natural (Natural)

bar :: Vec a
bar = foo

num' :: Natural
num' = num
Dominant language
Agda
Stars
211
Forks
51
Avg merge
1d 11h
Merged PRs (30d)
9

Getting set up

This project ships no dev container, Dockerfile or contributing guide, so setting up is up to you: start from its README, and see our first-contribution guide for the general steps.

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from agda/agda2hs

All issues in agda/agda2hs

Similar issues

More Build System issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.