Compiler takes a very long time/hangs when deriving decidable equality

[mpickering]

Please attach complete source files that exhibit the issue in addition to quoting from them here.

Steps to Reproduce

module Bug4

import Pruviloj.Derive.DecEq
import Pruviloj

%language ElabReflection

%access public export

Name : Type
Name = String

public export
data BRaw : Type where
  BS : BRaw
  BD : BRaw
  BBeta : Name -> BRaw

public export
brawDecEq : (x, y: BRaw) -> Dec (x = y)
%runElab (deriveDecEq `{brawDecEq })

public export
DecEq BRaw where
  decEq = brawDecEq

public export
data CRaw : Type where
  RFunCo : BRaw -> CRaw -> CRaw -> CRaw
  RIntCo : BRaw -> CRaw
  RBoolCo : BRaw -> CRaw

public export
crawDecEq : (x, y: CRaw) -> Dec (x = y)
%runElab (deriveDecEq `{crawDecEq })

public export
DecEq CRaw where
decEq = crawDecEq

idris -p puviloj Bug4.idr

Expected Behavior

Program terminates in a reasonable amount of time

Observed Behavior

Program does not terminate in a reasonable amount of time.

[ahmadsalim]

@mpickering Thanks for reporting the issue.

Do you know if it actually does not terminate or whether it is just really slow?

[mpickering]

I don't know if it terminates.

[ahmadsalim]

I have just tested it, it is just really slow but does terminate.