Panic when checking pragma BUILTIN SHARP

[berndlosert]

Agda panics when type-checking this code:

{-# OPTIONS --type-in-type #-}

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

The error is:

Panic: Pattern match failure in do expression at
src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs:68:5-13
when checking the pragma BUILTIN SHARP ♯_

If I remove {-# OPTIONS --type-in-type #-}, it works again. I'm not sure if this is a bug or intended behavior.

[berndlosert]

I'm using 2.6.2 by the way.

[andreasabel]

Thanks for the report @berndlosert!
Still works with 2.6.0, first breaks with 2.6.1.

I think the error location is still accurate:

agda/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs

Line 68 in d8145b9

Def inf _ <- primInf

[andreasabel]

Bisection says: 7807e9a is the first bad commit
Date: Tue Oct 15 14:16:10 2019 +0200
[ fix #3073 ] Don't eta-contract \x -> f l to f when --type-in-type
Ping @jespercockx

This looks plausible, because eta-contraction could have produced the Def form that is matched against at the problematic position.

[andreasabel]

The proposed fix 74f92b5 can be directly exploited, see #5614 (comment).