Internal error related to eta-expansion

asr / apia

Haskell program for proving first-order theorems written in Agda using automatic theorem provers for first-order logic

MIT License

6 stars 0 forks source link

Internal error related to eta-expansion #78

Open asr opened 7 years ago

asr commented 7 years ago

module Bug where

postulate
  D   : Set
  P   : D → Set
  k   : D
  Pk  : P k
  _≡_ : D → D → Set

c : (a : D) → P a → D
c a Pa = k
{-# ATP definition c #-}

postulate foo : c k Pk ≡ k
{-# ATP prove foo #-}

$ apia Bug.agda
An internal error has occurred. Please report this as a bug.
Location of the error: src/Apia/Utils/AgdaAPI/EtaExpansion.hs:74

asr commented 7 years ago

Blocked by #81.