compiler optimization - High compilation time and CPU in Idris -

i'm playing little formalisation in idris , i'm having strange behaviour: high compilation time , cpu usage function.

the code regex pattern matching algorithm. first regex definition:

data regexp : type   0 : regexp   eps  : regexp   chr  : char -> regexp   cat  : regexp -> regexp -> regexp   alt  : regexp -> regexp -> regexp   star : regexp -> regexp   comp : regexp -> regexp 

regex membership , non-membership defined following mutually recursive data types:

mutual         data notinregexp : list char -> regexp -> type     notinzero : notinregexp xs 0     notineps  : not (xs = []) -> notinregexp xs eps     notinchr  : not (xs = [ c ]) -> notinregexp xs (chr c)     notincat  : zs = xs ++ ys -> (either (notinregexp xs l)                                           ((inregexp xs l)                                          ,(notinregexp ys r)))                               -> notinregexp zs (cat l r)     notinalt  : notinregexp xs l -> notinregexp xs r -> notinregexp xs (alt l r)        notinstar : notinregexp xs eps ->                 notinregexp xs (cat e (star e)) ->                 notinregexp xs (star e)     notincomp : inregexp xs e -> notinregexp xs (comp e)                    data inregexp : list char -> regexp -> type     ineps : inregexp [] eps     inchr : inregexp [ ] (chr a)     incat : inregexp xs l ->             inregexp ys r ->             zs = xs ++ ys ->             inregexp zs (cat l r)     inaltl : inregexp xs l ->              inregexp xs (alt l r)     inaltr : inregexp xs r ->              inregexp xs (alt l r)     instar : inregexp xs (alt eps (cat e (star e))) ->              inregexp xs (star e)     incomp : notinregexp xs e -> inregexp xs (comp e) 

after these rather long definitions, define smart constructor alternatives:

 infixl 4 .|.   (.|.) : regexp -> regexp -> regexp  0 .|. e = e  e .|. 0 = e  e .|. e'   = alt e e' 

now, want prove smart constructor sound , complete respect regex membership semantics. proofs straightforward induction / case analysis. but, 1 of these proofs demanding lot of time , cpu compile (around 90% of cpu in mac os x el capitan).

the offending function is:

 altoptnotincomplete : notinregexp xs (alt l r) -> notinregexp xs (l .|. r)  altoptnotincomplete {l = zero} (notinalt x y) = y  altoptnotincomplete {l = eps}{r = zero} (notinalt x y) = x  altoptnotincomplete {l = eps}{r = eps} pr = pr  altoptnotincomplete {l = eps}{r = (chr x)} pr = pr  altoptnotincomplete {l = eps}{r = (cat x y)} pr = pr  altoptnotincomplete {l = eps}{r = (alt x y)} pr = pr  altoptnotincomplete {l = eps}{r = (star x)} pr = pr  altoptnotincomplete {l = eps}{r = (comp x)} pr = pr  altoptnotincomplete {l = (chr x)}{r = zero} (notinalt y z) = y  altoptnotincomplete {l = (chr x)}{r = eps} pr = pr  altoptnotincomplete {l = (chr x)}{r = (chr y)} pr = pr  altoptnotincomplete {l = (chr x)}{r = (cat y z)} pr = pr  altoptnotincomplete {l = (chr x)}{r = (alt y z)} pr = pr  altoptnotincomplete {l = (chr x)}{r = (star y)} pr = pr  altoptnotincomplete {l = (chr x)}{r = (comp y)} pr = pr  altoptnotincomplete {l = (cat x y)}{r = zero} (notinalt z w) = z  altoptnotincomplete {l = (cat x y)}{r = eps} pr = pr  altoptnotincomplete {l = (cat x y)}{r = (chr z)} pr = pr  altoptnotincomplete {l = (cat x y)}{r = (cat z w)} pr = pr  altoptnotincomplete {l = (cat x y)}{r = (alt z w)} pr = pr  altoptnotincomplete {l = (cat x y)}{r = (star z)} pr = pr  altoptnotincomplete {l = (cat x y)}{r = (comp z)} pr = pr  altoptnotincomplete {l = (alt x y)}{r = zero} (notinalt z w) = z  altoptnotincomplete {l = (alt x y)}{r = eps} pr = pr  altoptnotincomplete {l = (alt x y)}{r = (chr z)} pr = pr  altoptnotincomplete {l = (alt x y)}{r = (cat z w)} pr = pr  altoptnotincomplete {l = (alt x y)}{r = (alt z w)} pr = pr  altoptnotincomplete {l = (alt x y)}{r = (star z)} pr = pr  altoptnotincomplete {l = (alt x y)}{r = (comp z)} pr = pr  altoptnotincomplete {l = (star x)}{r = zero} (notinalt y z) = y  altoptnotincomplete {l = (star x)}{r = eps} pr = pr  altoptnotincomplete {l = (star x)}{r = (chr y)} pr = pr  altoptnotincomplete {l = (star x)}{r = (cat y z)} pr = pr  altoptnotincomplete {l = (star x)}{r = (alt y z)} pr = pr  altoptnotincomplete {l = (star x)}{r = (star y)} pr = pr  altoptnotincomplete {l = (star x)}{r = (comp y)} pr = pr  altoptnotincomplete {l = (comp x)}{r = zero} (notinalt y z) = y  altoptnotincomplete {l = (comp x)}{r = eps} pr = pr  altoptnotincomplete {l = (comp x)}{r = (chr y)} pr = pr  altoptnotincomplete {l = (comp x)}{r = (cat y z)} pr = pr  altoptnotincomplete {l = (comp x)}{r = (alt y z)} pr = pr  altoptnotincomplete {l = (comp x)}{r = (star y)} pr = pr  altoptnotincomplete {l = (comp x)}{r = (comp y)} pr = pr 

i can't understand why function demanding cpu. there way "optimize" code in order compilation behaves normally?

the previous code available @ following gist. i'm using idris 0.10 on mac os x el capitan.

any clue highly welcome.