"Partial" pattern match causes segfault at runtime

[SuprDewd]

Using Agda 2.5.2, the following code type checks, but when executed (agda -c crash.agda && ./crash), it segfaults.

module crash where

open import Data.Nat.Properties.Simple
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Data.Maybe
open import Data.Empty
open import IO
open import Data.Unit
open import Agda.Builtin.IO renaming (IO to BIO)
open import Data.String

data F : ℕ → Set where
  [] : F zero
  _∷1 : ∀ {n} → F n → F (suc n)
  _∷2 : ∀ {n} → F n → F (suc (suc n))

f : ∀ k → F (suc k) → F k ⊎ Maybe ⊥
f zero a = inj₂ nothing
f k (xs ∷1) = inj₂ nothing
-- to (suc k) xs = inj₂ nothing  -- This is fine
f (suc k) = λ xs → inj₂ nothing  -- This segfaults

myshow : F 1 ⊎ Maybe ⊥ → String
-- myshow (inj₁ b) = ""        -- This is fine
myshow (inj₁ (b ∷1)) = ""      -- This segfaults
myshow _ = ""

main : BIO ⊤
main = run (putStrLn (myshow (f 1 ([] ∷2))))

This was also tested using Agda 2.5.1.1, where it fails to type check with the following message:

crash.agda:20,1-23,10
Incomplete pattern matching for f. Missing cases:
  f (suc _) (_∷2 {._} _)
when checking the definition of f

If one looks closely, the pattern matching for f is complete, so it may be that the type checker was made smarter for 2.5.2, but somewhere the runtime is still unable to work out the logic.

[phile314]

Fixed in the GHC backend, still a problem in the JS backend.

[nad]

I restored the labels that you removed. Sometimes we search for fixed issues using labels.